Library tarski_to_coapp_theory

Require Export Ch06_out_lines.
Require Import tactics_axioms.


Section Tarski_is_a_Coapp_theory.

Context `{MT:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.

Definition diff : arity Tpoint 2 := fun A B : Tpoint ⇒ A ≠ B.

Lemma diff_perm_1 : ∀ A B, app_1_n diff A B → app_n_1 diff B A.
Proof.
unfold diff.
simpl.
auto.
Qed.

Lemma diff_perm_2 : ∀ A B (X : cartesianPower Tpoint 0), app_2_n diff A B X → app_2_n diff B A X.
Proof.
unfold diff.
unfold app_2_n.
simpl.
auto.
Qed.

Definition col : arity Tpoint 3 := Col.

Lemma col_perm_1 : ∀ A (X : cartesianPower Tpoint 2), app_1_n col A X → app_n_1 col X A.
Proof.
unfold col.
simpl.
Col.
Qed.

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

Lemma diff_or_col : ∀ A (X : cartesianPower Tpoint 2), app_1_n col A X ∨ app diff X.
Proof.
unfold col.
unfold diff.
simpl.
intros.
elim (eq_dec_points (fst X) (snd X)); intro H; try rewrite H; Col.
Qed.

Lemma pseudo_trans : ∀ A B C (X : cartesianPower Tpoint 1),
  app_1_n diff A X → app_2_n col B A X → app_2_n col C A X → app_2_n col B C X.
Proof.
unfold col.
unfold diff.
unfold app_2_n.
simpl.
eCol.
Qed.

Global Instance Tarski_is_a_Coapp_theory : (Coapp_theory (Build_Arity Tpoint 0) (Build_Coapp_predicates (Build_Arity Tpoint 0) diff Col)).
Proof.
exact (Build_Coapp_theory (Build_Arity Tpoint 0) (Build_Coapp_predicates (Build_Arity Tpoint 0) diff Col) diff_perm_1 diff_perm_2 col_perm_1 col_perm_2 diff_or_col pseudo_trans).
Qed.

End Tarski_is_a_Coapp_theory.