Require Import GeoCoq.Tarski_dev.Ch09_plane.
Require Import GeoCoq.Tactics.Coinc.tactics_axioms.

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

Section Tarski_is_a_Coinc_theory_for_cop.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Definition not_col : arity Tpoint 3 := fun A B C : Tpoint => ~ Col A B C.

Lemma not_col_perm_1 : forall A X, app_1_n not_col A X -> app_n_1 not_col X A.
Proof.
(* Goal: forall (COP : cartesianPower (@Tpoint Tn) (S (S (S (S O))))) (NOT_COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S (S O))) (@Coplanar Tn) (S (S (S O))) COP NOT_COL) (_ : @app (@Tpoint Tn) (S (S (S O))) not_col NOT_COL), @app (@Tpoint Tn) (S (S (S (S O)))) (@Coplanar Tn) COP *)
unfold not_col.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S (S O))), @app (@Tpoint Tn) (S (S O)) (@Coplanar Tn A A) X *)
simpl.
(* Goal: forall (A B : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S O)) (_ : not (@Col Tn A B X)), not (@Col Tn B A X) *)
Col.
Qed.

Lemma not_col_perm_2 : forall A B (X : cartesianPower Tpoint 1),
  app_2_n not_col A B X -> app_2_n not_col B A X.
Proof.
(* Goal: forall (COP : cartesianPower (@Tpoint Tn) (S (S (S (S O))))) (NOT_COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S (S O))) (@Coplanar Tn) (S (S (S O))) COP NOT_COL) (_ : @app (@Tpoint Tn) (S (S (S O))) not_col NOT_COL), @app (@Tpoint Tn) (S (S (S (S O)))) (@Coplanar Tn) COP *)
unfold not_col.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S (S O))), @app_2_n (@Tpoint Tn) (S (S O)) (@Coplanar Tn) A A X *)
unfold app_2_n.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S (S O))), @app (@Tpoint Tn) (S (S O)) (@Coplanar Tn A A) X *)
simpl.
(* Goal: forall (A B : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S O)) (_ : not (@Col Tn A B X)), not (@Col Tn B A X) *)
Col.
Qed.

Definition cop : arity Tpoint 4 := Coplanar.

Lemma cop_perm_1 : forall A (X : cartesianPower Tpoint 3), app_1_n cop A X -> app_n_1 cop X A.
Proof.
(* Goal: forall (COP : cartesianPower (@Tpoint Tn) (S (S (S (S O))))) (NOT_COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S (S O))) cop (S (S (S O))) COP NOT_COL) (_ : @app (@Tpoint Tn) (S (S (S O))) not_col NOT_COL), @app (@Tpoint Tn) (S (S (S (S O)))) cop COP *)
unfold cop.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S (S O))), @app (@Tpoint Tn) (S (S O)) (@Coplanar Tn A A) X *)
simpl.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S (S O))), @Coplanar Tn A A (@fst (@Tpoint Tn) (@Tpoint Tn) X) (@snd (@Tpoint Tn) (@Tpoint Tn) X) *)
Cop.
Qed.

Lemma cop_perm_2 : forall A B (X : cartesianPower Tpoint 2), app_2_n cop A B X -> app_2_n cop B A X.
Proof.
(* Goal: forall (COP : cartesianPower (@Tpoint Tn) (S (S (S (S O))))) (NOT_COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S (S O))) cop (S (S (S O))) COP NOT_COL) (_ : @app (@Tpoint Tn) (S (S (S O))) not_col NOT_COL), @app (@Tpoint Tn) (S (S (S (S O)))) cop COP *)
unfold cop.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S (S O))), @app_2_n (@Tpoint Tn) (S (S O)) (@Coplanar Tn) A A X *)
unfold app_2_n.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S (S O))), @app (@Tpoint Tn) (S (S O)) (@Coplanar Tn A A) X *)
simpl.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S (S O))), @Coplanar Tn A A (@fst (@Tpoint Tn) (@Tpoint Tn) X) (@snd (@Tpoint Tn) (@Tpoint Tn) X) *)
Cop.
Qed.

Lemma cop_bd : forall A (X : cartesianPower Tpoint 2), app_2_n cop A A X.
Proof.
(* Goal: forall (COP : cartesianPower (@Tpoint Tn) (S (S (S (S O))))) (NOT_COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S (S O))) cop (S (S (S O))) COP NOT_COL) (_ : @app (@Tpoint Tn) (S (S (S O))) not_col NOT_COL), @app (@Tpoint Tn) (S (S (S (S O)))) cop COP *)
unfold cop.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S (S O))), @app_2_n (@Tpoint Tn) (S (S O)) (@Coplanar Tn) A A X *)
unfold app_2_n.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S (S O))), @app (@Tpoint Tn) (S (S O)) (@Coplanar Tn A A) X *)
simpl.
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S (S O))), @Coplanar Tn A A (@fst (@Tpoint Tn) (@Tpoint Tn) X) (@snd (@Tpoint Tn) (@Tpoint Tn) X) *)
Cop.
Qed.

Lemma cop_3 : forall (COP : cartesianPower Tpoint 4) (NOT_COL : cartesianPower Tpoint 3),
  pred_conj cop COP NOT_COL -> app not_col NOT_COL -> app cop COP.
Proof.
(* Goal: forall (COP : cartesianPower (@Tpoint Tn) (S (S (S (S O))))) (NOT_COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (_ : @pred_conj (@Tpoint Tn) (S (S (S O))) cop COP NOT_COL) (_ : @app (@Tpoint Tn) (S (S (S O))) not_col NOT_COL), @app (@Tpoint Tn) (S (S (S (S O)))) cop COP *)
unfold pred_conj.
(* Goal: forall (COP : cartesianPower (@Tpoint Tn) (S (S (S (S O))))) (NOT_COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S (S O))) cop (S (S (S O))) COP NOT_COL) (_ : @app (@Tpoint Tn) (S (S (S O))) not_col NOT_COL), @app (@Tpoint Tn) (S (S (S (S O)))) cop COP *)
unfold cop.
(* Goal: forall (COP : cartesianPower (@Tpoint Tn) (S (S (S (S O))))) (NOT_COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S (S O))) (@Coplanar Tn) (S (S (S O))) COP NOT_COL) (_ : @app (@Tpoint Tn) (S (S (S O))) not_col NOT_COL), @app (@Tpoint Tn) (S (S (S (S O)))) (@Coplanar Tn) COP *)
unfold not_col.
(* Goal: forall (COP : cartesianPower (@Tpoint Tn) (S (S (S (S O))))) (NOT_COL : cartesianPower (@Tpoint Tn) (S (S (S O)))) (_ : @pred_conj_aux (@Tpoint Tn) (S (S (S O))) (@Coplanar Tn) (S (S (S O))) COP NOT_COL) (_ : @app (@Tpoint Tn) (S (S (S O))) (fun A B C : @Tpoint Tn => not (@Col Tn A B C)) NOT_COL), @app (@Tpoint Tn) (S (S (S (S O)))) (@Coplanar Tn) COP *)
simpl in *.
(* Goal: forall (A B : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S O)) (_ : not (@Col Tn A B X)), not (@Col Tn B A X) *)
intros COP NOT_COL HCop HNot_Col.
(* Goal: @Coplanar Tn (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) COP) (@fst (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) COP)) (@fst (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) COP))) (@snd (@Tpoint Tn) (@Tpoint Tn) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn)) (@snd (@Tpoint Tn) (prod (@Tpoint Tn) (prod (@Tpoint Tn) (@Tpoint Tn))) COP))) *)
destruct HCop as [HCop1 [HCop2 [HCop3 HCop4]]].
(* Goal: forall (A : @Tpoint Tn) (X : cartesianPower (@Tpoint Tn) (S (S O))), @Coplanar Tn A A (@fst (@Tpoint Tn) (@Tpoint Tn) X) (@snd (@Tpoint Tn) (@Tpoint Tn) X) *)
apply coplanar_pseudo_trans with (fst NOT_COL) (fst (snd NOT_COL)) (snd (snd NOT_COL)); Cop.
Qed.

Global Instance Tarski_is_a_Arity_for_cop : Arity.
(* Goal: Arity *)
Proof. exact (Build_Arity Tpoint 1). Defined.

Global Instance Tarski_is_a_Coinc_predicates_for_cop :
  (Coinc_predicates Tarski_is_a_Arity_for_cop).
Proof.
(* Goal: Coinc_predicates Tarski_is_a_Arity_for_cop *)
exact (Build_Coinc_predicates Tarski_is_a_Arity_for_cop not_col cop).
Defined.

Global Instance Tarski_is_a_Coinc_theory_for_cop :   (Coinc_theory Tarski_is_a_Arity_for_cop Tarski_is_a_Coinc_predicates_for_cop).
Proof.
exact (Build_Coinc_theory Tarski_is_a_Arity_for_cop
                          Tarski_is_a_Coinc_predicates_for_cop
                          not_col_perm_1 not_col_perm_2 cop_perm_1 cop_perm_2
                          cop_bd cop_3).
Defined.

End Tarski_is_a_Coinc_theory_for_cop.