Require Import GeoCoq.Utils.arity.
Require Import GeoCoq.Tactics.Coinc.tactics_axioms.

Section Permutations.

Context `{COT : Coinc_theory}.

Lemma PermWdOK :
  forall (cp1 cp2 : cartesianPower COINCpoint (S (S n))),
  app wd cp1 ->
  Permutation.Permutation (CPToList cp1) (CPToList cp2) ->
  app wd cp2.
Proof.
(* Goal: forall (cp1 cp2 : cartesianPower (@COINCpoint Ar) (S (S (S (@n Ar))))) (_ : @app (@COINCpoint Ar) (S (S (S (@n Ar)))) (@coinc Ar COP) cp1) (_ : @Permutation.Permutation (@COINCpoint Ar) (@CPToList (@COINCpoint Ar) (S (S (S (@n Ar)))) cp1) (@CPToList (@COINCpoint Ar) (S (S (S (@n Ar)))) cp2)), @app (@COINCpoint Ar) (S (S (S (@n Ar)))) (@coinc Ar COP) cp2 *)
intros cp1 cp2 Happ HPerm.
(* Goal: @app (@COINCpoint Ar) (S (S (S (@n Ar)))) (@coinc Ar COP) cp2 *)
apply PermOK with cp1; try assumption; clear HPerm; clear Happ; clear cp2; clear cp1.

  intros A X Happ; apply app_n_1_app with A X; try (apply wd_perm_1;
  apply app_app_1_n with (consHeadCP A X); try assumption).

(* Goal: @eq (@COINCpoint Ar) (@headCP (@COINCpoint Ar) (S (@n Ar)) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) A *)
(* Goal: @eq (cartesianPower (@COINCpoint Ar) (S (@n Ar))) (@tailCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) X *)
    simpl; reflexivity.

(* Goal: @eq (cartesianPower (@COINCpoint Ar) (S (@n Ar))) (@tailCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) X *)
    apply consHeadCPTl.

(* Goal: @eq (cartesianPower (@COINCpoint Ar) (S (S (@n Ar)))) (@allButLastCP (@COINCpoint Ar) (S (@n Ar)) (@consTailCP (@COINCpoint Ar) (S (S (@n Ar))) X A)) X *)
(* Goal: @eq (@COINCpoint Ar) (@lastCP (@COINCpoint Ar) (S (S (@n Ar))) (@consTailCP (@COINCpoint Ar) (S (S (@n Ar))) X A)) A *)
(* Goal: forall (A B : @COINCpoint Ar) (X : cartesianPower (@COINCpoint Ar) (S (@n Ar))) (_ : @app (@COINCpoint Ar) (S (S (S (@n Ar)))) (@coinc Ar COP) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) A (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) B X))), @app (@COINCpoint Ar) (S (S (S (@n Ar)))) (@coinc Ar COP) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)) *)
    apply consTailCPAbl.

(* Goal: @eq (@COINCpoint Ar) (@lastCP (@COINCpoint Ar) (S (S (@n Ar))) (@consTailCP (@COINCpoint Ar) (S (S (@n Ar))) X A)) A *)
(* Goal: forall (A B : @COINCpoint Ar) (X : cartesianPower (@COINCpoint Ar) (S (@n Ar))) (_ : @app (@COINCpoint Ar) (S (S (S (@n Ar)))) (@coinc Ar COP) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) A (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) B X))), @app (@COINCpoint Ar) (S (S (S (@n Ar)))) (@coinc Ar COP) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)) *)
    apply consTailCPLast.

  intros A B X Happ; apply app_2_n_app_default with B A X X; try (apply wd_perm_2;
  apply app_app_2_n_default with X (consHeadCP A (consHeadCP B X)); try assumption).

(* Goal: @eq (@COINCpoint Ar) (@headCP (@COINCpoint Ar) (S (@n Ar)) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) A *)
(* Goal: @eq (cartesianPower (@COINCpoint Ar) (S (@n Ar))) (@tailCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) X *)
    simpl; reflexivity.

(* Goal: @eq (@COINCpoint Ar) (@headCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (@n Ar) (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) B (@consHeadCP (@COINCpoint Ar) (@n Ar) A X)))) A *)
(* Goal: @eq (cartesianPower (@COINCpoint Ar) (@n Ar)) (@tailDefaultCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (@n Ar) (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) B (@consHeadCP (@COINCpoint Ar) (@n Ar) A X))) X) X *)
    rewrite consHeadCPTl; rewrite consHeadCPHd; reflexivity.

(* Goal: @eq (cartesianPower (@COINCpoint Ar) (@n Ar)) (@tailDefaultCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (@n Ar) (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) B (@consHeadCP (@COINCpoint Ar) (@n Ar) A X))) X) X *)
    rewrite consHeadCPTl; apply consTailCPTlD.

(* Goal: @eq (@COINCpoint Ar) (@headCP (@COINCpoint Ar) (S (@n Ar)) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) A *)
(* Goal: @eq (cartesianPower (@COINCpoint Ar) (S (@n Ar))) (@tailCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) X *)
    simpl; reflexivity.

(* Goal: @eq (@COINCpoint Ar) (@headCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (@n Ar) (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) B (@consHeadCP (@COINCpoint Ar) (@n Ar) A X)))) A *)
(* Goal: @eq (cartesianPower (@COINCpoint Ar) (@n Ar)) (@tailDefaultCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (@n Ar) (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) B (@consHeadCP (@COINCpoint Ar) (@n Ar) A X))) X) X *)
    rewrite consHeadCPTl; rewrite consHeadCPHd; reflexivity.

(* Goal: @eq (cartesianPower (@COINCpoint Ar) (@n Ar)) (@tailDefaultCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (@n Ar) (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) B (@consHeadCP (@COINCpoint Ar) (@n Ar) A X))) X) X *)
    rewrite consHeadCPTl; apply consTailCPTlD.
Qed.

Lemma PermCoincOK :
  forall (cp1 cp2 : cartesianPower COINCpoint (S (S (S n)))),
  app coinc cp1 ->
  Permutation.Permutation (CPToList cp1) (CPToList cp2) ->
  app coinc cp2.
Proof.
(* Goal: forall (cp1 cp2 : cartesianPower (@COINCpoint Ar) (S (S (S (@n Ar))))) (_ : @app (@COINCpoint Ar) (S (S (S (@n Ar)))) (@coinc Ar COP) cp1) (_ : @Permutation.Permutation (@COINCpoint Ar) (@CPToList (@COINCpoint Ar) (S (S (S (@n Ar)))) cp1) (@CPToList (@COINCpoint Ar) (S (S (S (@n Ar)))) cp2)), @app (@COINCpoint Ar) (S (S (S (@n Ar)))) (@coinc Ar COP) cp2 *)
intros cp1 cp2 Happ HPerm.
(* Goal: @app (@COINCpoint Ar) (S (S (S (@n Ar)))) (@coinc Ar COP) cp2 *)
apply PermOK with cp1; try assumption; clear HPerm; clear Happ; clear cp2; clear cp1.

  intros A X Happ; apply app_n_1_app with A X; try (apply coinc_perm_1;
  apply app_app_1_n with (consHeadCP A X); try assumption).

(* Goal: @eq (@COINCpoint Ar) (@headCP (@COINCpoint Ar) (S (@n Ar)) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) A *)
(* Goal: @eq (cartesianPower (@COINCpoint Ar) (S (@n Ar))) (@tailCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) X *)
    simpl; reflexivity.

(* Goal: @eq (cartesianPower (@COINCpoint Ar) (S (@n Ar))) (@tailCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) X *)
    apply consHeadCPTl.

(* Goal: @eq (cartesianPower (@COINCpoint Ar) (S (S (@n Ar)))) (@allButLastCP (@COINCpoint Ar) (S (@n Ar)) (@consTailCP (@COINCpoint Ar) (S (S (@n Ar))) X A)) X *)
(* Goal: @eq (@COINCpoint Ar) (@lastCP (@COINCpoint Ar) (S (S (@n Ar))) (@consTailCP (@COINCpoint Ar) (S (S (@n Ar))) X A)) A *)
(* Goal: forall (A B : @COINCpoint Ar) (X : cartesianPower (@COINCpoint Ar) (S (@n Ar))) (_ : @app (@COINCpoint Ar) (S (S (S (@n Ar)))) (@coinc Ar COP) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) A (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) B X))), @app (@COINCpoint Ar) (S (S (S (@n Ar)))) (@coinc Ar COP) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)) *)
    apply consTailCPAbl.

(* Goal: @eq (@COINCpoint Ar) (@lastCP (@COINCpoint Ar) (S (S (@n Ar))) (@consTailCP (@COINCpoint Ar) (S (S (@n Ar))) X A)) A *)
(* Goal: forall (A B : @COINCpoint Ar) (X : cartesianPower (@COINCpoint Ar) (S (@n Ar))) (_ : @app (@COINCpoint Ar) (S (S (S (@n Ar)))) (@coinc Ar COP) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) A (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) B X))), @app (@COINCpoint Ar) (S (S (S (@n Ar)))) (@coinc Ar COP) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)) *)
    apply consTailCPLast.

  intros A B X Happ; apply app_2_n_app with B A X; try (apply coinc_perm_2;
  apply app_app_2_n with (consHeadCP A (consHeadCP B X)); try assumption).

(* Goal: @eq (@COINCpoint Ar) (@headCP (@COINCpoint Ar) (S (@n Ar)) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) A *)
(* Goal: @eq (cartesianPower (@COINCpoint Ar) (S (@n Ar))) (@tailCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) X *)
    simpl; reflexivity.

(* Goal: @eq (@COINCpoint Ar) (@headCP (@COINCpoint Ar) (S (@n Ar)) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) A *)
(* Goal: @eq (cartesianPower (@COINCpoint Ar) (S (@n Ar))) (@tailCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) X *)
    simpl; reflexivity.

(* Goal: @eq (cartesianPower (@COINCpoint Ar) (S (@n Ar))) (@tailCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) X *)
    apply consHeadCPTl.

(* Goal: @eq (@COINCpoint Ar) (@headCP (@COINCpoint Ar) (S (@n Ar)) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) A *)
(* Goal: @eq (cartesianPower (@COINCpoint Ar) (S (@n Ar))) (@tailCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) X *)
    simpl; reflexivity.

(* Goal: @eq (@COINCpoint Ar) (@headCP (@COINCpoint Ar) (S (@n Ar)) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) A *)
(* Goal: @eq (cartesianPower (@COINCpoint Ar) (S (@n Ar))) (@tailCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) X *)
    simpl; reflexivity.

(* Goal: @eq (cartesianPower (@COINCpoint Ar) (S (@n Ar))) (@tailCP (@COINCpoint Ar) (@n Ar) (@tailCP (@COINCpoint Ar) (S (@n Ar)) (@consHeadCP (@COINCpoint Ar) (S (S (@n Ar))) B (@consHeadCP (@COINCpoint Ar) (S (@n Ar)) A X)))) X *)
    apply consHeadCPTl.
Qed.

End Permutations.
