Library tuple3

Require Import List Eqdep_dec Compare Bool Field Field_tac.
Require Import VectorSpace Grassmann G3.

Fixpoint natc (m n : nat) :=
match m, n with 0, 0 => Eq | 0, _ => Lt | _, 0 => Gt | S m1, S n1 => natc m1 n1 end.

Lemma natc_correct m n :
  match natc m n with Eq => m = n | Lt => m < n | Gt => n < m end.

Lemma natc_eq m n :
  match natc m n with
  | Eq => m = n
  | _ => True
  end.

Section FF.

Grassman for n = 3                               
Variable K : fparams.
Hypothesis FT :
  @field_theory (Field.K K) (v0 K) (v1 K) (addK K) (multK K)
        (fun x y => (addK K) x (oppK K y)) (oppK K)
        (fun x y => (multK K) x (invK K y)) (invK K) (@Logic.eq K).
Add Field Kfth : FT.
Definition Pp : params := Build_params 3 K.
Variable HP : fparamsProp Pp.

Section Generic.

Implementation of tuple vars 
Variable tvar : Type.
Variable tvcompare : tvar -> tvar -> comparison.

Variable tvarn : tvar -> nat.
Hypothesis tvcompare_inj : forall v1 v2,
  tvarn v1 = tvarn v2 -> v1 = v2.
Hypothesis tvcompare_def : forall v1 v2,
  tvcompare v1 v2 = natc (tvarn v1) (tvarn v2).

Lemma tvcompare_eq v1 v2 :
  match tvcompare v1 v2 with Eq => v1 = v2 | _ => v1 <> v2 end.

Lemma tvcompare_refl v : tvcompare v v = Eq.

Proof 
Variable interv : tvar -> point K.
Notation "{v[ x ]}" := (interv x).

Variable var : Type.
Variable coef : Type.
Variable cadd : coef -> coef -> coef.
Variable czerop : coef -> bool.
Variable czero : coef.
Variable conep : coef -> bool.
Variable cone : coef.
Variable copp : coef -> coef.
Variable cscale : var -> coef -> coef.

Variable interk : var -> K.
Notation "{k[ x ]}" := (interk x).
Variable interc : coef -> K.
Notation "{c[ x ]}" := (interc x).
Hypothesis cadd_c : forall x y, {c[cadd x y]} = ({c[x]} + {c[y]})%f.
Hypothesis cone_c : {c[cone]} = (1)%f.
Hypothesis conep_c : forall x,
  if conep x then {c[x]} = (1)%f else True.
Hypothesis czero_c : {c[czero]} = (0)%f.
Hypothesis cscale_c : forall k x,
  {c[cscale k x]} = ({k[k]} * {c[x]})%f.
Hypothesis czerop_c : forall x,
  if czerop x then {c[x]} = (0)%f else True.
Hypothesis copp_c : forall x, {c[copp x]} = (- {c[x]})%f.

We want to reduce expression 
Inductive tuple := Tuple (_ _ _: tvar).
Let line := list tuple.
Let expr := list (coef * line).

Definition intert (t : tuple) :=
  let (p1,p2,p3) := t in '[{v[p1]},{v[p2]},{v[p3]}].
Notation "{t[ x ]}" := (intert x).

Fixpoint interl (l :line) :=
  match l with nil => 1%f | t ::l1 => ({t[t]} * interl l1)%f end.
Notation "{l[ x ]}" := (interl x).

Fixpoint intere (e :expr) :=
  match e with nil => 0%f | (c,l)::e1 =>
  ({c[c]} * {l[l]} + intere e1)%f
  end.
Notation "{e[ x ]}" := (intere x).

Fixpoint intere1 (e :expr) :=
  match e with nil => 0%f | (c,t ::nil)::nil =>
    if conep c then {t[t]} else intere e
  | _ => intere e end.
Notation "{e1[ x ]}" := (intere1 x).

Lemma intere1_c e : {e1[e]} = {e[e]}.

Sign 
Inductive sign := Sm1 | S0 | S1.
Definition sopp s := match s with Sm1 => S1 | S0 => S0 | S1 => Sm1 end.
Definition smult s1 s2 :=
  match s1 with S0 => S0 | S1 => s2 | Sm1 => sopp s2 end.
Definition smult3 s1 s2 s3 :=
  match s1 with S0 => S0
 | S1 => smult s2 s3
 | Sm1 => sopp (smult s2 s3) end.

Membership 
Definition tin i (t : tuple) :=
  let (j1,j2,j3) := t in
  match tvcompare i j1 with Eq => true
  | _ => match tvcompare i j2 with Eq => true
  | _ => match tvcompare i j3 with Eq => true
  | _ => false end end end.

Lemma tin_correct i1 i j k :
  if tin i1 (Tuple i j k) then
        i1=i \/ i1 = j \/ i1 = k
  else
        i1<>i /\ i1 <> j /\ i1 <> k.

Substitution 
Definition tsubst i j (t : tuple) :=
  let (i1,i2,i3) := t in
  match tvcompare i i1 with
  | Eq => Tuple j i2 i3
  | _ =>
      match tvcompare i i2 with
     | Eq => Tuple i1 j i3
     | _ =>
         match tvcompare i i3 with
         | Eq => Tuple i1 i2 j
         | _ => t
         end
     end
  end.

Definition s2k (s: sign) : K :=
  match s with S0 => 0%f | S1 => 1%f | Sm1 => (-(1))%f end.

Lemma tsubst_c i t :
  if tin i t then exists a, exists b, exists s,
  ({t[t]} = s2k s * {t[Tuple i a b]} /\
   forall j, {t[tsubst i j t]} = s2k s * {t[Tuple j a b]})%f else True.

Add an element in a tuple  i1 [? i2 i3] 
Definition mk_tuplel i1 i2 i3 :=
match tvcompare i1 i2 with
| Eq => (S0, Tuple i1 i2 i3)
| Lt => (S1, Tuple i1 i2 i3)
| Gt =>
  match tvcompare i1 i3 with
  | Eq => ( S0, Tuple i1 i2 i3)
  | Lt => (Sm1, Tuple i2 i1 i3)
  | Gt => ( S1, Tuple i2 i3 i1)
  end
end.

Lemma mk_tuplel_c i1 i2 i3 :
 let (s,t1) := mk_tuplel i1 i2 i3 in
 {t[Tuple i1 i2 i3]} = (s2k s * {t[t1]})%f.

Add an element in a tuple  [i1 i2 ?] i3 
Definition mk_tupler i1 i2 i3 :=
match tvcompare i2 i3 with
| Eq => (S0, Tuple i1 i2 i3)
| Lt => (S1, Tuple i1 i2 i3)
| Gt =>
  match tvcompare i1 i3 with
  | Eq => ( S0, Tuple i1 i2 i3)
  | Lt => (Sm1, Tuple i1 i3 i2)
  | Gt => ( S1, Tuple i3 i1 i2)
  end
end.

Lemma mk_tupler_c i1 i2 i3 :
 let (s,t1) := mk_tupler i1 i2 i3 in
 {t[Tuple i1 i2 i3]} = (s2k s * {t[t1]})%f.

Inductive sprod := SProd (s : sign) (t1 t2 : tuple).

Definition esprod (s : sprod) :=
  let (s,t1,t2) := s in (s2k s * {t[t1]} * {t[t2]})%f.

Definition elsprod (l : list sprod) :=
  fold_left (fun res s => (res + esprod s)%f) l 0%f.

Definition tsplit3 (i1 i2 i3 j1 j2 j3 : tvar) :=
  match tvcompare i2 j2 with
  | Gt =>
     
     let (s1,t1) := mk_tuplel i1 j1 j2 in
     let (s'1,t'1) := mk_tupler i2 i3 j3 in
     let (s2,t2) := mk_tuplel i1 j1 j3 in
     let (s'2,t'2) := mk_tupler i2 i3 j2 in
     let (s3,t3) := mk_tuplel i1 j2 j3 in
     let (s'3,t'3) := mk_tupler i2 i3 j1 in
       SProd (smult s1 s'1) t1 t'1 ::
       SProd (sopp (smult s2 s'2)) t2 t'2 ::
       SProd (smult s3 s'3) t3 t'3 :: nil
  | _ =>
    match tvcompare i3 j3 with
    | Gt =>
        
       let (s1,t1) := mk_tupler i1 i2 j1 in
       let (s'1,t'1) := mk_tuplel i3 j2 j3 in
       let (s2,t2) := mk_tupler i1 i2 j2 in
       let (s'2,t'2) := mk_tuplel i3 j1 j3 in
       let (s3,t3) := mk_tupler i1 i2 j3 in
       let (s'3,t'3) := mk_tuplel i3 j1 j2 in
         SProd (smult s1 s'1) t1 t'1 ::
         SProd (sopp (smult s2 s'2)) t2 t'2 ::
         SProd (smult s3 s'3) t3 t'3 :: nil
    | _ => SProd S1 (Tuple i1 i2 i3) (Tuple j1 j2 j3)::nil
    end
  end.

Lemma s2km m1 m2 : s2k (smult m1 m2) = (s2k m1 * s2k m2)%f.

Lemma s2ko m : s2k (sopp m) = ((-(1)) * s2k m)%f.

Lemma tsplit3_c a b c d e f :
    ({t[Tuple a b c]} * {t[Tuple d e f]})%f =
         elsprod (tsplit3 a b c d e f).

Definition tsplit (t1 t2 : tuple) :=
Eval lazy beta delta [tsplit3] in
  let (i1,i2,i3) := t1 in
  let (j1,j2,j3) := t2 in
  match tvcompare i1 j1 with
  | Gt => SProd S1 t2 t1 :: nil
  | _ => tsplit3 i1 i2 i3 j1 j2 j3
  end.

Lemma tsplit_c t1 t2 :
    ({t[t1]} * {t[t2]})%f = elsprod (tsplit t1 t2).

Lexicographic comparison 
Fixpoint list_compare (T : Type) (cmp : T -> T -> comparison)
                                 (l1 l2 : list T) :=
match l1, l2 with
| nil, nil => Eq
| nil, _ => Lt
| _, nil => Gt
| a::l1, b::l2 => match cmp a b with
                  | Eq => list_compare T cmp l1 l2
                  | res => res
                  end
end.

Lemma list_compare_eq T cmp l1 l2 :
  (forall c1 c2, match cmp c1 c2 with Eq => c1 = c2 | _ => True end) ->
  match list_compare T cmp l1 l2 with Eq => l1 = l2 | _ => True end.

Definition tcompare (t1 t2 : tuple) :=
  let (i1, i2, i3) := t1 in
  let (j1, j2, j3) := t2 in
  match tvcompare i1 j1 with
  | Eq =>
    match tvcompare i2 j2 with
    | Eq => tvcompare i3 j3
    | r => r
    end
  | r => r
  end.

Lemma tcompare_eq t1 t2 :
  match tcompare t1 t2 with Eq => t1 = t2 | _ => True end.

Definition lcompare : line -> line -> _ := list_compare _ tcompare.
Lemma lcompare_eq l1 l2 :
  match lcompare l1 l2 with Eq => l1 = l2 | _ => True end.

Definition ecompare : expr -> expr -> _ := list_compare _ (fun x y => lcompare (snd x) (snd y)).

Lexicographic comparison 

Definition tsort (t : tuple) :=
  let (i1, i2, i3) := t in
  match tvcompare i1 i2 with
  | Eq => (S0, t)
  | Lt => match tvcompare i2 i3 with
          | Eq => ( S0, t)
          | Lt => ( S1, t)
          | Gt =>
              match tvcompare i1 i3 with
              | Eq => ( S0, t)
              | Lt => (Sm1, Tuple i1 i3 i2)
              | Gt => ( S1, Tuple i3 i1 i2)
              end
          end
  | Gt => match tvcompare i1 i3 with
          | Eq => ( S0, t)
          | Lt => (Sm1, Tuple i2 i1 i3)
          | Gt =>
              match tvcompare i2 i3 with
              | Eq => ( S0, t)
              | Lt => ( S1, Tuple i2 i3 i1)
              | Gt => (Sm1, Tuple i3 i2 i1)
              end
          end
  end.

Lemma tsort_c t :
  let (s,t1) := tsort t in {t[t]} = (s2k s * {t[t1]})%f.

Fixpoint linsert (t1 : tuple) (l : line) :=
match l with
| nil => t1 :: l
| t2::l1 => match tcompare t1 t2 with
                  | Gt => t2 :: linsert t1 l1
                  | res => t1 :: l
                  end
end.

Lemma linsert_length t l : length (linsert t l) = S (length l).

Lemma linsert_c t l : {l[linsert t l]} = ({t[t]} * {l[l]})%f.

Fixpoint lsort (l : line) :=
match l with
| nil => l
| t ::l1 => linsert t (lsort l1)
end.

Lemma lsort_c l : {l[lsort l]} = {l[l]}.

Fixpoint ltsort (c : sign) (l : line) :=
match l with
| nil => (c,l)
| t ::l1 => let (c1,t1) := tsort t in
            let (c2,l2) := ltsort (smult c1 c) l1 in
            (c2, linsert t1 l2)
end.

Lemma ltsort_c c l :
  let (s,l1) := ltsort c l in
  (s2k s * {l[l1]})%f = (s2k c * {l[l]})%f.

Fixpoint einsert (c1 : coef) (l1 : line) (e : expr) :=
match e with
| nil => (c1,l1) :: e
| (c2,l2)::e1 => match lcompare l1 l2 with
                  | Eq => let c := cadd c1 c2 in
                          if czerop c then e1 else (c,l1)::e1
                  | Gt => (c2,l2) :: einsert c1 l1 e1
                  | Lt => (c1,l1) :: e
                  end
end.

Lemma einsert_length c l e : length (einsert c l e) <= 1 + length e.

Lemma einsert_c c1 l1 e :
  {e[einsert c1 l1 e]} = ({c[c1]} * {l[l1]} + {e[e]})%f.

Definition scmp (s : sign) (c : coef) :=
  match s with S0 => czero | S1 => c | Sm1 => copp c end.

Lemma scmp_c s c :
 {c[scmp s c]} = (s2k s * {c[c]})%f.

Definition einsert0 (c1 : coef) (l1 : line) (e : expr) :=
  if czerop c1 then e else einsert c1 l1 e.

Lemma einsert0_c c1 l1 e :
  {e[einsert0 c1 l1 e]} = ({c[c1]} * {l[l1]} + {e[e]})%f.

Fixpoint etsort (e : expr) :=
match e with
| nil => nil
| (c,l)::e1 => let (c1, l1) := ltsort S1 l in
          einsert0 (scmp c1 c) l1 (etsort e1)
end.

Lemma etsort_c e : {e[etsort e]} = {e[e]}.

Reverse a tuple in a tail recursive way 
Fixpoint rev (T : Type) (t1 t2 : list T) :=
  match t1 with nil => t2 | n1 :: t3 => rev _ t3 (n1 :: t2) end.
Definition lrev: line -> line -> _ := rev tuple.
Lemma lrev_c l1 l2 :
 {l[lrev l1 l2]} = ({l[l1]} * {l[l2]})%f.

Fixpoint iter_split (c1 : coef) (l l1 : line) (accu : line) (e : expr)
   : expr :=
  if czerop c1 then e else
  match l with
  | nil => einsert c1 (lrev accu nil) e
  | _ :: l' =>
    match l1 with
    | nil => einsert c1 (lrev accu nil) e
    | t1 ::nil => einsert c1 (lrev accu (t1 ::nil)) e
    | t1 :: t2 :: l2 =>
       fold_left (fun e (v: sprod) =>
                   let (s1, t1, t2) := v in
                   let l3 := linsert t2 l2 in
                     iter_split (scmp s1 c1) l' l3 (t1 ::accu) e)
                  (tsplit t1 t2) e
    end
  end.

Lemma iter_split_c c1 l l1 accu e :
 length l1 <= length l ->
 {e[iter_split c1 l l1 accu e]} =
    ({c[c1]} * {l[lrev accu l1]} + {e[e]})%f.

Definition step (e : expr) : expr :=
  fold_left (fun e l => match l with
                        | (c, l1) => iter_split c l1 l1 nil e
                        end
             ) e nil.
Lemma step_c e : {e[step e]} = {e[e]}.

Inductive rp (T : Type) := Stop (_ : T) | More (_ : T).
Definition rp_val (T : Type) (x : rp T) :=
match x with Stop y => y | More y => y end.

Fixpoint iter_rp (T : Type) n f (v : rp T) := match v with
| More r => match n with
            | O => f r
            | S n1 => iter_rp T n1 f (iter_rp T n1 f v)
            end
| _ => v
end.

Definition iter_step (k : nat) (e : expr) :=
  iter_rp _ k (fun e => let e1 := step e in
                         match ecompare e e1 with
                          Eq => @Stop _ e
                         | _ => More _ e1
                         end) (More _ e).

Lemma iter_step_c k e : {e[rp_val _ (iter_step k e)]} = {e[e]}.

Elimination of an intersection from a line 
Fixpoint inter_elim (cc : coef) (x a b c d: tvar) (l : list tuple)
               (accu: list tuple) e : expr :=
  match l with
  | nil => einsert cc (rev _ accu l) e
  | t :: l1 =>
     if tin x t then
     let (c1,t1) := tsort (tsubst x a t) in
     let (c2,t2) := tsort (Tuple b c d) in
     let (c3,t3) := tsort (tsubst x b t) in
     let (c4,t4) := tsort (Tuple a c d) in
     einsert0
       (scmp (sopp (smult c1 c2)) cc)
         (linsert t1 (linsert t2 (rev _ accu l1)))
     (einsert0
       (scmp (smult c3 c4) cc)
         (linsert t3 (linsert t4 (rev _ accu l1)))
          e)
     else inter_elim cc x a b c d l1 (t ::accu) e
end.

Lemma inter_elim_c cc x a b c d l accu e :
 {v[x]} = ({v[a]} ∨ {v[b]}) ∧({v[c]} ∨ {v[d]}) :> vect K ->
 {e[inter_elim cc x a b c d l accu e]} =
  ({c[cc]} * {l[l]} * {l[accu]} + {e[e]})%f.

Fixpoint ielim (x a b c d: tvar) e accu :=
  match e with
  | nil => accu
  | (cc,l) :: e1 =>
       ielim x a b c d e1
         (inter_elim cc x a b c d l nil accu)
  end.

Lemma ielim_c x a b c d e accu:
 {v[x]} = ({v[a]} ∨ {v[b]}) ∧({v[c]} ∨ {v[d]}) :> vect K ->
 {e[ielim x a b c d e accu]} = ({e[accu]} + {e[e]})%f.

Definition nielim x a b c d e :=
  ielim x a b c d e nil.

Lemma nielim_c x a b c d e :
 {v[x]} = ({v[a]} ∨ {v[b]}) ∧({v[c]} ∨ {v[d]}) :> vect K ->
 {e[nielim x a b c d e]} = {e[e]}.

Definition do_elim x a b c d (e : expr) :=
  let e1 := nielim x a b c d e in
  match ecompare e e1 with
  | Eq => Stop _ e1
  | _ => More _ e1
  end.

Lemma do_elim_c x a b c d e :
 {v[x]} = ({v[a]} ∨ {v[b]}) ∧ ({v[c]} ∨ {v[d]}) :> vect K ->
  {e[rp_val _ (do_elim x a b c d e)]} = {e[e]}.

Definition iter_elim n x a b c d e :=
  iter_rp _ n (do_elim x a b c d) (More _ e).

Lemma iter_elim_c n x a b c d e :
 {v[x]} = ({v[a]} ∨ {v[b]}) ∧ ({v[c]} ∨ {v[d]}) :> vect K ->
  {e[rp_val _ (iter_elim n x a b c d e)]} = {e[e]}.

Elimination of a semi-free point 
Fixpoint free_elim (cc : coef) x a b c d (l : list tuple)
               (accu: list tuple) e :=
  match l with
  | nil => einsert cc (rev _ accu l) e
  | t ::l1 =>
     if tin x t then
     let (c1,t1) := tsort (tsubst x b t) in
     let cc1 := cscale a (scmp c1 cc) in
     let (c2,t2) := tsort (tsubst x d t) in
     let cc2 := cscale c (scmp c2 cc) in
     einsert0
       cc1 (linsert t1 (rev _ accu l1))
     (einsert0
       cc2 (linsert t2 (rev _ accu l1))
          e)
     else free_elim cc x a b c d l1 (t ::accu) e
end.

Lemma free_elim_c cc x a b c d l accu e :
 {v[x]} = {k[a]} .* {v[b]} + {k[c]} .* {v[d]} :> vect K ->
 {e[free_elim cc x a b c d l accu e]} =
   ({c[cc]} * {l[l]} * {l[accu]} + {e[e]})%f.

Fixpoint felim x a b c d e accu :=
  match e with
  | nil => accu
  | (cc,l)::e1 =>
       felim x a b c d e1
         (free_elim cc x a b c d l nil accu)
  end.

Lemma felim_c x a b c d e accu :
 {v[x]} = {k[a]} .* {v[b]} + {k[c]} .* {v[d]} :> vect K ->
 {e[felim x a b c d e accu]} = ({e[accu]} + {e[e]})%f.

Definition nfelim x a b c d e :=
  felim x a b c d e nil.

Lemma nfelim_c x a b c d e :
 {v[x]} = {k[a]} .* {v[b]} + {k[c]} .* {v[d]} :> vect K ->
 {e[nfelim x a b c d e]} = {e[e]}.

Definition do_free x a b c d (e : expr) :=
  let e1 := nfelim x a b c d e in
  match ecompare e e1 with
  | Eq => Stop _ e1
  | _ => More _ e1
  end.

Lemma do_free_c x a b c d e :
 {v[x]} = {k[a]} .* {v[b]} + {k[c]} .* {v[d]} :> vect K ->
  {e[rp_val _ (do_free x a b c d e)]} = {e[e]}.

Definition iter_free n x a b c d e :=
  iter_rp _ n (do_free x a b c d) (More _ e).

Lemma iter_free_c n x a b c d e :
 {v[x]} = {k[a]} .* {v[b]} + {k[c]} .* {v[d]} :> vect K ->
  {e[rp_val _ (iter_free n x a b c d e)]} = {e[e]}.




Implementation of contraction

Definition reorder (t1 t2 : tuple) :=
 let (m1,m2,m3) := t1 in
 let (n1,n2,n3) := t2 in
 match tvcompare m1 n1 with
 | Eq =>
      match tvcompare m2 n2 with
     | Eq => match tvcompare m3 n3 with
             |Eq => None
             | _ => Some (S1, S1, m1, m2, m3, n3)
             end
     | Lt =>
          match tvcompare m3 n2 with
          | Eq => Some (Sm1, S1, m1, m3, m2, n3)
          | Lt => None
          | Gt =>
             match tvcompare m3 n3 with
             | Eq => Some (Sm1, Sm1, m1, m3, m2, n2)
             | _ => None
             end
           end
     | Gt =>
          match tvcompare m2 n3 with
          | Eq => Some (S1, Sm1, m1, m2, m3, n2)
          | Gt => None
          | Lt =>
             match tvcompare m3 n3 with
             | Eq => Some (Sm1, Sm1, m1, m3, m2, n2)
             | _ => None
             end
          end
      end
 | Lt =>
      match tvcompare m2 n1 with
     | Eq =>
          match tvcompare m3 n2 with
          | Eq => Some (S1, S1, m2, m3, m1, n3)
          | Lt => None
          | Gt =>
             match tvcompare m3 n3 with
             | Eq => Some (S1, Sm1, m2, m3, m1, n2)
             | _ => None
             end
          end
     | Lt => None
     | Gt =>
          match tvcompare m2 n2 with
          | Eq =>
             match tvcompare m3 n3 with
             | Eq => Some (S1, S1, m2, m3, m1, n1)
             | _ => None
             end
          | _ => None
          end
      end
 | Gt =>
      match tvcompare m1 n2 with
     | Eq =>
          match tvcompare m2 n3 with
          | Eq => Some (S1, S1, m1, m2, m3, n1)
          | Gt => None
          | Lt =>
             match tvcompare m3 n3 with
             | Eq => Some (Sm1, S1, m1, m3, m2, n1)
             | _ => None
             end
          end
     | Gt => None
     | Lt =>
          match tvcompare m2 n2 with
          | Eq =>
             match tvcompare m3 n3 with
             | Eq => Some (S1, S1, m2, m3, m1, n1)
             | _ => None
             end
          | _ => None
          end
      end
  end.

Lemma reorder_c t1 t2 :
  match reorder t1 t2 with None => True | Some (s1, s2, m1,m2,m3,m4) =>
  ({t[t1]} = s2k s1 * {t[Tuple m1 m2 m3]} /\
   {t[t2]} = s2k s2 * {t[Tuple m1 m2 m4]})%f
  end.

Definition contraction_rule c t1 t2 t3 t4 :=
  match reorder t1 t2 with
  | None => None
  | Some (s1, s2, m1, m2, m3, m4) =>
  match reorder t3 t4 with
  | None => None
  | Some (s3, s4, n1, n2, n3, n4) =>
  let s1 := smult s1 s3 in
  let s2 := smult c (smult s2 s4) in
  match smult s1 s2 with
  | S0 => None | S1 => None
  | Sm1 =>
  match tvcompare m3 n4 with
  | Lt => None | Gt => None
  | Eq =>
  match tvcompare m4 n3 with
  | Lt => None | Gt => None
  | Eq =>
  match tvcompare m1 n1 with
  | Eq =>
           let (s3,t3) := tsort (Tuple m1 m2 n2) in
           let (s4,t4) := tsort (Tuple m1 m3 m4) in
           Some (smult s1 (smult s3 s4), t3, t4)
  | Lt => match tvcompare m2 n1 with
          | Eq =>
             
           let (s3,t3) := tsort (Tuple m1 m2 n2) in
           let (s4,t4) := tsort (Tuple m2 m3 m4) in
           Some (smult s1 (smult s3 s4), t3, t4)
          | Lt => None
          | Gt =>
             match tvcompare m2 n2 with
             | Eq =>
               
             let (s3,t3) := tsort (Tuple m2 m1 n1) in
             let (s4,t4) := tsort (Tuple m2 m3 m4) in
             Some (smult s1 (smult s3 s4), t3, t4)
             | _ => None
             end
          end
  | Gt => match tvcompare m1 n2 with
          | Eq =>
             
             let (s3,t3) := tsort (Tuple m1 m2 n1) in
             let (s4,t4) := tsort (Tuple m3 m1 m4) in
             Some (smult s1 (smult s3 s4), t3, t4)
          | Gt => None
          | Lt =>
             match tvcompare m2 n2 with
             | Eq =>
               
               let (s3,t3) := tsort (Tuple m2 m1 n1) in
               let (s4,t4) := tsort (Tuple m2 m3 m4) in
               Some (smult s1 (smult s3 s4), t3, t4)
             | _ => None
             end
          end
  end end end end end end.

Lemma contraction_rule_c c t1 t2 t3 t4 :
  match contraction_rule c t1 t2 t3 t4 with
  | None => True
  | Some (s, t5, t6) =>
    ({t[t1]} * {t[t3]} + s2k c * ({t[t2]} * {t[t4]}) =
      s2k s * {t[t5]} * {t[t6]})%f
  end.

Fixpoint delta (m n : nat) (l1 l2 al1 al2 al3: line) :
  option (line * line * line) :=
  match l1 with
  | nil => match natc n (length l2) with
          | Eq => Some (lrev al1 nil, lrev al2 l2, lrev al3 nil)
          | _ => None
          end
  | t1 :: l3 =>
      (fix delta1 n (l2 : list tuple) al2 :=
        match l2 with
        | nil =>
           match natc m (length l1) with
           | Eq => Some (lrev al1 l1, lrev al2 nil, lrev al3 nil)
           | _ => None
           end
        | t2 :: l4 =>
            match tcompare t1 t2 with
            | Eq => delta m n l3 l4 al1 al2 (t1 ::al3)
            | Lt => match m with
                    | O => None
                    | S m1 => delta m1 n l3 l2 (t1 ::al1) al2 al3
                    end
            | Gt => match n with
                    | O => None
                    | S n1 => delta1 n1 l4 (t2 ::al2)
                    end
            end
        end) n l2 al2
  end.

Lemma delta_c m n l1 l2 al1 al2 al3 :
  match delta m n l1 l2 al1 al2 al3 with
  | None => True
  | Some (l3,l4,l5) =>
      ({l[l1]} * {l[al1]} * {l[al3]} = {l[l3]} * {l[l5]} /\
       {l[l2]} * {l[al2]} * {l[al3]} = {l[l4]} * {l[l5]})%f
  end.

Fixpoint has_delta (c : coef) (l : line) (e : expr) :=
  match e with
  | nil => None
  | (c1,l1)::e1 =>
     match delta 2 2 l l1 nil nil nil with
     | Some (t1 :: t2 :: nil, t3 :: t4 :: nil, rl) =>
       let s :=
          if czerop (cadd c c1) then Sm1 else
          if czerop (cadd c (copp c1)) then S1 else
          S0 in
       if match s with S0 => true | _ => false end then
         has_delta c l e1
       else
         match contraction_rule s t1 t3 t2 t4 with
         | None=> has_delta c l e1
         | Some (c5, t5, t6) =>
               Some ((c1,l1),
                   (scmp c5 c,
                     linsert t5 (linsert t6 rl)))
         end
     | _ => has_delta c l e1
     end
  end.

Lemma has_delta_in c l e :
  match has_delta c l e with None => True | Some (p,_) => In p e end.

Lemma has_delta_c c l e :
  match has_delta c l e with None => True | Some ((c1,l1),(c2,l2)) =>
  ({c[c]} * {l[l]} + {c[c1]} * {l[l1]} = {c[c2]} * {l[l2]})%f
  end.

Fixpoint edelta (e : expr) :=
  match e with
  | nil => None
  | (c,l) :: e1 =>
     match has_delta c l e1 with
     | None => edelta e1
     | Some r => Some ((c,l), r) end
  end.

Lemma edelta_in e :
  match edelta e with None => True | Some (p,(p1,_)) =>
     In p e /\ In p1 e end.

Lemma edelta_c e :
  match edelta e with None => True | Some ((c,l),((c1,l1),(c2,l2))) =>
  ({c[c]} * {l[l]} + {c[c1]} * {l[l1]} = {c[c2]} * {l[l2]})%f
  end.

Fixpoint eremove c l (e : expr) :=
  match e with
  | nil => None
  | (c1,l1) :: e1 =>
       if czerop (cadd c1 (copp c)) then
       match lcompare l l1 with
       | Eq => Some e1
       | _ =>
          match eremove c l e1 with
          | Some e2 => Some ((c1,l1):: e2)
          | _ => None
          end
       end
       else
          match eremove c l e1 with
          | Some e2 => Some ((c1,l1):: e2)
          | _ => None
          end
  end.

Lemma eremove_c c l e :
  match eremove c l e with None => True | Some e1 =>
  {e[e1]} = ({e[e]} + (-(1)) * {c[c]} * {l[l]})%f
  end.

Definition do_contra (e : expr) :=
  match edelta e with
  | None => Stop _ e
  | Some ((c1,l1),((c2,l2),(c3,l3))) =>
     match eremove c2 l2 e with
     | Some e1 =>
       match eremove c1 l1 e1 with
       | Some e2 =>
           More _ (einsert c3 l3 e2)
       | _ => Stop _ e
       end
     | _ => Stop _ e
    end
  end.

Lemma do_contra_c e :
  {e[rp_val _ (do_contra e)]} = {e[e]}.

Definition iter_contra n e := iter_rp _ n do_contra (More _ e).

Lemma iter_contra_c n e :
  {e[rp_val _ (iter_contra n e)]} = {e[e]}.

Inductive action :=
  Inter (_ _ _ _ _: tvar)
| SFree (_:tvar) (_:var) (_: tvar) (_:var) (_: tvar).

Definition intera (a: action): Prop :=
  match a with
  | Inter x a b c d =>
       {v[x]} = ({v[a]} ∨ {v[b]}) ∧ ({v[c]} ∨ {v[d]}) :> vect K
  | SFree x a b c d =>
       {v[x]} = {k[a]} .* {v[b]} + {k[c]} .* {v[d]} :> vect K
  end.

Fixpoint interla (l : list action) (c : Prop) : Prop :=
  match l with
  | nil => c
  | a :: l1 => intera a -> interla l1 c
  end.

Definition interla_refine (c1 c2 : Prop) l :
  (c1 -> c2) -> (interla l c1 -> interla l c2).

Fixpoint resolve l e :=
  match l with
  | nil => e
  | (Inter x a b c d)::l1 =>
      rp_val _ (iter_elim 10 x a b c d (resolve l1 e))
  | (SFree x a b c d)::l1 =>
      rp_val _ (iter_free 10 x a b c d (resolve l1 e))
  end.

Lemma resolve_c l e : interla l ({e[e]} = {e[resolve l e]}).

Definition do_auto n l e :=
  let e1 := resolve l e in
  let e2 := rp_val _ (iter_contra 10 e1) in
  rp_val _ (iter_step n e2).

Lemma do_auto_c n l e :
  interla l ({e1[e]} = {e1[do_auto n l e]}).

End Generic.

Require Import ZArith.

Notation "'{' a ',' b ',' c '}'" := (Tuple _ a b c).

Section NatImplem.

 tvar -> nat 
Definition tvar := nat.
Definition tvcompare : tvar -> tvar -> comparison := natc.
Definition tvarn : tvar -> nat := id.
Lemma tvcompare_inj v1 v2 : tvarn v1 = tvarn v2 -> v1 = v2.
Lemma tvcompare_def v1 v2 :
  tvcompare v1 v2 = natc (tvarn v1) (tvarn v2).


Definition var := nat.
Variable interk : var -> K.
Notation "{k[ x ]}" := (interk x).

Definition term := (Z * (list var))%type.

Definition intervs (l : list var) : K :=
  (fold_left (fun res v => res * {k[v]}) l 1)%f.
Notation "{vs[ x ]}" := (intervs x).

Lemma intervs_nil : {vs[nil]} = 1%f.

Lemma intervs_cons v l : {vs[v::l]} = ({k[v]} * {vs[l]})%f.
Definition interm (x : term): K :=
  let (z,l) := x in (Z_to_K _ z * {vs[l]})%f.
Notation "{m[ x ]}" := (interm x).

Definition term_add (t1 t2 : term) :=
  let (z1,l) := t1 in
  let (z2,_) := t2 in ((z1 + z2)%Z, l).

Definition term_cmp (t1 t2 : term) :=
  let (_,l1) := t1 in
  let (_,l2) := t2 in list_compare _ natc l1 l2.

Lemma term_add_c t1 t2 :
  match term_cmp t1 t2 with
  | Eq => {m[term_add t1 t2]} = ({m[t1]} + {m[t2]})%f
  | _ => True
  end.

Definition term_opp (t : term): term :=
  let (z,l) := t in ((-z)%Z, l).

Lemma term_opp_c t : {m[term_opp t]} = (-{m[t]})%f.

Fixpoint list_insert (i: nat) (l : list nat) :=
  match l with
  | nil => (i :: nil)
  | j :: l1 =>
      match natc j i with
      | Lt => j :: list_insert i l1
      | _ => i :: l
      end
   end.

Definition term_scale (v : nat) (t : term) : term :=
  let (z, l) := t in
  (z, list_insert v l).

Lemma term_scale_c v t :
  {m[term_scale v t]} = ({k[v]} * {m[t]})%f.

Definition term_zerop (t : term) :=
  let (z,l) := t in Zeq_bool 0%Z z.

Lemma term_zerop_c t : if term_zerop t then {m[t]} = 0%f else True.

Definition coef := list term.

Definition interc (c : coef) : K :=
 fold_left (fun res v => res + ({m[v]}))%f c 0%f.
Notation "{c[ x ]}" := (interc x).

Lemma interc_nil : {c[nil]} = 0%f.

Lemma interc_cons t c : {c[t ::c]} = ({m[t]} + {c[c]})%f.

Definition c0 : coef := nil.

Lemma c0_c : {c[c0]} = 0%f.

Definition c1 : coef := (1%Z,@nil var)::nil.

Lemma c1_c : {c[c1]} = 1%f.

Definition copp (c : coef) : coef := map term_opp c.

Lemma copp_c c : {c[copp c]} = (-{c[c]})%f.

Definition cscale (v : var) (c : coef) : coef :=
  map (term_scale v) c.

Lemma cscale_c v c :
  {c[cscale v c]} = ({k[v]} * {c[c]})%f.

Definition ccons (t : term) (c : coef) :=
  if term_zerop t then c else t :: c.

Lemma ccons_c t c : {c[ccons t c]} = ({m[t]} + {c[c]})%f.

Fixpoint cadd (a b : coef) : coef :=
  match a with
  | nil => b
  | t1 :: a1 =>
      (fix cadd1 (b : coef) : coef :=
        match b with
        | nil => a
        | t2 :: b1 =>
            match term_cmp t1 t2 with
            | Eq => ccons (term_add t1 t2) (cadd a1 b1)
            | Lt => ccons t1 (cadd a1 b)
            | Gt => ccons t2 (cadd1 b1)
            end
        end) b
  end.

Lemma cadd_c c1 c2 : {c[cadd c1 c2]} = ({c[c1]} + {c[c2]})%f.

Definition ccmp (c1 c2 : coef) :=
  list_compare _ term_cmp c1 c2.

Definition czerop (c : coef) :=
  match c with nil => true | _ => false end.

Lemma czerop_c c : if czerop c then {c[c]} = 0%f else True.

Definition conep (c : coef) :=
  match c with (Zpos xH,nil) :: nil => true | _ => false end.

Lemma conep_c c : if conep c then {c[c]} = 1%f else True.

Lemma natc_id n : natc n n = Eq.

Lemma list_compare_id l : list_compare _ natc l l = Eq.

Lemma cadd_opp a: cadd a (copp a) = nil.

Lemma czerop_opp a : czerop (cadd a (copp a)) = true.

Definition ndo_auto:= do_auto _ natc nat _ cadd czerop c0 copp cscale.

Definition ndo_auto_c i :=
  do_auto_c _ natc tvarn tvcompare_inj tvcompare_def i nat _
  cadd czerop c0 conep copp cscale interk interc cadd_c conep_c c0_c
  cscale_c czerop_c copp_c.

End NatImplem.

Code taken from Ring 

Inductive TBool : Set :=
 | RBtrue : TBool
 | RBfalse : TBool.

Ltac IN a l :=
 match l with
 | (cons a ?l) => constr:RBtrue
 | (cons _ ?l) => IN a l
 | nil => constr:RBfalse
 end.

Ltac AddFv a l :=
 match (IN a l) with
 | RBtrue => constr:l
 | _ => constr:(cons a l)
 end.

Ltac Find_at a l :=
 match l with
 | nil => constr:O
 | (cons a _) => constr:O
 | (cons _ ?l) => let p := Find_at a l in eval compute in (S p)
 end.

Ltac Cstl a l :=
  match l with (?l1,?l2) =>
   let l3 := AddFv a l1 in constr:(l3 , l2) end.

Ltac Cstr a l :=
  match l with (?l1,?l2) =>
   let l3 := AddFv a l2 in constr:(l1 , l3) end.

Ltac FV t fv :=
  match t with
  | (?t1 -> ?t2) =>
    let fv1 := FV t1 fv in let fv2 := FV t2 fv1 in constr:fv2
  | (bracket _ (p2v _ ?t1) (p2v _ ?t2) (p2v _ ?t3) = _) =>
    let fv1 := Cstl t1 fv in let fv2 := Cstl t2 fv1 in
    let fv3 := Cstl t3 fv2 in constr:fv3
  | (inter_lines _ ?t1 ?t2 ?t3 ?t4 ?t5) =>
    let fv1 := Cstl t1 fv in let fv2 := Cstl t2 fv1 in
    let fv3 := Cstl t3 fv2 in let fv4 := Cstl t4 fv3 in
    let fv5 := Cstl t5 fv4 in constr:fv5
  | (online1 _ ?t1 ?t2 ?t3 ?t4 ?t5) =>
    let fv1 := Cstl t1 fv in let fv2 := Cstr t2 fv1 in
    let fv3 := Cstl t3 fv2 in let fv4 := Cstr t4 fv3 in
    let fv5 := Cstl t5 fv4 in constr:fv5
  end.

Ltac GetHyp t fv1 fv2 :=
  match t with
  | (inter_lines _ ?t1 ?t2 ?t3 ?t4 ?t5) =>
    let n1 := Find_at t1 fv1 in let n2 := Find_at t2 fv1 in
    let n3 := Find_at t3 fv1 in let n4 := Find_at t4 fv1 in
    let n5 := Find_at t5 fv1 in constr:(Inter tvar var n1 n2 n3 n4 n5)
  | (online1 _ ?t1 ?t2 ?t3 ?t4 ?t5) =>
    let n1 := Find_at t1 fv1 in let n2 := Find_at t2 fv2 in
    let n3 := Find_at t3 fv1 in let n4 := Find_at t4 fv2 in
    let n5 := Find_at t5 fv1 in constr:(SFree tvar var n1 n2 n3 n4 n5)
  end.

Ltac GetHyps t fv1 fv2 :=
  match t with
  | (?t1 -> ?t2) =>
    let t1 := GetHyp t1 fv1 fv2 in
    let l1 := GetHyps t2 fv1 fv2 in constr:(t1 :: l1)
  | _ => constr:(@nil (action tvar var))
  end.

Ltac GetConcl t fv :=
  match t with
  | (?t1 -> ?t2) => GetConcl t2 fv
  | (bracket _ (p2v _ ?t1) (p2v _ ?t2) (p2v _ ?t3) = _) =>
    let n1 := Find_at t1 fv in let n2 := Find_at t2 fv in
    let n3 := Find_at t3 fv in
     constr:((c1,(Tuple tvar n1 n2 n3) :: nil) :: nil)
  end.

Ltac preProcess :=
intuition;
apply bracket0_collinear; auto;
repeat
match goal with H: (?H1 : Prop) |- _ =>
  match H1 with
  | (inter_lines _ _ _ _ _ _) =>
    generalize H; clear H
  | (online ?F ?t1 ?t2 ?t3) =>
      let k1 := fresh "k" in
      let k2 := fresh "k" in
      case (online_def F HP t1 t2 t3 H); intros (k1, k2);
      simpl fst; simpl snd; clear H
  | _ => clear H
  end
end.

Ltac doTac1 :=
match goal with |- ?H =>
  match FV H (nil : list (point K),nil : list K) with
  | (?fv1,?fv2) =>
    let concl := GetConcl H fv1 in
    let hyps := GetHyps H fv1 fv2 in
    set (cc := concl);
    set (hh := hyps)
  end
end.

Ltac doTac :=
match goal with |- ?H =>
  match FV H (nil : list (point K), nil : list K) with
  | (?fv1,?fv2) =>
    let concl := GetConcl H fv1 in
    let hyps := GetHyps H fv1 fv2 in
    generalize (ndo_auto_c (fun v => nth v fv2 0%f)
                           (fun v => nth v fv1 (0%f,(0%f,(0%f, tt))))
                            10 hyps concl);
    let ff := fresh "ff" in
    (set (ff := do_auto nat natc nat coef cadd czerop c0 copp cscale 10 hyps concl);
    vm_compute in ff;
    unfold ff;
    lazy zeta iota beta delta[interla intera c1 conep intere1 interl intert nth];
    let HH := fresh "HH" in
      intros HH; apply HH
    )
  end
end.

Ltac mTac := preProcess; doTac.

Section Examples.


Let ex1 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10: point K,
  p5 is_the_intersection_of [p1, p2] and [p3, p4] ->
  p6 is_the_intersection_of [p1, p3] and [p2, p4] ->
  p7 is_the_intersection_of [p2, p3] and [p1, p4] ->
  p8 is_the_intersection_of [p2, p3] and [p5, p6] ->
  p9 is_the_intersection_of [p2, p4] and [p5, p7] ->
 p10 is_the_intersection_of [p3, p4] and [p6, p7] ->
 [p8 , p9 , p10] are_collinear.

Lemma ex1_proof : ex1.
Let ex2 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10: point K,
 p5 is_the_intersection_of [p1,p2] and [p3,p4] ->
 p6 is_the_intersection_of [p1,p3] and [p2,p4] ->
 p7 is_the_intersection_of [p2,p3] and [p1,p4] ->
 p8 is_the_intersection_of [p1,p3] and [p5,p7] ->
 p9 is_the_intersection_of [p6,p7] and [p4,p8] ->
p10 is_the_intersection_of [p2,p4] and [p5,p7] ->
 [p3,p9,p10] are_collinear.

Print ex2.

Theorem ex2_proof : ex2.
Let ex3 := forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10: point K,
  p5 is_the_intersection_of [p1,p2] and [p3,p4] ->
  p6 is_the_intersection_of [p1,p3] and [p2,p4] ->
  p7 is_the_intersection_of [p2,p3] and [p1,p4] ->
  p8 is_the_intersection_of [p1,p3] and [p5,p7] ->
  p9 is_the_intersection_of [p1,p4] and [p5,p6] ->
 p10 is_the_intersection_of [p3,p4] and [p6,p7] ->
 [p8,p9,p10] are_collinear.

Print ex3.

Lemma ex3_proof : ex3.
Let ex4 := forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 : point K,
  p6 is_the_intersection_of [p1,p2] and [p3,p4] ->
  p7 is_the_intersection_of [p1,p3] and [p2,p4] ->
  p8 is_the_intersection_of [p2,p3] and [p1,p4] ->
  p9 is_the_intersection_of [p5,p6] and [p7,p8] ->
 p10 is_the_intersection_of [p5,p7] and [p6,p8] ->
 p11 is_the_intersection_of [p3,p9] and [p2,p10] ->
 p12 is_the_intersection_of [p6,p7] and [p5,p8] ->
 [p1,p11,p12] are_collinear.

Print ex4.

Lemma ex4_proof : ex4.
Let ex5 := forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13: point K,
  p6 is_the_intersection_of [p1,p3] and [p2,p4] ->
  p7 is_the_intersection_of [p2,p3] and [p5,p6] ->
  p8 is_the_intersection_of [p2,p5] and [p3,p4] ->
  p9 is_the_intersection_of [p1,p2] and [p6,p8] ->
 p10 is_the_intersection_of [p7,p9] and [p2,p4] ->
 p11 is_the_intersection_of [p3,p9] and [p6,p7] ->
 p12 is_the_intersection_of [p1,p5] and [p4,p11] ->
 p13 is_the_intersection_of [p2,p8] and [p3,p9] ->
 [p10,p12,p13] are_collinear.

Print ex5.

Lemma ex5_l : ex5.
Let ex6 := forall p1 p2 p3 p4 p5 p6 p7 p8 p9: point K,
  p5 is_free_on [p1,p2] ->
  p6 is_free_on [p3,p4] ->
  p7 is_the_intersection_of [p2,p3] and [p1,p4] ->
  p8 is_the_intersection_of [p3,p5] and [p1,p6] ->
  p9 is_the_intersection_of [p4,p5] and [p2,p6] ->
  [p7,p8,p9] are_collinear.

Print ex6.

Lemma ex6_proof : ex6.
Let ex7 := forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10: point K,
  p6 is_free_on [p1,p3] ->
  p7 is_the_intersection_of [p1,p2] and [p4,p5] ->
  p8 is_the_intersection_of [p1,p5] and [p2,p4] ->
  p9 is_the_intersection_of [p3,p8] and [p5,p6] ->
 p10 is_the_intersection_of [p2,p3] and [p4,p9] ->
 [p6,p7,p10] are_collinear.

Print ex7.

Definition ex7_proof : ex7.
Let ex8 := forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 : point K,
  p4 is_free_on [p1,p2] ->
  p5 is_free_on [p1,p2] ->
  p6 is_free_on [p1,p3] ->
  p7 is_free_on [p2,p3] ->
  p8 is_the_intersection_of [p2,p3] and [p4,p6] ->
  p9 is_the_intersection_of [p2,p3] and [p5,p6] ->
 p10 is_the_intersection_of [p1,p3] and [p5,p7] ->
 p11 is_the_intersection_of [p1,p3] and [p4,p7] ->
 p12 is_the_intersection_of [p1,p2] and [p8,p10] ->
 [p9,p11,p12] are_collinear.

Print ex8.

Lemma ex8_proof : ex8.
Let ex9_1 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15: point K,
  p5 is_free_on [p1,p2] ->
  p6 is_the_intersection_of [p1,p2] and [p3,p4] ->
  p7 is_the_intersection_of [p1,p3] and [p2,p4] ->
  p8 is_the_intersection_of [p2,p3] and [p1,p4] ->
  p9 is_the_intersection_of [p1,p3] and [p4,p5] ->
 p10 is_the_intersection_of [p2,p3] and [p4,p5] ->
 p11 is_the_intersection_of [p1,p4] and [p3,p5] ->
 p12 is_the_intersection_of [p2,p4] and [p3,p5] ->
 p13 is_the_intersection_of [p1,p2] and [p8,p9] ->
 p14 is_the_intersection_of [p1,p2] and [p7,p10] ->
 p15 is_the_intersection_of [p1,p2] and [p10,p11] ->
 [p7,p11,p13] are_collinear.

Print ex9_1.

Lemma ex9_proof1 : ex9_1.
Let ex9_2 :=
   forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15: point K,
  p5 is_free_on [p1,p2] ->
  p6 is_the_intersection_of [p1,p2] and [p3,p4] ->
  p7 is_the_intersection_of [p1,p3] and [p2,p4] ->
  p8 is_the_intersection_of [p2,p3] and [p1,p4] ->
  p9 is_the_intersection_of [p1,p3] and [p4,p5] ->
 p10 is_the_intersection_of [p2,p3] and [p4,p5] ->
 p11 is_the_intersection_of [p1,p4] and [p3,p5] ->
 p12 is_the_intersection_of [p2,p4] and [p3,p5] ->
 p13 is_the_intersection_of [p1,p2] and [p8,p9] ->
 p14 is_the_intersection_of [p1,p2] and [p7,p10] ->
 p15 is_the_intersection_of [p1,p2] and [p10,p11] ->
 [p8,p12,p14] are_collinear.

Print ex9_2.

Lemma ex9_proof2 : ex9_2.
Let ex9_3 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15: point K,
  p5 is_free_on [p1,p2] ->
  p6 is_the_intersection_of [p1,p2] and [p3,p4] ->
  p7 is_the_intersection_of [p1,p3] and [p2,p4] ->
  p8 is_the_intersection_of [p2,p3] and [p1,p4] ->
  p9 is_the_intersection_of [p1,p3] and [p4,p5] ->
 p10 is_the_intersection_of [p2,p3] and [p4,p5] ->
 p11 is_the_intersection_of [p1,p4] and [p3,p5] ->
 p12 is_the_intersection_of [p2,p4] and [p3,p5] ->
 p13 is_the_intersection_of [p1,p2] and [p8,p9] ->
 p14 is_the_intersection_of [p1,p2] and [p7,p10] ->
 p15 is_the_intersection_of [p1,p2] and [p10,p11] ->
  [p9,p12,p15] are_collinear.

Print ex9_3.

Lemma ex9_proof3 : ex9_3.
Let ex10_1 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13: point K,
  p5 is_free_on [p1,p2] ->
  p6 is_the_intersection_of [p1,p2] and [p3,p4] ->
  p7 is_the_intersection_of [p1,p3] and [p2,p4] ->
  p8 is_the_intersection_of [p1,p3] and [p4,p5] ->
  p9 is_the_intersection_of [p2,p3] and [p6,p7] ->
 p10 is_the_intersection_of [p2,p4] and [p1,p9] ->
 p11 is_the_intersection_of [p3,p4] and [p1,p9] ->
 p12 is_the_intersection_of [p2,p3] and [p8,p10] ->
 p13 is_the_intersection_of [p4,p9] and [p3,p10] ->
 [p5,p11,p12] are_collinear.

Print ex10_1.

Lemma ex10_proof1 : ex10_1.
Let ex10_2 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13: point K,
  p5 is_free_on [p1,p2] ->
  p6 is_the_intersection_of [p1,p2] and [p3,p4] ->
  p7 is_the_intersection_of [p1,p3] and [p2,p4] ->
  p8 is_the_intersection_of [p1,p3] and [p4,p5] ->
  p9 is_the_intersection_of [p2,p3] and [p6,p7] ->
 p10 is_the_intersection_of [p2,p4] and [p1,p9] ->
 p11 is_the_intersection_of [p3,p4] and [p1,p9] ->
 p12 is_the_intersection_of [p2,p3] and [p8,p10] ->
 p13 is_the_intersection_of [p4,p9] and [p3,p10] ->
 [p7,p11,p13] are_collinear.

Print ex10_2.

Lemma ex10_proof2 : ex10_2.
Let ex11 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13: point K,
  p5 is_free_on [p1,p2] ->
  p6 is_the_intersection_of [p1,p2] and [p3,p4] ->
  p7 is_the_intersection_of [p1,p3] and [p2,p4] ->
  p8 is_the_intersection_of [p2,p3] and [p1,p4] ->
  p9 is_the_intersection_of [p1,p3] and [p5,p8] ->
 p10 is_the_intersection_of [p2,p3] and [p6,p9] ->
 p11 is_the_intersection_of [p1,p2] and [p7,p10] ->
 p12 is_the_intersection_of [p1,p3] and [p8,p11] ->
 p13 is_the_intersection_of [p2,p3] and [p6,p12] ->
 [p5,p7,p13] are_collinear.

Print ex11.

Lemma ex11_proof : ex11.
Let ex12 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15
         p16 p17 p18 p19 p20 p21 p22 p23 p24 p25: point K,
 p10 is_free_on [p1,p9] ->
 p11 is_the_intersection_of [p1,p3] and [p2,p4] ->
 p12 is_the_intersection_of [p2,p4] and [p3,p5] ->
 p13 is_the_intersection_of [p3,p5] and [p4,p6] ->
 p14 is_the_intersection_of [p4,p6] and [p5,p7] ->
 p15 is_the_intersection_of [p5,p7] and [p6,p8] ->
 p16 is_the_intersection_of [p6,p8] and [p1,p7] ->
 p17 is_the_intersection_of [p1,p7] and [p2,p8] ->
 p18 is_the_intersection_of [p2,p8] and [p1,p3] ->
 p19 is_the_intersection_of [p2,p9] and [p10,p18] ->
 p20 is_the_intersection_of [p3,p9] and [p11,p19] ->
 p21 is_the_intersection_of [p4,p9] and [p12,p20] ->
 p22 is_the_intersection_of [p5,p9] and [p13,p21] ->
 p23 is_the_intersection_of [p6,p9] and [p14,p22] ->
 p24 is_the_intersection_of [p7,p9] and [p15,p23] ->
 p25 is_the_intersection_of [p8,p9] and [p16,p24] ->
 [p10,p17,p25] are_collinear.

Print ex12.

Lemma ex12_proof : ex12.
Let ex13 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15 p16: point K,
  p7 is_free_on [p1,p2] ->
  p8 is_the_intersection_of [p1,p3] and [p2,p4] ->
  p9 is_the_intersection_of [p2,p3] and [p1,p4] ->
 p10 is_the_intersection_of [p1,p5] and [p4,p6] ->
 p11 is_the_intersection_of [p3,p5] and [p1,p6] ->
 p12 is_the_intersection_of [p1,p3] and [p6,p7] ->
 p13 is_the_intersection_of [p1,p6] and [p9,p10] ->
 p14 is_the_intersection_of [p1,p5] and [p8,p11] ->
 p15 is_the_intersection_of [p1,p2] and [p12,p13] ->
 p16 is_the_intersection_of [p5,p7] and [p1,p4] ->
 [p14,p15,p16] are_collinear.

Print ex13.

Lemma ex13_proof : ex13.
Let ex14 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9: point K,
  p6 is_the_intersection_of [p1,p2] and [p3,p4] ->
  p7 is_the_intersection_of [p2,p4] and [p1,p5] ->
  p8 is_the_intersection_of [p1,p3] and [p4,p5] ->
  p9 is_the_intersection_of [p5,p6] and [p3,p7] ->
  [p2,p8,p9] are_collinear.

Print ex14.

Lemma ex14_proof : ex14.
Let ex15 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9: point K,
  p6 is_the_intersection_of [p2,p3] and [p1,p4] ->
  p7 is_the_intersection_of [p1,p2] and [p4,p5] ->
  p8 is_the_intersection_of [p3,p4] and [p2,p5] ->
  p9 is_the_intersection_of [p3,p7] and [p1,p8] ->
  [p5,p6,p9] are_collinear.

Print ex15.

Lemma ex15_proof : ex15.
Let ex16 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10: point K,
  p5 is_free_on [p2,p3] ->
  p6 is_the_intersection_of [p1,p2] and [p3,p4] ->
  p7 is_the_intersection_of [p1,p3] and [p2,p4] ->
  p8 is_the_intersection_of [p1,p5] and [p6,p7] ->
  p9 is_the_intersection_of [p4,p5] and [p6,p7] ->
 p10 is_the_intersection_of [p2,p3] and [p4,p8] ->
[p1,p9,p10] are_collinear.

Print ex16.

Lemma ex16_proof : ex16.
Let ex17 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 : point K,
  p9 is_free_on [p5,p8] ->
  p6 is_the_intersection_of [p1,p2] and [p3,p4] ->
  p7 is_the_intersection_of [p2,p3] and [p1,p4] ->
  p8 is_the_intersection_of [p6,p7] and [p1,p3] ->
  p9 is_the_intersection_of [p3,p4] and [p5,p8] ->
 p10 is_the_intersection_of [p7,p9] and [p5,p6] ->
 p11 is_the_intersection_of [p6,p9] and [p5,p7] ->
 p12 is_the_intersection_of [p6,p7] and [p2,p4] ->
 [p10,p11,p12] are_collinear.

Print ex17.

Lemma ex17_proof : ex17.
Let ex18 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14: point K,
  p7 is_free_on [p1,p2] ->
  p8 is_the_intersection_of [p2,p3] and [p5,p6] ->
  p9 is_the_intersection_of [p1,p3] and [p7,p8] ->
 p10 is_the_intersection_of [p1,p4] and [p7,p8] ->
 p11 is_the_intersection_of [p2,p4] and [p7,p8] ->
 p12 is_the_intersection_of [p3,p4] and [p7,p8] ->
 p13 is_the_intersection_of [p5,p7] and [p6,p9] ->
 p14 is_the_intersection_of [p5,p11] and [p6,p12] ->
 [p10,p13,p14] are_collinear.

Print ex18.

Lemma ex18_proof : ex18.
Let ex19 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 : point K,
  p6 is_free_on [p1,p2] ->
  p7 is_the_intersection_of [p1,p5] and [p3,p4] ->
  p8 is_the_intersection_of [p2,p7] and [p4,p6] ->
  p9 is_the_intersection_of [p5,p8] and [p2,p3] ->
 p10 is_the_intersection_of [p1,p9] and [p3,p4] ->
 p11 is_the_intersection_of [p3,p6] and [p1,p5] ->
 p12 is_the_intersection_of [p6,p9] and [p4,p5] ->
 [p10,p11,p12] are_collinear.

Print ex19.

Lemma ex19_proof : ex19.
Let ex20 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14: point K,
  p7 is_free_on [p1,p2] ->
  p8 is_free_on [p1,p3] ->
  p9 is_the_intersection_of [p1,p4] and [p5,p6] ->
 p10 is_the_intersection_of [p1,p5] and [p4,p6] ->
 p11 is_the_intersection_of [p3,p7] and [p2,p8] ->
 p12 is_the_intersection_of [p3,p4] and [p8,p9] ->
 p13 is_the_intersection_of [p2,p5] and [p7,p10] ->
 p14 is_the_intersection_of [p5,p8] and [p3,p10] ->
 [p11,p13,p14] are_collinear.

Print ex20.

Lemma ex20_proof : ex20.
Let ex21 :=
  forall p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13: point K,
  p5 is_free_on [p2,p3] ->
  p6 is_the_intersection_of [p1,p3] and [p2,p4] ->
  p7 is_the_intersection_of [p2,p3] and [p1,p4] ->
  p8 is_the_intersection_of [p3,p4] and [p6,p7] ->
  p9 is_free_on [p1,p2] ->
 p10 is_the_intersection_of [p5,p6] and [p1,p8] ->
 p11 is_the_intersection_of [p2,p8] and [p9,p10] ->
 p12 is_the_intersection_of [p7,p11] and [p1,p3] ->
 p13 is_the_intersection_of [p3,p9] and [p6,p7] ->
[p5,p12,p13] are_collinear.

Print ex21.

Definition ex21_proof : ex21.
End Examples.

End FF.