Require Export GeoCoq.Tarski_dev.Ch06_out_lines.
Require Import GeoCoq.Tactics.Coinc.tactics_axioms.

(* In this file we prove that Col in Tarski neutral dimensionless is a Coinc_theory *)

Section Tarski_is_a_Coinc_theory_for_col.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Definition diff : arity Tpoint 2 := fun A B : Tpoint => A <> B.

Lemma diff_perm_1 : forall A B, app_1_n diff A B -> app_n_1 diff B A.
Proof.
(* Goal: forall (COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (DIFF : cartesianPower (@Tpoint Tn) (S (S O))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S O)) (@Col Tn) (S (S O)) COL DIFF) (_ : @app (@Tpoint Tn) (S (S O)) diff DIFF), @app (@Tpoint Tn) (S (S (S O))) (@Col Tn) COL *)
unfold diff.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S O)), @app (@Tpoint Tn) (S O) (@Col Tn A A) X *)
simpl.
(* Goal: forall (A B : @Tpoint Tn) (_ : cartesianPower (@Tpoint Tn) O) (_ : not (@eq (@Tpoint Tn) A B)), not (@eq (@Tpoint Tn) B A) *)
auto.
Qed.

Lemma diff_perm_2 : forall A B (X : cartesianPower Tpoint 0), app_2_n diff A B X -> app_2_n diff B A X.
Proof.
(* Goal: forall (COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (DIFF : cartesianPower (@Tpoint Tn) (S (S O))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S O)) (@Col Tn) (S (S O)) COL DIFF) (_ : @app (@Tpoint Tn) (S (S O)) diff DIFF), @app (@Tpoint Tn) (S (S (S O))) (@Col Tn) COL *)
unfold diff.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S O)), @app_2_n (@Tpoint Tn) (S O) (@Col Tn) A A X *)
unfold app_2_n.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S O)), @app (@Tpoint Tn) (S O) (@Col Tn A A) X *)
simpl.
(* Goal: forall (A B : @Tpoint Tn) (_ : cartesianPower (@Tpoint Tn) O) (_ : not (@eq (@Tpoint Tn) A B)), not (@eq (@Tpoint Tn) B A) *)
auto.
Qed.

Definition col : arity Tpoint 3 := Col.

Lemma col_perm_1 : forall A (X : cartesianPower Tpoint 2), app_1_n col A X -> app_n_1 col X A.
Proof.
(* Goal: forall (COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (DIFF : cartesianPower (@Tpoint Tn) (S (S O))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S O)) col (S (S O)) COL DIFF) (_ : @app (@Tpoint Tn) (S (S O)) diff DIFF), @app (@Tpoint Tn) (S (S (S O))) col COL *)
unfold col.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S O)), @app (@Tpoint Tn) (S O) (@Col Tn A A) X *)
simpl.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S O)), @Col Tn A A X *)
Col.
Qed.

Lemma col_perm_2 : forall A B (X : cartesianPower Tpoint 1), app_2_n col A B X -> app_2_n col B A X.
Proof.
(* Goal: forall (COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (DIFF : cartesianPower (@Tpoint Tn) (S (S O))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S O)) col (S (S O)) COL DIFF) (_ : @app (@Tpoint Tn) (S (S O)) diff DIFF), @app (@Tpoint Tn) (S (S (S O))) col COL *)
unfold col.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S O)), @app_2_n (@Tpoint Tn) (S O) (@Col Tn) A A X *)
unfold app_2_n.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S O)), @app (@Tpoint Tn) (S O) (@Col Tn A A) X *)
simpl.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S O)), @Col Tn A A X *)
Col.
Qed.

Lemma col_bd : forall A (X : cartesianPower Tpoint 1), app_2_n col A A X.
Proof.
(* Goal: forall (COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (DIFF : cartesianPower (@Tpoint Tn) (S (S O))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S O)) col (S (S O)) COL DIFF) (_ : @app (@Tpoint Tn) (S (S O)) diff DIFF), @app (@Tpoint Tn) (S (S (S O))) col COL *)
unfold col.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S O)), @app_2_n (@Tpoint Tn) (S O) (@Col Tn) A A X *)
unfold app_2_n.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S O)), @app (@Tpoint Tn) (S O) (@Col Tn A A) X *)
simpl.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S O)), @Col Tn A A X *)
Col.
Qed.

Lemma col_3 : forall (COL : cartesianPower Tpoint 3) (DIFF : cartesianPower Tpoint 2),
  pred_conj col COL DIFF -> app diff DIFF -> app col COL.
Proof.
(* Goal: forall (COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (DIFF : cartesianPower (@Tpoint Tn) (S (S O))) (_ : @pred_conj (@Tpoint Tn) (S (S O)) col COL DIFF) (_ : @app (@Tpoint Tn) (S (S O)) diff DIFF), @app (@Tpoint Tn) (S (S (S O))) col COL *)
unfold pred_conj.
(* Goal: forall (COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (DIFF : cartesianPower (@Tpoint Tn) (S (S O))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S O)) col (S (S O)) COL DIFF) (_ : @app (@Tpoint Tn) (S (S O)) diff DIFF), @app (@Tpoint Tn) (S (S (S O))) col COL *)
unfold col.
(* Goal: forall (COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (DIFF : cartesianPower (@Tpoint Tn) (S (S O))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S O)) (@Col Tn) (S (S O)) COL DIFF) (_ : @app (@Tpoint Tn) (S (S O)) diff DIFF), @app (@Tpoint Tn) (S (S (S O))) (@Col Tn) COL *)
unfold diff.
(* Goal: forall (COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (DIFF : cartesianPower (@Tpoint Tn) (S (S O))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S O)) (@Col Tn) (S (S O)) COL DIFF) (_ : @app (@Tpoint Tn) (S (S O)) (fun A B : @Tpoint Tn => not (@eq (@Tpoint Tn) A B)) DIFF), @app (@Tpoint Tn) (S (S (S O))) (@Col Tn) COL *)
simpl in *.
(* Goal: forall (COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (DIFF : cartesianPower (@Tpoint Tn) (S (S O))) (_ : and (@Col Tn (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) COL) (@fst (@Tpoint Tn) (@Tpoint Tn) DIFF) (@snd (@Tpoint Tn) (@Tpoint Tn) DIFF)) (and (@Col Tn (@fst (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) COL)) (@fst (@Tpoint Tn) (@Tpoint Tn) DIFF) (@snd (@Tpoint Tn) (@Tpoint Tn) DIFF)) (@Col Tn (@snd (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) COL)) (@fst (@Tpoint Tn) (@Tpoint Tn) DIFF) (@snd (@Tpoint Tn) (@Tpoint Tn) DIFF)))) (_ : not (@eq (@Tpoint Tn) (@fst (@Tpoint Tn) (@Tpoint Tn) DIFF) (@snd (@Tpoint Tn) (@Tpoint Tn) DIFF))), @Col Tn (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) COL) (@fst (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) COL)) (@snd (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) COL)) *)
intros COL DIFF HCol HDiff.
(* Goal: @Col Tn (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) COL) (@fst (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) COL)) (@snd (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) COL)) *)
destruct HCol as [HCol1 [HCol2 HCol3]].
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S O)), @Col Tn A A X *)
apply col3 with (fst DIFF) (snd DIFF); Col.
Qed.

Global Instance Tarski_is_a_Arity_for_col : Arity.
(* Goal: Arity *)
Proof. exact (Build_Arity Tpoint 0). Defined.

Global Instance Tarski_is_a_Coinc_predicates_for_col :
  (Coinc_predicates Tarski_is_a_Arity_for_col).
Proof.
(* Goal: Coinc_predicates Tarski_is_a_Arity_for_col *)
exact (Build_Coinc_predicates Tarski_is_a_Arity_for_col diff Col).
Defined.

Global Instance Tarski_is_a_Coinc_theory_for_col :
  (Coinc_theory Tarski_is_a_Arity_for_col Tarski_is_a_Coinc_predicates_for_col).
Proof.
exact (Build_Coinc_theory Tarski_is_a_Arity_for_col
                          Tarski_is_a_Coinc_predicates_for_col
                          diff_perm_1 diff_perm_2 col_perm_1 col_perm_2
                          col_bd col_3).
Defined.

End Tarski_is_a_Coinc_theory_for_col.