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.
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.
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.
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.
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]}.
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.
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.
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.
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.
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).
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)).
(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]}.
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]}.
(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]}.
(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.
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.