From 421488ebba1e8b1f0c9770a2bb1971551be76363 Mon Sep 17 00:00:00 2001 From: pottier Date: Thu, 16 Jun 2011 14:01:47 +0000 Subject: Tests de nsatz avec la geometrie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14210 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/nsatz/Nsatz.v | 64 +++++++++++++++++++++++++++++++----------------- plugins/nsatz/ideal.ml | 4 +-- plugins/nsatz/nsatz.ml4 | 37 ++++++++++++++++------------ plugins/nsatz/polynom.ml | 3 +-- 4 files changed, 66 insertions(+), 42 deletions(-) (limited to 'plugins/nsatz') 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 -- cgit v1.2.3