Library GeoCoq.Tactics.Coinc.tactics_axioms

Require Export GeoCoq.Utils.arity.

Class Col_theory (COLTpoint : Type) (CTCol: COLTpoint → COLTpoint → COLTpoint → Prop) :=
{
  CTcol_trivial : ∀ A B : COLTpoint, CTCol A A B;
  CTcol_permutation_1 : ∀ A B C : COLTpoint, CTCol A B C → CTCol B C A;
  CTcol_permutation_2 : ∀ A B C : COLTpoint, CTCol A B C → CTCol A C B;
  CTcol3 : ∀ X Y A B C : COLTpoint,
             X ≠ Y → CTCol X Y A → CTCol X Y B → CTCol X Y C → CTCol A B C
}.

Class Arity :=
{
  COINCpoint : Type;
  n : nat
}.

Class Coinc_predicates (Ar : Arity) :=
{
  wd : arity COINCpoint (S (S n));
  coinc : arity COINCpoint (S (S (S n)))
}.

Class Coinc_theory (Ar : Arity) (COP : Coinc_predicates Ar) :=
{
  wd_perm_1 : ∀ A : COINCpoint,
              ∀ X : cartesianPower COINCpoint (S n),
                app_1_n wd A X → app_n_1 wd X A;
  wd_perm_2 : ∀ A B : COINCpoint,
              ∀ X : cartesianPower COINCpoint n,
                app_2_n wd A B X → app_2_n wd B A X;
  coinc_perm_1 : ∀ A : COINCpoint,
                 ∀ X : cartesianPower COINCpoint (S (S n)),
                   app_1_n coinc A X → app_n_1 coinc X A;
  coinc_perm_2 : ∀ A B : COINCpoint,
                 ∀ X : cartesianPower COINCpoint (S n),
                   app_2_n coinc A B X → app_2_n coinc B A X;
  coinc_bd : ∀ A : COINCpoint,
             ∀ X : cartesianPower COINCpoint (S n),
              app_2_n coinc A A X;
  coinc_n : ∀ COINC : cartesianPower COINCpoint (S (S (S n))),
            ∀ WD : cartesianPower COINCpoint (S (S n)),
              pred_conj coinc COINC WD →
              app wd WD →
              app coinc COINC
}.