Library GeoCoq.Tactics.Coinc.tarski_to_coinc_theory_for_cop

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


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 : ∀ A X, app_1_n not_col A X → app_n_1 not_col X A.
Proof.
unfold not_col.
simpl.
Col.
Qed.

Lemma not_col_perm_2 : ∀ A B (X : cartesianPower Tpoint 1),
  app_2_n not_col A B X → app_2_n not_col B A X.
Proof.
unfold not_col.
unfold app_2_n.
simpl.
Col.
Qed.

Definition cop : arity Tpoint 4 := Coplanar.

Lemma cop_perm_1 : ∀ A (X : cartesianPower Tpoint 3), app_1_n cop A X → app_n_1 cop X A.
Proof.
unfold cop.
simpl.
Cop.
Qed.

Lemma cop_perm_2 : ∀ A B (X : cartesianPower Tpoint 2), app_2_n cop A B X → app_2_n cop B A X.
Proof.
unfold cop.
unfold app_2_n.
simpl.
Cop.
Qed.

Lemma cop_bd : ∀ A (X : cartesianPower Tpoint 2), app_2_n cop A A X.
Proof.
unfold cop.
unfold app_2_n.
simpl.
Cop.
Qed.

Lemma cop_3 : ∀ (COP : cartesianPower Tpoint 4) (NOT_COL : cartesianPower Tpoint 3),
  pred_conj cop COP NOT_COL → app not_col NOT_COL → app cop COP.
Proof.
unfold pred_conj.
unfold cop.
unfold not_col.
simpl in ×.
intros COP NOT_COL HCop HNot_Col.
destruct HCop as [HCop1 [HCop2 [HCop3 HCop4]]].
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.
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.
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.