diff options
| -rw-r--r-- | plugins/nsatz/Nsatz.v | 64 | ||||
| -rw-r--r-- | plugins/nsatz/ideal.ml | 4 | ||||
| -rw-r--r-- | plugins/nsatz/nsatz.ml4 | 37 | ||||
| -rw-r--r-- | plugins/nsatz/polynom.ml | 3 | ||||
| -rw-r--r-- | test-suite/success/Nsatz.v | 533 |
5 files changed, 458 insertions, 183 deletions
diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 4f2010f29..6d5ea258b 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -28,6 +28,8 @@ Require Export Cring. Declare ML Module "nsatz_plugin". +(* Definition of integral domains: commutative ring without zero divisor *) + Class Integral_domain {R : Type}`{Rcr:Cring R} := { integral_domain_product: forall x y, x * y == 0 -> x == 0 \/ y == 0; @@ -278,19 +280,21 @@ Fixpoint interpret3 t fv {struct t}: R := End integral_domain. +Ltac equality_to_goal H x y:= + let h := fresh "nH" in + (assert (h:equality x y); + [solve [cring] | clear H; clear h]) + || (try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H) +. + Ltac equalities_to_goal := lazymatch goal with - | H: (_ ?x ?y) |- _ => - try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H - | H: (_ _ ?x ?y) |- _ => - try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H - | H: (_ _ _ ?x ?y) |- _ => - try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H - | H: (_ _ _ _ ?x ?y) |- _ => - try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H + | H: (_ ?x ?y) |- _ => equality_to_goal H x y + | H: (_ _ ?x ?y) |- _ => equality_to_goal H x y + | H: (_ _ _ ?x ?y) |- _ => equality_to_goal H x y + | H: (_ _ _ _ ?x ?y) |- _ => equality_to_goal H x y (* extension possible :-) *) - | H: (?x == ?y) |- _ => - try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H + | H: (?x == ?y) |- _ => equality_to_goal H x y end. (* lp est incluse dans fv. La met en tete. *) @@ -392,8 +396,8 @@ match goal with let lp := get_lpol g in let lpol := eval compute in (List.rev lp) in (* idtac "polynomes:"; idtac lpol;*) - simpl; intros; - simpl; + (*simpl;*) intros; + (*simpl;*) let SplitPolyList kont := match lpol with | ?p2::?lp2 => kont p2 lp2 @@ -411,28 +415,28 @@ match goal with [ (vm_compute;reflexivity) || idtac "invalid nsatz certificate" | let Hg2 := fresh "Hg" in assert (Hg2: (interpret3 q fv) == 0); - [ simpl; + [ (*simpl*) idtac; generalize (@check_correct _ _ _ _ _ _ _ _ _ _ _ fv lp21 q (lci,lq) Hg); let cc := fresh "H" in - simpl; intro cc; apply cc; clear cc; - simpl; + (*simpl*) idtac; intro cc; apply cc; clear cc; + (*simpl*) idtac; repeat (split;[assumption|idtac]); exact I - | simpl in Hg2; simpl; + | (*simpl in Hg2;*) (*simpl*) idtac; apply Rintegral_domain_pow with (interpret3 c fv) (nat_of_N r); - simpl; + (*simpl*) idtac; try apply integral_domain_one_zero; try apply integral_domain_minus_one_zero; try trivial; try exact integral_domain_one_zero; try exact integral_domain_minus_one_zero - || (simpl) || idtac "could not prove discrimination result" + || ((*simpl*) idtac) || idtac "could not prove discrimination result" ] ] ) ) end end end end . -Ltac nsatz:= +Ltac nsatz_default:= intros; try apply (@psos_r1b _ _ _ _ _ _ _ _ _ _ _); match goal with |- (@equality ?r _ _ _) => @@ -440,11 +444,26 @@ Ltac nsatz:= nsatz_generic 6%N 1%Z (@nil r) (@nil r) end. +Tactic Notation "nsatz" := nsatz_default. + +Tactic Notation "nsatz" "with" + "radicalmax" ":=" constr(radicalmax) + "strategy" ":=" constr(info) + "parameters" ":=" constr(lparam) + "variables" ":=" constr(lvar):= + intros; + try apply (@psos_r1b _ _ _ _ _ _ _ _ _ _ _); + match goal with |- (@equality ?r _ _ _) => + repeat equalities_to_goal; + nsatz_generic radicalmax info lparam lvar + end. + Section test. Context {R:Type}`{Rid:Integral_domain R}. Goal forall x y:R, x == x. -nsatz. +nsatz with radicalmax := 6%N strategy := 1%Z parameters := (@nil R) + variables := (@nil R). Qed. Goal forall x y:R, x == y -> y*y == x*x. @@ -510,8 +529,6 @@ Qed. (* Rational numbers *) Require Import QArith. -Check Q_Setoid. - Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq). Instance Qri : (Ring (Ro:=Qops)). @@ -557,3 +574,6 @@ Goal forall x y:Z, x = y -> (x*x-x+1)%Z = ((y*y-y)+1+0)%Z. nsatz. Qed. +Goal forall x y:Z, x = y -> x = x -> (x*x-x+1)%Z = ((y*y-y)+1+0)%Z. +nsatz. +Qed.
\ No newline at end of file diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index 84a05f0ee..b635fd1fc 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -363,7 +363,7 @@ let stringPcut p = nsP2:=10; let res = if (length p)> !nsP2 - then (stringP [hd p])^" + "^(string_of_int (length p))^" termes" + then (stringP [hd p])^" + "^(string_of_int (length p))^" terms" else stringP p in (*Polynomesrec.nsP1:= max_int;*) nsP2:= max_int; @@ -992,7 +992,7 @@ let pbuchf pq p lp0= coefpoldep_remove a q; coefpoldep_set a q c) lca !poldep; let a0 = a in - info ("\nnew polynomials: "^(stringPcut (ppol a0))^"\n"); + info ("\nnew polynomial: "^(stringPcut (ppol a0))^"\n"); let ct = coef1 (* contentP a0 *) in (*info ("content: "^(string_of_coef ct)^"\n");*) poldep:=addS a0 lp; diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index 4b8b706d4..3b8cf137e 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -326,6 +326,8 @@ open PIdeal let term_pol_sparse np t= let d = !nvars in let rec aux t = +(* info ("conversion de: "^(string_of_term t)^"\n");*) + let res = match t with | Zero -> zeroP | Const r -> @@ -342,9 +344,11 @@ let term_pol_sparse np t= | Sub (t1,t2) -> plusP (aux t1) (oppP (aux t2)) | Mul (t1,t2) -> multP (aux t1) (aux t2) | Pow (t1,n) -> puisP (aux t1) n - in (*info ("conversion de: "^(string_of_term t)^"\n");*) + in +(* info ("donne: "^(stringP res)^"\n");*) + res + in let res= aux t in - (*info ("donne: "^(stringP res)^"\n");*) res (* sparse polynomial to term *) @@ -367,7 +371,7 @@ let polrec_to_term p = (* approximation of the Horner form used in the tactic ring *) let pol_sparse_to_term n2 p = - info "pol_sparse_to_term ->\n"; + (* info "pol_sparse_to_term ->\n";*) let p = PIdeal.repr p in let rec aux p = match p with @@ -411,7 +415,7 @@ let pol_sparse_to_term n2 p = then Var (string_of_int (i0)) else pow (Var (string_of_int (i0)),e0) in add(mul(vm, aux (List.rev (!p1))), aux (List.rev (!p2)))) - in info "-> pol_sparse_to_term\n"; + in (*info "-> pol_sparse_to_term\n";*) aux p @@ -492,35 +496,35 @@ let theoremedeszeros_termes lp = match lp with | Const (Int sugarparam)::Const (Int nparam)::lp -> ((match sugarparam with - |0 -> info "calcul sans sugar\n"; + |0 -> info "computation without sugar\n"; lexico:=false; sugar_flag := false; divide_rem_with_critical_pair := false - |1 -> info "calcul avec sugar\n"; + |1 -> info "computation with sugar\n"; lexico:=false; sugar_flag := true; divide_rem_with_critical_pair := false - |2 -> info "ordre lexico calcul sans sugar\n"; + |2 -> info "ordre lexico computation without sugar\n"; lexico:=true; sugar_flag := false; divide_rem_with_critical_pair := false - |3 -> info "ordre lexico calcul avec sugar\n"; + |3 -> info "ordre lexico computation with sugar\n"; lexico:=true; sugar_flag := true; divide_rem_with_critical_pair := false - |4 -> info "calcul sans sugar, division par les paires\n"; + |4 -> info "computation without sugar, division by pairs\n"; lexico:=false; sugar_flag := false; divide_rem_with_critical_pair := true - |5 -> info "calcul avec sugar, division par les paires\n"; + |5 -> info "computation with sugar, division by pairs\n"; lexico:=false; sugar_flag := true; divide_rem_with_critical_pair := true - |6 -> info "ordre lexico calcul sans sugar, division par les paires\n"; + |6 -> info "ordre lexico computation without sugar, division by pairs\n"; lexico:=true; sugar_flag := false; divide_rem_with_critical_pair := true - |7 -> info "ordre lexico calcul avec sugar, division par les paires\n"; + |7 -> info "ordre lexico computation with sugar, division by pairs\n"; lexico:=true; sugar_flag := true; divide_rem_with_critical_pair := true @@ -537,6 +541,7 @@ let theoremedeszeros_termes lp = | p::lp1 -> let lpol = List.rev lp1 in let (cert,lp0,p,_lct) = theoremedeszeros lpol p in + info "cert ok\n"; let lc = cert.last_comb::List.rev cert.gb_comb in match remove_zeros (fun x -> x=zeroP) lc with | [] -> assert false @@ -548,8 +553,8 @@ let theoremedeszeros_termes lp = let lci = List.rev lci in let lci = List.map (List.map (pol_sparse_to_term m)) lci in let lq = List.map (pol_sparse_to_term m) lq in - info ("nombre de parametres: "^string_of_int nparam^"\n"); - info "terme calcule\n"; + info ("number of parametres: "^string_of_int nparam^"\n"); + info "term computed\n"; (c,r,lci,lq) ) |_ -> assert false @@ -568,7 +573,7 @@ let nsatz lpol = let certif = hash_certif certif in let certif = certif_term certif in let c = mkt_term c in - info "constr calcule\n"; + info "constr computed\n"; (c, certif) *) @@ -589,7 +594,7 @@ let nsatz lpol = mkt_app lcons [tlp ();ltterm;r]) res (mkt_app lnil [tlp ()]) in - info "terme calcule\n"; + info "term computed\n"; res let return_term t = diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index b8210bd39..45fcb2d25 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -282,12 +282,11 @@ let rec multx n v p = p2.(i+n)<-p1.(i); done; Prec (x,p2) - |_ -> if p = (Pint coef0) then (Pint coef0) + |_ -> if equal p (Pint coef0) then (Pint coef0) else (let p2=Array.create (n+1) (Pint coef0) in p2.(n)<-p; Prec (v,p2)) - (* product *) let rec multP p q = match (p,q) with diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v index acb5cfd19..b190ea460 100644 --- a/test-suite/success/Nsatz.v +++ b/test-suite/success/Nsatz.v @@ -1,28 +1,26 @@ -Require Import Nsatz ZArith Reals List Ring_polynom. +Require Import Nsatz. (* Example with a generic domain *) -Context {R:Type}`{Rid:Integral_domain R}. +Section test. -Goal forall x y:A, x == y -> x+0 == y*1+0. -nsatz. -Qed. +Context {A:Type}`{Aid:Integral_domain A}. Lemma example3 : forall x y z, x+y+z==0 -> x*y+x*z+y*z==0-> - x*y*z==0 -> x*x*x==0. + x*y*z==0 -> x^3%Z==0. Proof. -Time nsatzA. -Admitted. +Time nsatz. +Qed. Lemma example4 : forall x y z u, x+y+z+u==0 -> x*y+x*z+x*u+y*z+y*u+z*u==0-> x*y*z+x*y*u+x*z*u+y*z*u==0-> - x*y*z*u==0 -> x*x*x*x==0. + x*y*z*u==0 -> x^4%Z==0. Proof. -Time nsatzA. +Time nsatz. Qed. Lemma example5 : forall x y z u v, @@ -30,15 +28,17 @@ Lemma example5 : forall x y z u v, x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v==0-> x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v==0-> x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z==0 -> - x*y*z*u*v==0 -> x*x*x*x*x ==0. + x*y*z*u*v==0 -> x^5%Z==0. Proof. -Time nsatzA. +Time nsatz. Qed. Goal forall x y:Z, x = y -> (x+0)%Z = (y*1+0)%Z. nsatz. Qed. +Require Import Reals. + Goal forall x y:R, x = y -> (x+0)%R = (y*1+0)%R. nsatz. Qed. @@ -47,85 +47,17 @@ Goal forall a b c x:R, a = b -> b = c -> (a*a)%R = (c*c)%R. nsatz. Qed. -Section Examples. - -Delimit Scope PE_scope with PE. -Infix "+" := PEadd : PE_scope. -Infix "*" := PEmul : PE_scope. -Infix "-" := PEsub : PE_scope. -Infix "^" := PEpow : PE_scope. -Notation "[ n ]" := (@PEc Z n) (at level 0). - -Open Scope R_scope. - -Lemma example1 : forall x y, - x+y=0 -> - x*y=0 -> - x^2=0. -Proof. - nsatz. -Qed. - -Lemma example2 : forall x, x^2=0 -> x=0. -Proof. - nsatz. -Qed. - -(* -Notation X := (PEX Z 3). -Notation Y := (PEX Z 2). -Notation Z_ := (PEX Z 1). -*) -Lemma example3b : forall x y z, - x+y+z=0 -> - x*y+x*z+y*z=0-> - x*y*z=0 -> x^3=0. -Proof. -Time nsatz. -Qed. - -(* -Notation X := (PEX Z 4). -Notation Y := (PEX Z 3). -Notation Z_ := (PEX Z 2). -Notation U := (PEX Z 1). -*) -Lemma example4b : forall x y z u, - x+y+z+u=0 -> - x*y+x*z+x*u+y*z+y*u+z*u=0-> - x*y*z+x*y*u+x*z*u+y*z*u=0-> - x*y*z*u=0 -> x^4=0. -Proof. -Time nsatz. -Qed. - -(* -Notation x_ := (PEX Z 5). -Notation y_ := (PEX Z 4). -Notation z_ := (PEX Z 3). -Notation u_ := (PEX Z 2). -Notation v_ := (PEX Z 1). -Notation "x :: y" := (List.cons x y) -(at level 60, right associativity, format "'[hv' x :: '/' y ']'"). -Notation "x :: y" := (List.app x y) -(at level 60, right associativity, format "x :: y"). -*) - -Lemma example5b : forall x y z u v, - x+y+z+u+v=0 -> - x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v=0-> - x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v=0-> - x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z=0 -> - x*y*z*u*v=0 -> x^5=0. -Proof. -Time nsatz. -Qed. - -End Examples. +End test. Section Geometry. +(* See the interactive pictures of Laurent Théry + on http://www-sop.inria.fr/marelle/CertiGeo/ + and research paper on + https://docs.google.com/fileview?id=0ByhB3nPmbnjTYzFiZmIyNGMtYTkwNC00NWFiLWJiNzEtODM4NmVkYTc2NTVk&hl=fr +*) -Open Scope R_scope. +Require Import List. +Require Import Reals. Record point:Type:={ X:R; @@ -147,60 +79,122 @@ Definition equal2(A B:point):= (X A)=(X B) /\ (Y A)=(Y B). Definition equal3(A B:point):= - ((X A)-(X B))^2+((Y A)-(Y B))^2 = 0. + ((X A)-(X B))^2%Z+((Y A)-(Y B))^2%Z = 0. Definition nequal2(A B:point):= (X A)<>(X B) \/ (Y A)<>(Y B). Definition nequal3(A B:point):= - not (((X A)-(X B))^2+((Y A)-(Y B))^2 = 0). + not (((X A)-(X B))^2%Z+((Y A)-(Y B))^2%Z = 0). Definition middle(A B I:point):= - 2*(X I)=(X A)+(X B) /\ 2*(Y I)=(Y A)+(Y B). + 2%R*(X I)=(X A)+(X B) /\ 2%R*(Y I)=(Y A)+(Y B). Definition distance2(A B:point):= - (X B - X A)^2 + (Y B - Y A)^2. + (X B - X A)^2%Z + (Y B - Y A)^2%Z. (* AB = CD *) Definition samedistance2(A B C D:point):= - (X B - X A)^2 + (Y B - Y A)^2 = (X D - X C)^2 + (Y D - Y C)^2. + (X B - X A)^2%Z + (Y B - Y A)^2%Z = (X D - X C)^2%Z + (Y D - Y C)^2%Z. Definition determinant(A O B:point):= (X A - X O)*(Y B - Y O) - (Y A - Y O)*(X B - X O). Definition scalarproduct(A O B:point):= (X A - X O)*(X B - X O) + (Y A - Y O)*(Y B - Y O). Definition norm2(A O B:point):= - ((X A - X O)^2+(Y A - Y O)^2)*((X B - X O)^2+(Y B - Y O)^2). - - -Lemma a1:forall A B C:Prop, ((A\/B)/\(A\/C)) -> (A\/(B/\C)). -intuition. -Qed. - -Lemma a2:forall A B C:Prop, ((A\/C)/\(B\/C)) -> ((A/\B)\/C). -intuition. + ((X A - X O)^2%Z+(Y A - Y O)^2%Z)*((X B - X O)^2%Z+(Y B - Y O)^2%Z). + +Definition equaldistance(A B C D:point):= + ((X B) - (X A))^2%Z + ((Y B) - (Y A))^2%Z = + ((X D) - (X C))^2%Z + ((Y D) - (Y C))^2%Z. + +Definition equaltangente(A B C D E F:point):= + let s1:= determinant A B C in + let c1:= scalarproduct A B C in + let s2:= determinant D E F in + let c2:= scalarproduct D E F in + s1 * c2 = s2 * c1. + +Ltac cnf2 f := + match f with + | ?A \/ (?B /\ ?C) => + let c1 := cnf2 (A\/B) in + let c2 := cnf2 (A\/C) in constr:(c1/\c2) + | (?B /\ ?C) \/ ?A => + let c1 := cnf2 (B\/A) in + let c2 := cnf2 (C\/A) in constr:(c1/\c2) + | (?A \/ ?B) \/ ?C => + let c1 := cnf2 (B\/C) in cnf2 (A \/ c1) + | _ => f + end +with cnf f := + match f with + | ?A \/ ?B => + let c1 := cnf A in + let c2 := cnf B in + cnf2 (c1 \/ c2) + | ?A /\ ?B => + let c1 := cnf A in + let c2 := cnf B in + constr:(c1 /\ c2) + | _ => f + end. + +Ltac scnf := + match goal with + | |- ?f => let c := cnf f in + assert c;[repeat split| tauto] + end. + +Ltac disj_to_pol f := + match f with + | ?a = ?b \/ ?g => let p := disj_to_pol g in constr:((a - b)* p) + | ?a = ?b => constr:(a - b) + end. + +Lemma fastnsatz1:forall x y:R, x - y = 0 -> x = y. +nsatz. Qed. -Lemma a3:forall a b c d:R, (a-b)*(c-d)=0 -> (a=b \/ c=d). -intros. -assert ( (a-b = 0) \/ (c-d = 0)). -apply Rmult_integral. -trivial. -destruct H0. -left; nsatz. -right; nsatz. -Qed. +Ltac fastnsatz:= + try trivial; try apply fastnsatz1; try trivial; nsatz. + +Ltac proof_pol_disj := + match goal with + | |- ?g => let p := disj_to_pol g in + let h := fresh "hp" in + assert (h:p = 0); + [idtac| + prod_disj h p] + | _ => idtac + end +with prod_disj h p := + match goal with + | |- ?a = ?b \/ ?g => + match p with + | ?q * ?p1 => + let h0 := fresh "hp" in + let h1 := fresh "hp" in + let h2 := fresh "hp" in + assert (h0:a - b = 0 \/ p1 = 0); + [apply Rmult_integral; exact h| + destruct h0 as [h1|h2]; + [left; fastnsatz| + right; prod_disj h2 p1]] + end + | _ => fastnsatz + end. -Ltac geo_unfold := - unfold collinear; unfold parallel; unfold notparallel; unfold orthogonal; - unfold equal2; unfold equal3; unfold nequal2; unfold nequal3; - unfold middle; unfold samedistance2; - unfold determinant; unfold scalarproduct; unfold norm2; unfold distance2. +(* +Goal forall a b c d e f:R, a=b \/ c=d \/ e=f \/ e=a. +intros. scnf; proof_pol_disj . +admit.*) -Ltac geo_end := - repeat ( - repeat (match goal with h:_/\_ |- _ => decompose [and] h; clear h end); - repeat (apply a1 || apply a2 || apply a3); - repeat split). +Ltac geo_unfold := + unfold collinear, parallel, notparallel, orthogonal, + equal2, equal3, nequal2, nequal3, + middle, samedistance2, + determinant, scalarproduct, norm2, distance2, + equaltangente, determinant, scalarproduct, equaldistance. Ltac geo_rewrite_hyps:= repeat (match goal with @@ -208,14 +202,41 @@ Ltac geo_rewrite_hyps:= | h:Y _ = _ |- _ => rewrite h in *; clear h end). +Ltac geo_split_hyps:= + repeat (match goal with + | h:_ /\ _ |- _ => destruct h + end). + Ltac geo_begin:= geo_unfold; intros; geo_rewrite_hyps; - geo_end. + geo_split_hyps; + scnf; proof_pol_disj. + +Ltac geo_end:= + simpl; unfold R2, addition, add_notation, multiplication, mul_notation, one, one_notation, zero, zero_notation, equality, eq_notation; + discrR. (* Examples *) +Lemma medians: forall A B C A1 B1 C1 H:point, + middle B C A1 -> + middle A C B1 -> + middle A B C1 -> + collinear A A1 H -> collinear B B1 H -> + collinear C C1 H + \/ collinear A B C. +Proof. geo_begin. Time nsatz. +(*Finished transaction in 2. secs (2.69359u,0.s) +*) Qed. + +Lemma Pythagore: forall A B C:point, + orthogonal A B A C -> + distance2 A C + distance2 A B = distance2 B C. +Proof. geo_begin. Time nsatz. +(*Finished transaction in 0. secs (0.354946u,0.s) +*) Qed. Lemma Thales: forall O A B C D:point, collinear O A C -> collinear O B D -> @@ -223,11 +244,252 @@ Lemma Thales: forall O A B C D:point, (distance2 O B * distance2 O C = distance2 O D * distance2 O A /\ distance2 O B * distance2 C D = distance2 O D * distance2 A B) \/ collinear O A B. -repeat geo_begin. -Time nsatz. +geo_begin. +Time nsatz. (*Finished transaction in 2. secs (1.598757u,0.s)*) Time nsatz. Qed. +Lemma segments_of_chords: forall A B C D M O:point, + equaldistance O A O B -> + equaldistance O A O C -> + equaldistance O A O D -> + collinear A B M -> + collinear C D M -> + (distance2 M A) * (distance2 M B) = (distance2 M C) * (distance2 M D) + \/ parallel A B C D. +Proof. geo_begin. Time nsatz. +(*Finished transaction in 3. secs (2.704589u,0.s) +*) Qed. + + +Lemma isoceles: forall A B C:point, + equaltangente A B C B C A -> + distance2 A B = distance2 A C + \/ collinear A B C. +Proof. geo_begin. Time nsatz. +(*Finished transaction in 1. secs (1.140827u,0.s)*) Qed. + +Lemma minh: forall A B C D O E H I:point, + X A = 0 -> Y A = 0 -> Y O = 0 -> + equaldistance O A O B -> + equaldistance O A O C -> + equaldistance O A O D -> + orthogonal A C B D -> + collinear A C E -> + collinear B D E -> + collinear A B H -> + orthogonal E H A B -> + collinear C D I -> + middle C D I -> + collinear H E I + \/ (X C)^2%Z * (X B)^5%Z * (X O)^2%Z + * (X C - 2%Z * X O)^3%Z * (-2%Z * X O + X B)=0 + \/ parallel A C B D. +Proof. geo_begin. +Time nsatz with radicalmax :=1%N strategy:=1%Z + parameters:=(X O::X B::X C::nil) + variables:= (@nil R). +(*Finished transaction in 13. secs (10.102464u,0.s) +*) +geo_end. +Qed. + +Lemma Pappus: forall A B C A1 B1 C1 P Q S:point, + X A = 0 -> Y A = 0 -> Y B = 0 -> Y C = 0 -> + collinear A1 B1 C1 -> + collinear A B1 P -> collinear A1 B P -> + collinear A C1 Q -> collinear A1 C Q -> + collinear B C1 S -> collinear B1 C S -> + collinear P Q S + \/ (Y A1 - Y B1)^2%Z=0 \/ (X A = X B1) + \/ (X A1 = X C) \/ (X C = X B1) + \/ parallel A B1 A1 B \/ parallel A C1 A1 C \/ parallel B C1 B1 C. +Proof. +geo_begin. +Time nsatz with radicalmax :=1%N strategy:=0%Z + parameters:=(X B::X A1::Y A1::X B1::Y B1::X C::Y C1::nil) + variables:= (X B + :: X A1 + :: Y A1 + :: X B1 + :: Y B1 + :: X C + :: Y C1 + :: X C1 :: Y P :: X P :: Y Q :: X Q :: Y S :: X S :: nil). +(*Finished transaction in 8. secs (7.795815u,0.000999999999999s) +*) +Qed. + +Lemma Simson: forall A B C O D E F G:point, + X A = 0 -> Y A = 0 -> + equaldistance O A O B -> + equaldistance O A O C -> + equaldistance O A O D -> + orthogonal E D B C -> + collinear B C E -> + orthogonal F D A C -> + collinear A C F -> + orthogonal G D A B -> + collinear A B G -> + collinear E F G + \/ (X C)^2%Z = 0 \/ (Y C)^2%Z = 0 \/ (X B)^2%Z = 0 \/ (Y B)^2%Z = 0 \/ (Y C - Y B)^2%Z = 0 + \/ equal3 B A + \/ equal3 A C \/ (X C - X B)^2%Z = 0 + \/ equal3 B C. +Proof. +geo_begin. +Time nsatz with radicalmax :=1%N strategy:=0%Z + parameters:=(X B::Y B::X C::Y C::Y D::nil) + variables:= (@nil R). (* compute -[X Y]. *) +(*Finished transaction in 8. secs (7.550852u,0.s) +*) +Qed. + +Lemma threepoints: forall A B C A1 B1 A2 B2 H1 H2 H3:point, + (* H1 intersection of bisections *) + middle B C A1 -> orthogonal H1 A1 B C -> + middle A C B1 -> orthogonal H1 B1 A C -> + (* H2 intersection of medians *) + collinear A A1 H2 -> collinear B B1 H2 -> + (* H3 intersection of altitudes *) + collinear B C A2 -> orthogonal A A2 B C -> + collinear A C B2 -> orthogonal B B2 A C -> + collinear A A1 H3 -> collinear B B1 H3 -> + collinear H1 H2 H3 + \/ collinear A B C. +Proof. geo_begin. Time nsatz. geo_end. +(*Finished transaction in 7. secs (6.282045u,0.s) +*) Qed. + +Lemma Feuerbach: forall A B C A1 B1 C1 O A2 B2 C2 O2:point, + forall r r2:R, + X A = 0 -> Y A = 0 -> X B = 1 -> Y B = 0-> + middle A B C1 -> middle B C A1 -> middle C A B1 -> + distance2 O A1 = distance2 O B1 -> + distance2 O A1 = distance2 O C1 -> + collinear A B C2 -> orthogonal A B O2 C2 -> + collinear B C A2 -> orthogonal B C O2 A2 -> + collinear A C B2 -> orthogonal A C O2 B2 -> + distance2 O2 A2 = distance2 O2 B2 -> + distance2 O2 A2 = distance2 O2 C2 -> + r^2%Z = distance2 O A1 -> + r2^2%Z = distance2 O2 A2 -> + distance2 O O2 = (r + r2)^2%Z + \/ distance2 O O2 = (r - r2)^2%Z + \/ collinear A B C. +Proof. geo_begin. Time nsatz. +(*Finished transaction in 21. secs (19.021109u,0.s)*) +geo_end. Qed. + + + + +Lemma Euler_circle: forall A B C A1 B1 C1 A2 B2 C2 O:point, + middle A B C1 -> middle B C A1 -> middle C A B1 -> + orthogonal A B C C2 -> collinear A B C2 -> + orthogonal B C A A2 -> collinear B C A2 -> + orthogonal A C B B2 -> collinear A C B2 -> + distance2 O A1 = distance2 O B1 -> + distance2 O A1 = distance2 O C1 -> + (distance2 O A2 = distance2 O A1 + /\distance2 O B2 = distance2 O A1 + /\distance2 O C2 = distance2 O A1) + \/ collinear A B C. +Proof. geo_begin. Time nsatz. +(*Finished transaction in 13. secs (11.208296u,0.124981s)*) +geo_end. +Time nsatz. +(*Finished transaction in 10. secs (8.846655u,0.s)*) +geo_end. +Time nsatz. +(*Finished transaction in 11. secs (9.186603u,0.s)*) +geo_end. +Qed. + + + +Lemma Desargues: forall A B C A1 B1 C1 P Q R S:point, + X S = 0 -> Y S = 0 -> Y A = 0 -> + collinear A S A1 -> collinear B S B1 -> collinear C S C1 -> + collinear B1 C1 P -> collinear B C P -> + collinear A1 C1 Q -> collinear A C Q -> + collinear A1 B1 R -> collinear A B R -> + collinear P Q R + \/ X A = X B \/ X A = X C \/ X B = X C \/ X A = 0 \/ Y B = 0 \/ Y C = 0 + \/ collinear S B C \/ parallel A C A1 C1 \/ parallel A B A1 B1. +Proof. +geo_begin. +Time +let lv := rev (X A + :: X B + :: Y B + :: X C + :: Y C + :: Y A1 :: X A1 + :: Y B1 + :: Y C1 + :: X R + :: Y R + :: X Q + :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in +nsatz with radicalmax :=1%N strategy:=0%Z + parameters:=(X A::X B::Y B::X C::Y C::X A1::Y B1::Y C1::nil) + variables:= lv. (*Finished transaction in 8. secs (8.02578u,0.001s)*) +Qed. + +Lemma chords: forall O A B C D M:point, + equaldistance O A O B -> + equaldistance O A O C -> + equaldistance O A O D -> + collinear A B M -> collinear C D M -> + scalarproduct A M B = scalarproduct C M D + \/ parallel A B C D. +Proof. geo_begin. Time nsatz. +(*Finished transaction in 4. secs (3.959398u,0.s)*) +Qed. + +Lemma Ceva: forall A B C D E F M:point, + collinear M A D -> collinear M B E -> collinear M C F -> + collinear B C D -> collinear E A C -> collinear F A B -> + (distance2 D B) * (distance2 E C) * (distance2 F A) = + (distance2 D C) * (distance2 E A) * (distance2 F B) + \/ collinear A B C. +Proof. geo_begin. Time nsatz. +(*Finished transaction in 105. secs (104.121171u,0.474928s)*) +Qed. + +Lemma bissectrices: forall A B C M:point, + equaltangente C A M M A B -> + equaltangente A B M M B C -> + equaltangente B C M M C A + \/ equal3 A B. +Proof. geo_begin. Time nsatz. +(*Finished transaction in 2. secs (1.937705u,0.s)*) +geo_end. Qed. + +Lemma bisections: forall A B C A1 B1 C1 H:point, + middle B C A1 -> orthogonal H A1 B C -> + middle A C B1 -> orthogonal H B1 A C -> + middle A B C1 -> + orthogonal H C1 A B + \/ collinear A B C. +Proof. geo_begin. +Time nsatz. (*Finished transaction in 2. secs (2.024692u,0.002s)*) +Qed. + +Lemma altitudes: forall A B C A1 B1 C1 H:point, + collinear B C A1 -> orthogonal A A1 B C -> + collinear A C B1 -> orthogonal B B1 A C -> + collinear A B C1 -> orthogonal C C1 A B -> + collinear A A1 H -> collinear B B1 H -> + collinear C C1 H + \/ equal2 A B + \/ collinear A B C. +Proof. geo_begin. +Time nsatz. (*Finished transaction in 3. secs (3.001544u,0.s)*) +Time nsatz. (*Finished transaction in 4. secs (3.113527u,0.s)*) +Qed. + Lemma hauteurs:forall A B C A1 B1 C1 H:point, collinear B C A1 -> orthogonal A A1 B C -> collinear A C B1 -> orthogonal B B1 A C -> @@ -238,26 +500,15 @@ Lemma hauteurs:forall A B C A1 B1 C1 H:point, \/ collinear A B C. geo_begin. - -(* Time nsatzRpv 2%N 1%Z (@nil R) (@nil R).*) -(*Finished transaction in 3. secs (2.363641u,0.s)*) -(*Time nsatz_domainR. trop long! *) Time let lv := constr:(Y A1 - :: X A1 - :: Y B1 - :: X B1 - :: Y A0 - :: Y B - :: X B - :: X A0 - :: X H - :: Y C - :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in - nsatz_domainpv ltac:pretacR 2%N 1%Z (@Datatypes.nil R) lv ltac:simplR Rdi; - discrR. -(* Finished transaction in 6. secs (5.579152u,0.001s) *) + :: X A1 :: Y B1 :: X B1 :: Y A :: Y B :: X B :: X A :: X H :: Y C + :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in +nsatz with radicalmax := 2%N strategy := 1%Z parameters := (@Datatypes.nil R) + variables := lv. +(*Finished transaction in 5. secs (4.360337u,0.008999s)*) Qed. + End Geometry. |