From f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 6 Aug 2010 16:15:08 -0400 Subject: Imported Upstream version 8.3~rc1+dfsg --- plugins/nsatz/Nsatz.v | 663 +++++++++++++++++++++++++++++++++++++++++++ plugins/nsatz/NsatzR.v | 407 -------------------------- plugins/nsatz/NsatzZ.v | 73 ----- plugins/nsatz/Nsatz_domain.v | 558 ------------------------------------ plugins/nsatz/vo.itarget | 4 +- 5 files changed, 664 insertions(+), 1041 deletions(-) create mode 100644 plugins/nsatz/Nsatz.v delete mode 100644 plugins/nsatz/NsatzR.v delete mode 100644 plugins/nsatz/NsatzZ.v delete mode 100644 plugins/nsatz/Nsatz_domain.v (limited to 'plugins/nsatz') diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v new file mode 100644 index 00000000..aa32b386 --- /dev/null +++ b/plugins/nsatz/Nsatz.v @@ -0,0 +1,663 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* A -> A}. +Notation "x + y" := (addition x y). +Class Multiplication (A : Type) := {multiplication : A -> A -> A}. +Notation "x * y" := (multiplication x y). +Class Subtraction (A : Type) := {subtraction : A -> A -> A}. +Notation "x - y" := (subtraction x y). +Class Opposite (A : Type) := {opposite : A -> A}. +Notation "- x" := (opposite x). + +Class Ring (R:Type) := { + ring0: R; ring1: R; + ring_plus: R->R->R; ring_mult: R->R->R; + ring_sub: R->R->R; ring_opp: R->R; + ring_eq : R -> R -> Prop; + ring_ring: + ring_theory ring0 ring1 ring_plus ring_mult ring_sub + ring_opp ring_eq; + ring_setoid: Equivalence ring_eq; + ring_plus_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_plus; + ring_mult_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_mult; + ring_sub_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_sub; + ring_opp_comp: Proper (ring_eq==>ring_eq) ring_opp +}. + +Class Domain (R : Type) := { + domain_ring:> Ring R; + domain_axiom_product: + forall x y, ring_eq (ring_mult x y) ring0 -> (ring_eq x ring0) \/ (ring_eq y ring0); + domain_axiom_one_zero: not (ring_eq ring1 ring0)}. + +Section domain. + +Variable R: Type. +Variable Rd: Domain R. + +Existing Instance ring_setoid. +Existing Instance ring_plus_comp. +Existing Instance ring_mult_comp. +Existing Instance ring_sub_comp. +Existing Instance ring_opp_comp. + +Add Ring Rr: (@ring_ring R (@domain_ring R Rd)). + +Instance zero_ring : Zero R := {zero := ring0}. +Instance one_ring : One R := {one := ring1}. +Instance addition_ring : Addition R := {addition x y := ring_plus x y}. +Instance multiplication_ring : Multiplication R := {multiplication x y := ring_mult x y}. +Instance subtraction_ring : Subtraction R := {subtraction x y := ring_sub x y}. +Instance opposite_ring : Opposite R := {opposite x := ring_opp x}. + +Infix "==" := ring_eq (at level 70, no associativity). + +Lemma psos_r1b: forall x y:R, x - y == 0 -> x == y. +intros x y H; setoid_replace x with ((x - y) + y); simpl; + [setoid_rewrite H | idtac]; simpl; ring. +Qed. + +Lemma psos_r1: forall x y, x == y -> x - y == 0. +intros x y H; simpl; setoid_rewrite H; simpl; ring. +Qed. + +Lemma nsatzR_diff: forall x y:R, not (x == y) -> not (x - y == 0). +intros. +intro; apply H. +simpl; setoid_replace x with ((x - y) + y). simpl. +setoid_rewrite H0. +simpl; ring. +simpl. simpl; ring. +Qed. + +(* adpatation du code de Benjamin aux setoides *) +Require Import ZArith. + +Definition PolZ := Pol Z. +Definition PEZ := PExpr Z. + +Definition P0Z : PolZ := @P0 Z 0%Z. + +Definition PolZadd : PolZ -> PolZ -> PolZ := + @Padd Z 0%Z Zplus Zeq_bool. + +Definition PolZmul : PolZ -> PolZ -> PolZ := + @Pmul Z 0%Z 1%Z Zplus Zmult Zeq_bool. + +Definition PolZeq := @Peq Z Zeq_bool. + +Definition norm := + @norm_aux Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool. + +Fixpoint mult_l (la : list PEZ) (lp: list PolZ) : PolZ := + match la, lp with + | a::la, p::lp => PolZadd (PolZmul (norm a) p) (mult_l la lp) + | _, _ => P0Z + end. + +Fixpoint compute_list (lla: list (list PEZ)) (lp:list PolZ) := + match lla with + | List.nil => lp + | la::lla => compute_list lla ((mult_l la lp)::lp) + end. + +Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) := + let (lla, lq) := certif in + let lp := List.map norm lpe in + PolZeq (norm qe) (mult_l lq (compute_list lla lp)). + + +(* Correction *) +Definition PhiR : list R -> PolZ -> R := + (Pphi 0 ring_plus ring_mult (gen_phiZ 0 1 ring_plus ring_mult ring_opp)). + +Definition pow (r : R) (n : nat) := pow_N 1 ring_mult r (Nnat.N_of_nat n). + +Definition PEevalR : list R -> PEZ -> R := + PEeval 0 ring_plus ring_mult ring_sub ring_opp + (gen_phiZ 0 1 ring_plus ring_mult ring_opp) + Nnat.nat_of_N pow. + +Lemma P0Z_correct : forall l, PhiR l P0Z = 0. +Proof. trivial. Qed. + +Lemma Rext: ring_eq_ext ring_plus ring_mult ring_opp ring_eq. +apply mk_reqe. intros. setoid_rewrite H; rewrite H0; ring. + intros. setoid_rewrite H; setoid_rewrite H0; ring. +intros. setoid_rewrite H; ring. Qed. + +Lemma Rset : Setoid_Theory R ring_eq. +apply ring_setoid. +Qed. + +Lemma PolZadd_correct : forall P' P l, + PhiR l (PolZadd P P') == ((PhiR l P) + (PhiR l P')). +Proof. +simpl. + refine (Padd_ok Rset Rext (Rth_ARth Rset Rext (@ring_ring _ (@domain_ring _ Rd))) + (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd)))). +Qed. + +Lemma PolZmul_correct : forall P P' l, + PhiR l (PolZmul P P') == ((PhiR l P) * (PhiR l P')). +Proof. + refine (Pmul_ok Rset Rext (Rth_ARth Rset Rext (@ring_ring _ (@domain_ring _ Rd))) + (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd)))). +Qed. + +Lemma R_power_theory + : power_theory 1 ring_mult ring_eq Nnat.nat_of_N pow. +apply mkpow_th. unfold pow. intros. rewrite Nnat.N_of_nat_of_N. ring. Qed. + +Lemma norm_correct : + forall (l : list R) (pe : PEZ), PEevalR l pe == PhiR l (norm pe). +Proof. + intros;apply (norm_aux_spec Rset Rext (Rth_ARth Rset Rext (@ring_ring _ (@domain_ring _ Rd))) + (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd))) R_power_theory) + with (lmp:= List.nil). + compute;trivial. +Qed. + +Lemma PolZeq_correct : forall P P' l, + PolZeq P P' = true -> + PhiR l P == PhiR l P'. +Proof. + intros;apply + (Peq_ok Rset Rext (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd))));trivial. +Qed. + +Fixpoint Cond0 (A:Type) (Interp:A->R) (l:list A) : Prop := + match l with + | List.nil => True + | a::l => Interp a == 0 /\ Cond0 A Interp l + end. + +Lemma mult_l_correct : forall l la lp, + Cond0 PolZ (PhiR l) lp -> + PhiR l (mult_l la lp) == 0. +Proof. + induction la;simpl;intros. ring. + destruct lp;trivial. simpl. ring. + simpl in H;destruct H. + setoid_rewrite PolZadd_correct. + simpl. setoid_rewrite PolZmul_correct. simpl. setoid_rewrite H. + setoid_rewrite IHla. unfold zero. simpl. ring. trivial. +Qed. + +Lemma compute_list_correct : forall l lla lp, + Cond0 PolZ (PhiR l) lp -> + Cond0 PolZ (PhiR l) (compute_list lla lp). +Proof. + induction lla;simpl;intros;trivial. + apply IHlla;simpl;split;trivial. + apply mult_l_correct;trivial. +Qed. + +Lemma check_correct : + forall l lpe qe certif, + check lpe qe certif = true -> + Cond0 PEZ (PEevalR l) lpe -> + PEevalR l qe == 0. +Proof. + unfold check;intros l lpe qe (lla, lq) H2 H1. + apply PolZeq_correct with (l:=l) in H2. + rewrite norm_correct, H2. + apply mult_l_correct. + apply compute_list_correct. + clear H2 lq lla qe;induction lpe;simpl;trivial. + simpl in H1;destruct H1. + rewrite <- norm_correct;auto. +Qed. + +(* fin *) + +Lemma pow_not_zero: forall p n, pow p n == 0 -> p == 0. +induction n. unfold pow; simpl. intros. absurd (1 == 0). +simpl. apply domain_axiom_one_zero. + trivial. setoid_replace (pow p (S n)) with (p * (pow p n)). intros. +case (@domain_axiom_product _ _ _ _ H). trivial. trivial. +unfold pow; simpl. +clear IHn. induction n; simpl; try ring. + rewrite pow_pos_Psucc. ring. exact Rset. + intros. setoid_rewrite H; setoid_rewrite H0; ring. + intros. simpl; ring. intros. simpl; ring. Qed. + +Lemma Rdomain_pow: forall c p r, ~c == ring0 -> ring_mult c (pow p r) == ring0 -> p == ring0. +intros. case (@domain_axiom_product _ _ _ _ H0). intros; absurd (c == ring0); auto. +intros. apply pow_not_zero with r. trivial. Qed. + +Definition R2:= ring_plus ring1 ring1. + +Fixpoint IPR p {struct p}: R := + match p with + xH => ring1 + | xO xH => ring_plus ring1 ring1 + | xO p1 => ring_mult R2 (IPR p1) + | xI xH => ring_plus ring1 (ring_plus ring1 ring1) + | xI p1 => ring_plus ring1 (ring_mult R2 (IPR p1)) + end. + +Definition IZR1 z := + match z with Z0 => ring0 + | Zpos p => IPR p + | Zneg p => ring_opp(IPR p) + end. + +Fixpoint interpret3 t fv {struct t}: R := + match t with + | (PEadd t1 t2) => + let v1 := interpret3 t1 fv in + let v2 := interpret3 t2 fv in (ring_plus v1 v2) + | (PEmul t1 t2) => + let v1 := interpret3 t1 fv in + let v2 := interpret3 t2 fv in (ring_mult v1 v2) + | (PEsub t1 t2) => + let v1 := interpret3 t1 fv in + let v2 := interpret3 t2 fv in (ring_sub v1 v2) + | (PEopp t1) => + let v1 := interpret3 t1 fv in (ring_opp v1) + | (PEpow t1 t2) => + let v1 := interpret3 t1 fv in pow v1 (Nnat.nat_of_N t2) + | (PEc t1) => (IZR1 t1) + | (PEX n) => List.nth (pred (nat_of_P n)) fv 0 + end. + + +End domain. + +Ltac equalities_to_goal := + lazymatch goal with + | H: (@ring_eq _ _ ?x ?y) |- _ => + try generalize (@psos_r1 _ _ _ _ H); clear H + end. + +Ltac nsatz_domain_begin tacsimpl := + intros; + try apply (@psos_r1b _ _); + repeat equalities_to_goal; + tacsimpl. + +Ltac generalise_eq_hyps:= + repeat + (match goal with + |h : (@ring_eq _ _ ?p ?q)|- _ => revert h + end). + +Ltac lpol_goal t := + match t with + | ?a = ring0 -> ?b => + let r:= lpol_goal b in + constr:(a::r) + | ?a = ring0 => constr:(a::nil) + end. + +(* lp est incluse dans fv. La met en tete. *) + +Ltac parametres_en_tete fv lp := + match fv with + | (@nil _) => lp + | (@cons _ ?x ?fv1) => + let res := AddFvTail x lp in + parametres_en_tete fv1 res + end. + +Ltac append1 a l := + match l with + | (@nil _) => constr:(cons a l) + | (cons ?x ?l) => let l' := append1 a l in constr:(cons x l') + end. + +Ltac rev l := + match l with + |(@nil _) => l + | (cons ?x ?l) => let l' := rev l in append1 x l' + end. + + + +Ltac nsatz_call_n info nparam p rr lp kont := + (*idtac "Trying power: " rr;*) + let ll := constr:(PEc info :: PEc nparam :: PEpow p rr :: lp) in + nsatz_compute ll; + (*idtac "done";*) + match goal with + | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ => + intros _; + set (lci:=lci0); + set (lq:=lq0); + kont c rr lq lci + end. + +Ltac nsatz_call radicalmax info nparam p lp kont := + let rec try_n n := + lazymatch n with + | 0%N => fail + | _ => + (let r := eval compute in (Nminus radicalmax (Npred n)) in + nsatz_call_n info nparam p r lp kont) || + let n' := eval compute in (Npred n) in try_n n' + end in + try_n radicalmax. + + +Set Implicit Arguments. +Class Cclosed_seq T (l:list T) := {}. +Instance Iclosed_nil T : Cclosed_seq (T:=T) nil. +Instance Iclosed_cons T t l `{Cclosed_seq (T:=T) l} : Cclosed_seq (T:=T) (t::l). + +Class Cfind_at (R:Type) (b:R) (l:list R) (i:nat) := {}. +Instance Ifind0 (R:Type) (b:R) l: Cfind_at b (b::l) 0. +Instance IfindS (R:Type) (b2 b1:R) l i `{Cfind_at R b1 l i} : Cfind_at b1 (b2::l) (S i) | 1. +Definition Ifind0' := Ifind0. +Definition IfindS' := IfindS. + +Definition li_find_at (R:Type) (b:R) l i `{Cfind_at R b l i} {H:Cclosed_seq (T:=R) l} := (l,i). + +Class Creify (R:Type) (e:PExpr Z) (l:list R) (b:R) := {}. +Instance Ireify_zero (R:Type) (Rd:Domain R) l : Creify (PEc 0%Z) l ring0. +Instance Ireify_one (R:Type) (Rd:Domain R) l : Creify (PEc 1%Z) l ring1. +Instance Ireify_plus (R:Type) (Rd:Domain R) e1 l b1 e2 b2 `{Creify R e1 l b1} `{Creify R e2 l b2} + : Creify (PEadd e1 e2) l (ring_plus b1 b2). +Instance Ireify_mult (R:Type) (Rd:Domain R) e1 l b1 e2 b2 `{Creify R e1 l b1} `{Creify R e2 l b2} + : Creify (PEmul e1 e2) l (ring_mult b1 b2). +Instance Ireify_sub (R:Type) (Rd:Domain R) e1 l b1 e2 b2 `{Creify R e1 l b1} `{Creify R e2 l b2} + : Creify (PEsub e1 e2) l (ring_sub b1 b2). +Instance Ireify_opp (R:Type) (Rd:Domain R) e1 l b1 `{Creify R e1 l b1} + : Creify (PEopp e1) l (ring_opp b1). +Instance Ireify_var (R:Type) b l i `{Cfind_at R b l i} + : Creify (PEX _ (P_of_succ_nat i)) l b | 100. + + +Class Creifylist (R:Type) (le:list (PExpr Z)) (l:list R) (lb:list R) := {}. +Instance Creify_nil (R:Type) l : Creifylist nil l (@nil R). +Instance Creify_cons (R:Type) e1 l b1 le2 lb2 `{Creify R e1 l b1} `{Creifylist R le2 l lb2} + : Creifylist (e1::le2) l (b1::lb2). + +Definition li_reifyl (R:Type) le l lb `{Creifylist R le l lb} + {H:Cclosed_seq (T:=R) l} := (l,le). + +Unset Implicit Arguments. + +Ltac lterm_goal g := + match g with + ring_eq ?b1 ?b2 => constr:(b1::b2::nil) + | ring_eq ?b1 ?b2 -> ?g => let l := lterm_goal g in constr:(b1::b2::l) + end. + +Ltac reify_goal l le lb Rd:= + match le with + nil => idtac + | ?e::?le1 => + match lb with + ?b::?lb1 => (* idtac "b="; idtac b;*) + let x := fresh "B" in + set (x:= b) at 1; + change x with (@interpret3 _ Rd e l); + clear x; + reify_goal l le1 lb1 Rd + end + end. + +Ltac get_lpol g := + match g with + ring_eq (interpret3 _ _ ?p _) _ => constr:(p::nil) + | ring_eq (interpret3 _ _ ?p _) _ -> ?g => + let l := get_lpol g in constr:(p::l) + end. + +Ltac nsatz_domain_generic radicalmax info lparam lvar tacsimpl Rd := + match goal with + |- ?g => let lb := lterm_goal g in + (*idtac "lb"; idtac lb;*) + match eval red in (li_reifyl (lb:=lb)) with + | (?fv, ?le) => + let fv := match lvar with + (@nil _) => fv + | _ => lvar + end in + (* idtac "variables:";idtac fv;*) + let nparam := eval compute in (Z_of_nat (List.length lparam)) in + let fv := parametres_en_tete fv lparam in + (*idtac "variables:"; idtac fv; + idtac "nparam:"; idtac nparam; *) + match eval red in (li_reifyl (l:=fv) (lb:=lb)) with + | (?fv, ?le) => + (*idtac "variables:";idtac fv; idtac le; idtac lb;*) + reify_goal fv le lb Rd; + match goal with + |- ?g => + let lp := get_lpol g in + let lpol := eval compute in (List.rev lp) in + (*idtac "polynomes:"; idtac lpol;*) + tacsimpl; intros; + + let SplitPolyList kont := + match lpol with + | ?p2::?lp2 => kont p2 lp2 + | _ => idtac "polynomial not in the ideal" + end in + tacsimpl; + SplitPolyList ltac:(fun p lp => + set (p21:=p) ; + set (lp21:=lp); + (*idtac "lp:"; idtac lp; *) + nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => + set (q := PEmul c (PEpow p21 r)); + let Hg := fresh "Hg" in + assert (Hg:check lp21 q (lci,lq) = true); + [ (vm_compute;reflexivity) || idtac "invalid nsatz certificate" + | let Hg2 := fresh "Hg" in + assert (Hg2: ring_eq (interpret3 _ Rd q fv) ring0); + [ tacsimpl; + apply (@check_correct _ Rd fv lp21 q (lci,lq) Hg); + tacsimpl; + repeat (split;[assumption|idtac]); exact I + | simpl in Hg2; tacsimpl; + apply Rdomain_pow with (interpret3 _ Rd c fv) (Nnat.nat_of_N r); auto with domain; + tacsimpl; apply domain_axiom_one_zero + || (simpl) || idtac "could not prove discrimination result" + ] + ] +) +) +end end end end . + +Ltac nsatz_domainpv pretac radicalmax info lparam lvar tacsimpl rd := + pretac; + nsatz_domain_begin tacsimpl; auto with domain; + nsatz_domain_generic radicalmax info lparam lvar tacsimpl rd. + +Ltac nsatz_domain:= + intros; + match goal with + |- (@ring_eq _ (@domain_ring ?r ?rd) _ _ ) => + nsatz_domainpv ltac:idtac 6%N 1%Z (@nil r) (@nil r) ltac:(simpl) rd + end. + +(* Dans R *) +Require Import Reals. +Require Import RealField. + +Instance Rri : Ring R := { + ring0 := 0%R; + ring1 := 1%R; + ring_plus := Rplus; + ring_mult := Rmult; + ring_sub := Rminus; + ring_opp := Ropp; + ring_eq := @eq R; + ring_ring := RTheory}. + +Lemma Raxiom_one_zero: 1%R <> 0%R. +discrR. +Qed. + +Instance Rdi : Domain R := { + domain_ring := Rri; + domain_axiom_product := Rmult_integral; + domain_axiom_one_zero := Raxiom_one_zero}. + +Hint Resolve ring_setoid ring_plus_comp ring_mult_comp ring_sub_comp ring_opp_comp: domain. + +Ltac replaceR:= +replace 0%R with (@ring0 _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; +replace 1%R with (@ring1 _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; +replace Rplus with (@ring_plus _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; +replace Rmult with (@ring_mult _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; +replace Rminus with (@ring_sub _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; +replace Ropp with (@ring_opp _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; +replace (@eq R) with (@ring_eq _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]. + +Ltac simplR:= + simpl; replaceR. + +Ltac pretacR:= + replaceR; + replace Rri with (@domain_ring _ Rdi) in *; [idtac | reflexivity]. + +Ltac nsatz_domainR:= + nsatz_domainpv ltac:pretacR 6%N 1%Z (@Datatypes.nil R) (@Datatypes.nil R) + ltac:simplR Rdi; + discrR. + + +Goal forall x y:R, x = y -> (x*x-x+1)%R = ((y*y-y)+1+0)%R. +nsatz_domainR. +Qed. + + +(* Dans Z *) +Instance Zri : Ring Z := { + ring0 := 0%Z; + ring1 := 1%Z; + ring_plus := Zplus; + ring_mult := Zmult; + ring_sub := Zminus; + ring_opp := Zopp; + ring_eq := (@eq Z); + ring_ring := Zth}. + +Lemma Zaxiom_one_zero: 1%Z <> 0%Z. +discriminate. +Qed. + +Instance Zdi : Domain Z := { + domain_ring := Zri; + domain_axiom_product := Zmult_integral; + domain_axiom_one_zero := Zaxiom_one_zero}. + +Ltac replaceZ := +replace 0%Z with (@ring0 _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; +replace 1%Z with (@ring1 _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; +replace Zplus with (@ring_plus _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; +replace Zmult with (@ring_mult _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; +replace Zminus with (@ring_sub _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; +replace Zopp with (@ring_opp _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; +replace (@eq Z) with (@ring_eq _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]. + +Ltac simplZ:= + simpl; replaceZ. + +Ltac pretacZ := +replaceZ; +replace Zri with (@domain_ring _ Zdi) in *; [idtac | reflexivity]. + +Ltac nsatz_domainZ:= +nsatz_domainpv ltac:pretacZ 6%N 1%Z (@Datatypes.nil Z) (@Datatypes.nil Z) ltac:simplZ Zdi. + + +(* Dans Q *) +Require Import QArith. + +Instance Qri : Ring Q := { + ring0 := 0%Q; + ring1 := 1%Q; + ring_plus := Qplus; + ring_mult := Qmult; + ring_sub := Qminus; + ring_opp := Qopp; + ring_eq := Qeq; + ring_ring := Qsrt}. + +Lemma Qaxiom_one_zero: not (Qeq 1%Q 0%Q). +discriminate. +Qed. + +Instance Qdi : Domain Q := { + domain_ring := Qri; + domain_axiom_product := Qmult_integral; + domain_axiom_one_zero := Qaxiom_one_zero}. + +Ltac replaceQ := +replace 0%Q with (@ring0 _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; +replace 1%Q with (@ring1 _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; +replace Qplus with (@ring_plus _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; +replace Qmult with (@ring_mult _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; +replace Qminus with (@ring_sub _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; +replace Qopp with (@ring_opp _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; +replace Qeq with (@ring_eq _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]. + +Ltac simplQ:= + simpl; replaceQ. + +Ltac pretacQ := +replaceQ; +replace Qri with (@domain_ring _ Qdi) in *; [idtac | reflexivity]. + +Ltac nsatz_domainQ:= +nsatz_domainpv ltac:pretacQ 6%N 1%Z (@Datatypes.nil Q) (@Datatypes.nil Q) ltac:simplQ Qdi. + +(* tactique générique *) + +Ltac nsatz := + intros; + match goal with + | |- (@eq R _ _) => nsatz_domainR + | |- (@eq Z _ _) => nsatz_domainZ + | |- (@Qeq _ _) => nsatz_domainQ + | |- _ => nsatz_domain + end. +(* +Goal forall x y:Q, Qeq x y -> Qeq (x*x-x+1)%Q ((y*y-y)+1+0)%Q. +nsatz. +Qed. + +Goal forall x y:Z, x = y -> (x*x-x+1)%Z = ((y*y-y)+1+0)%Z. +nsatz. +Qed. + +Goal forall x y:R, x = y -> (x*x-x+1)%R = ((y*y-y)+1+0)%R. +nsatz. +Qed. +*) diff --git a/plugins/nsatz/NsatzR.v b/plugins/nsatz/NsatzR.v deleted file mode 100644 index 41e02c76..00000000 --- a/plugins/nsatz/NsatzR.v +++ /dev/null @@ -1,407 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* x = y. -intros x y H; replace x with ((x - y) + y); - [rewrite H | idtac]; ring. -Qed. - -Lemma psos_r1: forall x y, x = y -> x - y = 0. -intros x y H; rewrite H; ring. -Qed. - -Lemma nsatzR_not1: forall x y:R, x<>y -> exists z:R, z*(x-y)-1=0. -intros. -exists (1/(x-y)). -field. -unfold not. -unfold not in H. -intros. -apply H. -replace x with ((x-y)+y). -rewrite H0. -ring. -ring. -Qed. - -Lemma nsatzR_not1_0: forall x:R, x<>0 -> exists z:R, z*x-1=0. -intros. -exists (1/(x)). -field. -auto. -Qed. - - -Ltac equalities_to_goal := - lazymatch goal with - | H: (@eq R ?x 0) |- _ => try revert H - | H: (@eq R 0 ?x) |- _ => - try generalize (sym_equal H); clear H - | H: (@eq R ?x ?y) |- _ => - try generalize (psos_r1 _ _ H); clear H - end. - -Lemma nsatzR_not2: 1<>0. -auto with *. -Qed. - -Lemma nsatzR_diff: forall x y:R, x<>y -> x-y<>0. -intros. -intro; apply H. -replace x with (x-y+y) by ring. -rewrite H0; ring. -Qed. - -(* Removes x<>0 from hypothesis *) -Ltac nsatzR_not_hyp:= - match goal with - | H: ?x<>?y |- _ => - match y with - |0 => - let H1:=fresh "Hnsatz" in - let y:=fresh "x" in - destruct (@nsatzR_not1_0 _ H) as (y,H1); clear H - |_ => generalize (@nsatzR_diff _ _ H); clear H; intro - end - end. - -Ltac nsatzR_not_goal := - match goal with - | |- ?x<>?y :> R => red; intro; apply nsatzR_not2 - | |- False => apply nsatzR_not2 - end. - -Ltac nsatzR_begin := - intros; - repeat nsatzR_not_hyp; - try nsatzR_not_goal; - try apply psos_r1b; - repeat equalities_to_goal. - -(* code de Benjamin *) - -Definition PolZ := Pol Z. -Definition PEZ := PExpr Z. - -Definition P0Z : PolZ := @P0 Z 0%Z. - -Definition PolZadd : PolZ -> PolZ -> PolZ := - @Padd Z 0%Z Zplus Zeq_bool. - -Definition PolZmul : PolZ -> PolZ -> PolZ := - @Pmul Z 0%Z 1%Z Zplus Zmult Zeq_bool. - -Definition PolZeq := @Peq Z Zeq_bool. - -Definition norm := - @norm_aux Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool. - -Fixpoint mult_l (la : list PEZ) (lp: list PolZ) : PolZ := - match la, lp with - | a::la, p::lp => PolZadd (PolZmul (norm a) p) (mult_l la lp) - | _, _ => P0Z - end. - -Fixpoint compute_list (lla: list (list PEZ)) (lp:list PolZ) := - match lla with - | List.nil => lp - | la::lla => compute_list lla ((mult_l la lp)::lp) - end. - -Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) := - let (lla, lq) := certif in - let lp := List.map norm lpe in - PolZeq (norm qe) (mult_l lq (compute_list lla lp)). - - -(* Correction *) -Definition PhiR : list R -> PolZ -> R := - (Pphi 0 Rplus Rmult (gen_phiZ 0 1 Rplus Rmult Ropp)). - -Definition PEevalR : list R -> PEZ -> R := - PEeval 0 Rplus Rmult Rminus Ropp (gen_phiZ 0 1 Rplus Rmult Ropp) - Nnat.nat_of_N pow. - -Lemma P0Z_correct : forall l, PhiR l P0Z = 0. -Proof. trivial. Qed. - - -Lemma PolZadd_correct : forall P' P l, - PhiR l (PolZadd P P') = (PhiR l P + PhiR l P'). -Proof. - refine (Padd_ok Rset Rext (Rth_ARth Rset Rext (F_R Rfield)) - (gen_phiZ_morph Rset Rext (F_R Rfield))). -Qed. - -Lemma PolZmul_correct : forall P P' l, - PhiR l (PolZmul P P') = (PhiR l P * PhiR l P'). -Proof. - refine (Pmul_ok Rset Rext (Rth_ARth Rset Rext (F_R Rfield)) - (gen_phiZ_morph Rset Rext (F_R Rfield))). -Qed. - -Lemma norm_correct : - forall (l : list R) (pe : PEZ), PEevalR l pe = PhiR l (norm pe). -Proof. - intros;apply (norm_aux_spec Rset Rext (Rth_ARth Rset Rext (F_R Rfield)) - (gen_phiZ_morph Rset Rext (F_R Rfield)) R_power_theory) with (lmp:= List.nil). - compute;trivial. -Qed. - -Lemma PolZeq_correct : forall P P' l, - PolZeq P P' = true -> - PhiR l P = PhiR l P'. -Proof. - intros;apply - (Peq_ok Rset Rext (gen_phiZ_morph Rset Rext (F_R Rfield)));trivial. -Qed. - -Fixpoint Cond0 (A:Type) (Interp:A->R) (l:list A) : Prop := - match l with - | List.nil => True - | a::l => Interp a = 0 /\ Cond0 A Interp l - end. - -Lemma mult_l_correct : forall l la lp, - Cond0 PolZ (PhiR l) lp -> - PhiR l (mult_l la lp) = 0. -Proof. - induction la;simpl;intros;trivial. - destruct lp;trivial. - simpl in H;destruct H. - rewrite PolZadd_correct, PolZmul_correct, H, IHla;[ring | trivial]. -Qed. - -Lemma compute_list_correct : forall l lla lp, - Cond0 PolZ (PhiR l) lp -> - Cond0 PolZ (PhiR l) (compute_list lla lp). -Proof. - induction lla;simpl;intros;trivial. - apply IHlla;simpl;split;trivial. - apply mult_l_correct;trivial. -Qed. - -Lemma check_correct : - forall l lpe qe certif, - check lpe qe certif = true -> - Cond0 PEZ (PEevalR l) lpe -> - PEevalR l qe = 0. -Proof. - unfold check;intros l lpe qe (lla, lq) H2 H1. - apply PolZeq_correct with (l:=l) in H2. - rewrite norm_correct, H2. - apply mult_l_correct. - apply compute_list_correct. - clear H2 lq lla qe;induction lpe;simpl;trivial. - simpl in H1;destruct H1. - rewrite <- norm_correct;auto. -Qed. - -(* fin du code de Benjamin *) - -Lemma nsatzR_l3:forall c p r, ~c=0 -> c*p^r=0 -> p=0. -intros. -elim (Rmult_integral _ _ H0);intros. - absurd (c=0);auto. - - clear H0; induction r; simpl in *. - contradict H1; discrR. - - elim (Rmult_integral _ _ H1); auto. -Qed. - - -Ltac generalise_eq_hyps:= - repeat - (match goal with - |h : (?p = ?q)|- _ => revert h - end). - -Ltac lpol_goal t := - match t with - | ?a = 0 -> ?b => - let r:= lpol_goal b in - constr:(a::r) - | ?a = 0 => constr:(a::nil) - end. - -Fixpoint IPR p {struct p}: R := - match p with - xH => 1 - | xO xH => 1 + 1 - | xO p1 => 2 * (IPR p1) - | xI xH => 1 + (1 + 1) - | xI p1 => 1 + 2 * (IPR p1) - end. - -Definition IZR1 z := - match z with Z0 => 0 - | Zpos p => IPR p - | Zneg p => -(IPR p) - end. - -Fixpoint interpret3 t fv {struct t}: R := - match t with - | (PEadd t1 t2) => - let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (v1 + v2) - | (PEmul t1 t2) => - let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (v1 * v2) - | (PEsub t1 t2) => - let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (v1 - v2) - | (PEopp t1) => - let v1 := interpret3 t1 fv in (-v1) - | (PEpow t1 t2) => - let v1 := interpret3 t1 fv in v1 ^(Nnat.nat_of_N t2) - | (PEc t1) => (IZR1 t1) - | (PEX n) => List.nth (pred (nat_of_P n)) fv 0 - end. - -(* lp est incluse dans fv. La met en tete. *) - -Ltac parametres_en_tete fv lp := - match fv with - | (@nil _) => lp - | (@cons _ ?x ?fv1) => - let res := AddFvTail x lp in - parametres_en_tete fv1 res - end. - -Ltac append1 a l := - match l with - | (@nil _) => constr:(cons a l) - | (cons ?x ?l) => let l' := append1 a l in constr:(cons x l') - end. - -Ltac rev l := - match l with - |(@nil _) => l - | (cons ?x ?l) => let l' := rev l in append1 x l' - end. - - -Ltac nsatz_call_n info nparam p rr lp kont := - nsatz_compute (PEc info :: PEc nparam :: PEpow p rr :: lp); - match goal with - | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ => - intros _; - set (lci:=lci0); - set (lq:=lq0); - kont c rr lq lci - end. - -Ltac nsatz_call radicalmax info nparam p lp kont := - let rec try_n n := - lazymatch n with - | 0%N => fail - | _ => -(* idtac "Trying power: " n;*) - (let r := eval compute in (Nminus radicalmax (Npred n)) in - nsatz_call_n info nparam p r lp kont) || - let n' := eval compute in (Npred n) in try_n n' - end in - try_n radicalmax. - - -Ltac nsatzR_gen radicalmax info lparam lvar n RNG lH _rl := - get_Pre RNG (); - let mkFV := Ring_tac.get_RingFV RNG in - let mkPol := Ring_tac.get_RingMeta RNG in - generalise_eq_hyps; - let t := Get_goal in - let lpol := lpol_goal t in - intros; - let fv := - match lvar with - | nil => - let fv1 := FV_hypo_tac mkFV ltac:(get_Eq RNG) lH in - let fv1 := list_fold_right mkFV fv1 lpol in - rev fv1 - (* heuristique: les dernieres variables auront le poid le plus fort *) - | _ => lvar - end in - check_fv fv; - (*idtac "variables:";idtac fv;*) - let nparam := eval compute in (Z_of_nat (List.length lparam)) in - let fv := parametres_en_tete fv lparam in - idtac "variables:"; idtac fv; - (* idtac "nparam:"; idtac nparam;*) - let lpol := list_fold_right - ltac:(fun p l => let p' := mkPol p fv in constr:(p'::l)) - (@nil (PExpr Z)) - lpol in - let lpol := eval compute in (List.rev lpol) in - (*idtac lpol;*) - let SplitPolyList kont := - match lpol with - | ?p2::?lp2 => kont p2 lp2 - | _ => idtac "polynomial not in the ideal" - end in - SplitPolyList ltac:(fun p lp => - set (p21:=p) ; - set (lp21:=lp); - nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => - set (q := PEmul c (PEpow p21 r)); - let Hg := fresh "Hg" in - assert (Hg:check lp21 q (lci,lq) = true); - [ (vm_compute;reflexivity) || idtac "invalid nsatz certificate" - | let Hg2 := fresh "Hg" in - assert (Hg2: interpret3 q fv = 0); - [ simpl; apply (@check_correct fv lp21 q (lci,lq) Hg); simpl; - repeat (split;[assumption|idtac]); exact I - | simpl in Hg2; simpl; - apply nsatzR_l3 with (interpret3 c fv) (Nnat.nat_of_N r);simpl; - [ discrR || idtac "could not prove discrimination result" - | exact Hg2] - ] - ])). - -Ltac nsatzRpv radicalmax info lparam lvar:= - nsatzR_begin; - intros; - let G := Get_goal in - ring_lookup - (PackRing ltac:(nsatzR_gen radicalmax info lparam lvar ring_subst_niter)) - [] G. - -Ltac nsatzR := nsatzRpv 6%N 1%Z (@nil R) (@nil R). -Ltac nsatzRradical radicalmax := nsatzRpv radicalmax 1%Z (@nil R) (@nil R). -Ltac nsatzRparameters lparam := nsatzRpv 6%N 1%Z lparam (@nil R). - -Tactic Notation "nsatz" := nsatzR. -Tactic Notation "nsatz" "with" "lexico" := - nsatzRpv 6%N 2%Z (@nil R) (@nil R). -Tactic Notation "nsatz" "with" "lexico" "sugar":= - nsatzRpv 6%N 3%Z (@nil R) (@nil R). -Tactic Notation "nsatz" "without" "sugar":= - nsatzRpv 6%N 0%Z (@nil R) (@nil R). - - diff --git a/plugins/nsatz/NsatzZ.v b/plugins/nsatz/NsatzZ.v deleted file mode 100644 index b57aa0ed..00000000 --- a/plugins/nsatz/NsatzZ.v +++ /dev/null @@ -1,73 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* IZR x = IZR y. -Proof IZR_eq. (* or f_equal ... *) - -Lemma nsatzZconclR: forall x y:Z, IZR x = IZR y -> x = y. -Proof eq_IZR. - -Lemma nsatzZhypnotR: forall x y:Z, x<>y -> IZR x <> IZR y. -Proof IZR_neq. - -Lemma nsatzZconclnotR: forall x y:Z, IZR x <> IZR y -> x <> y. -Proof. -intros x y H. contradict H. f_equal. assumption. -Qed. - -Ltac nsatzZtoR1 := - repeat - (match goal with - | H:(@eq Z ?x ?y) |- _ => - generalize (@nsatzZhypR _ _ H); clear H; intro H - | |- (@eq Z ?x ?y) => apply nsatzZconclR - | H:not (@eq Z ?x ?y) |- _ => - generalize (@nsatzZhypnotR _ _ H); clear H; intro H - | |- not (@eq Z ?x ?y) => apply nsatzZconclnotR - end). - -Lemma nsatzZR1: forall x y:Z, IZR(x+y) = (IZR x + IZR y)%R. -Proof plus_IZR. - -Lemma nsatzZR2: forall x y:Z, IZR(x*y) = (IZR x * IZR y)%R. -Proof mult_IZR. - -Lemma nsatzZR3: forall x y:Z, IZR(x-y) = (IZR x - IZR y)%R. -Proof. -intros; symmetry. apply Z_R_minus. -Qed. - -Lemma nsatzZR4: forall (x:Z) p, IZR(x ^ Zpos p) = (IZR x ^ nat_of_P p)%R. -Proof. -intros. rewrite pow_IZR. -do 2 f_equal. -apply Zpos_eq_Z_of_nat_o_nat_of_P. -Qed. - -Ltac nsatzZtoR2:= - repeat - (rewrite nsatzZR1 in * || - rewrite nsatzZR2 in * || - rewrite nsatzZR3 in * || - rewrite nsatzZR4 in *). - -Ltac nsatzZ_begin := - intros; - nsatzZtoR1; - nsatzZtoR2; - simpl in *. - (*cbv beta iota zeta delta [nat_of_P Pmult_nat plus mult] in *.*) - -Ltac nsatzZ := - nsatzZ_begin; (*idtac "nsatzZ_begin;";*) - nsatzR. diff --git a/plugins/nsatz/Nsatz_domain.v b/plugins/nsatz/Nsatz_domain.v deleted file mode 100644 index 5e0ae4ef..00000000 --- a/plugins/nsatz/Nsatz_domain.v +++ /dev/null @@ -1,558 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* A -> A}. -Notation "x + y" := (addition x y). -Class Multiplication (A : Type) := {multiplication : A -> A -> A}. -Notation "x * y" := (multiplication x y). -Class Subtraction (A : Type) := {subtraction : A -> A -> A}. -Notation "x - y" := (subtraction x y). -Class Opposite (A : Type) := {opposite : A -> A}. -Notation "- x" := (opposite x). - -Class Ring (R:Type) := { - ring0: R; ring1: R; - ring_plus: R->R->R; ring_mult: R->R->R; - ring_sub: R->R->R; ring_opp: R->R; - ring_ring: - ring_theory ring0 ring1 ring_plus ring_mult ring_sub - ring_opp (@eq R)}. - -Class Domain (R : Type) := { - domain_ring:> Ring R; - domain_axiom_product: - forall x y, ring_mult x y = ring0 -> x = ring0 \/ y = ring0; - domain_axiom_one_zero: ring1 <> ring0}. - -Ltac ring2 := simpl; ring. - -Section domain. - -Variable R: Type. -Variable Rd: Domain R. -Add Ring Rr: (@ring_ring R (@domain_ring R Rd)). - -Instance zero_ring : Zero R := {zero := ring0}. -Instance one_ring : One R := {one := ring1}. -Instance addition_ring : Addition R := {addition x y := ring_plus x y}. -Instance multiplication_ring : Multiplication R := {multiplication x y := ring_mult x y}. -Instance subtraction_ring : Subtraction R := {subtraction x y := ring_sub x y}. -Instance opposite_ring : Opposite R := {opposite x := ring_opp x}. - -Lemma psos_r1b: forall x y:R, x - y = 0 -> x = y. -intros x y H; replace x with ((x - y) + y); - [rewrite H | idtac]; ring2. -Qed. - -Lemma psos_r1: forall x y, x = y -> x - y = 0. -intros x y H; rewrite H; ring2. -Qed. - - -Lemma nsatzR_diff: forall x y:R, x<>y -> x - y<>0. -intros. -intro; apply H. -replace x with ((x - y) + y) by ring2. -rewrite H0; ring2. -Qed. - -(* code de Benjamin *) -Require Import ZArith. - -Definition PolZ := Pol Z. -Definition PEZ := PExpr Z. - -Definition P0Z : PolZ := @P0 Z 0%Z. - -Definition PolZadd : PolZ -> PolZ -> PolZ := - @Padd Z 0%Z Zplus Zeq_bool. - -Definition PolZmul : PolZ -> PolZ -> PolZ := - @Pmul Z 0%Z 1%Z Zplus Zmult Zeq_bool. - -Definition PolZeq := @Peq Z Zeq_bool. - -Definition norm := - @norm_aux Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool. - -Fixpoint mult_l (la : list PEZ) (lp: list PolZ) : PolZ := - match la, lp with - | a::la, p::lp => PolZadd (PolZmul (norm a) p) (mult_l la lp) - | _, _ => P0Z - end. - -Fixpoint compute_list (lla: list (list PEZ)) (lp:list PolZ) := - match lla with - | List.nil => lp - | la::lla => compute_list lla ((mult_l la lp)::lp) - end. - -Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) := - let (lla, lq) := certif in - let lp := List.map norm lpe in - PolZeq (norm qe) (mult_l lq (compute_list lla lp)). - - -(* Correction *) -Definition PhiR : list R -> PolZ -> R := - (Pphi 0 ring_plus ring_mult (gen_phiZ 0 1 ring_plus ring_mult ring_opp)). - -Definition pow (r : R) (n : nat) := pow_N 1 ring_mult r (Nnat.N_of_nat n). - -Definition PEevalR : list R -> PEZ -> R := - PEeval 0 ring_plus ring_mult ring_sub ring_opp - (gen_phiZ 0 1 ring_plus ring_mult ring_opp) - Nnat.nat_of_N pow. - -Lemma P0Z_correct : forall l, PhiR l P0Z = 0. -Proof. trivial. Qed. - -Lemma Rext: ring_eq_ext ring_plus ring_mult ring_opp eq. -apply mk_reqe. intros. rewrite H; rewrite H0; trivial. - intros. rewrite H; rewrite H0; trivial. -intros. rewrite H; trivial. Qed. - -Lemma Rset : Setoid_Theory R eq. -apply Eqsth. -Qed. - -Lemma PolZadd_correct : forall P' P l, - PhiR l (PolZadd P P') = ((PhiR l P) + (PhiR l P')). -Proof. - refine (Padd_ok Rset Rext (Rth_ARth Rset Rext (@ring_ring _ (@domain_ring _ Rd))) - (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd)))). -Qed. - -Lemma PolZmul_correct : forall P P' l, - PhiR l (PolZmul P P') = ((PhiR l P) * (PhiR l P')). -Proof. - refine (Pmul_ok Rset Rext (Rth_ARth Rset Rext (@ring_ring _ (@domain_ring _ Rd))) - (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd)))). -Qed. - -Lemma R_power_theory - : power_theory 1 ring_mult eq Nnat.nat_of_N pow. -apply mkpow_th. unfold pow. intros. rewrite Nnat.N_of_nat_of_N. trivial. Qed. - -Lemma norm_correct : - forall (l : list R) (pe : PEZ), PEevalR l pe = PhiR l (norm pe). -Proof. - intros;apply (norm_aux_spec Rset Rext (Rth_ARth Rset Rext (@ring_ring _ (@domain_ring _ Rd))) - (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd))) R_power_theory) - with (lmp:= List.nil). - compute;trivial. -Qed. - -Lemma PolZeq_correct : forall P P' l, - PolZeq P P' = true -> - PhiR l P = PhiR l P'. -Proof. - intros;apply - (Peq_ok Rset Rext (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd))));trivial. -Qed. - -Fixpoint Cond0 (A:Type) (Interp:A->R) (l:list A) : Prop := - match l with - | List.nil => True - | a::l => Interp a = 0 /\ Cond0 A Interp l - end. - -Lemma mult_l_correct : forall l la lp, - Cond0 PolZ (PhiR l) lp -> - PhiR l (mult_l la lp) = 0. -Proof. - induction la;simpl;intros;trivial. - destruct lp;trivial. - simpl in H;destruct H. - rewrite PolZadd_correct, PolZmul_correct, H, IHla;[ring2 | trivial]. -Qed. - -Lemma compute_list_correct : forall l lla lp, - Cond0 PolZ (PhiR l) lp -> - Cond0 PolZ (PhiR l) (compute_list lla lp). -Proof. - induction lla;simpl;intros;trivial. - apply IHlla;simpl;split;trivial. - apply mult_l_correct;trivial. -Qed. - -Lemma check_correct : - forall l lpe qe certif, - check lpe qe certif = true -> - Cond0 PEZ (PEevalR l) lpe -> - PEevalR l qe = 0. -Proof. - unfold check;intros l lpe qe (lla, lq) H2 H1. - apply PolZeq_correct with (l:=l) in H2. - rewrite norm_correct, H2. - apply mult_l_correct. - apply compute_list_correct. - clear H2 lq lla qe;induction lpe;simpl;trivial. - simpl in H1;destruct H1. - rewrite <- norm_correct;auto. -Qed. - -(* fin du code de Benjamin *) - -Lemma pow_not_zero: forall p n, pow p n = 0 -> p = 0. -induction n. unfold pow; simpl. intros. absurd (1 = 0). -simpl. apply domain_axiom_one_zero. - trivial. replace (pow p (S n)) with (p * (pow p n)). intros. -case (@domain_axiom_product _ _ _ _ H). trivial. trivial. -unfold pow; simpl. -clear IHn. induction n; try ring2. simpl. - rewrite pow_pos_Psucc. trivial. exact Rset. - intros. rewrite H; rewrite H0; trivial. - intros. ring2. intros. ring2. Qed. - -Lemma Rdomain_pow: forall c p r, ~c= 0 -> c * (pow p r)= 0 -> p = ring0. -intros. case (@domain_axiom_product _ _ _ _ H0). intros; absurd (c = 0); auto. -intros. apply pow_not_zero with r. trivial. Qed. - -Definition R2:= 1 + 1. - -Fixpoint IPR p {struct p}: R := - match p with - xH => 1 - | xO xH => 1 + 1 - | xO p1 => R2 + (IPR p1) - | xI xH => 1 + (1 + 1) - | xI p1 => 1 + (R2 * (IPR p1)) - end. - -Definition IZR1 z := - match z with Z0 => 0 - | Zpos p => IPR p - | Zneg p => -(IPR p) - end. - -Fixpoint interpret3 t fv {struct t}: R := - match t with - | (PEadd t1 t2) => - let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (v1 + v2) - | (PEmul t1 t2) => - let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (v1 * v2) - | (PEsub t1 t2) => - let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (v1 - v2) - | (PEopp t1) => - let v1 := interpret3 t1 fv in (- v1) - | (PEpow t1 t2) => - let v1 := interpret3 t1 fv in pow v1 (Nnat.nat_of_N t2) - | (PEc t1) => (IZR1 t1) - | (PEX n) => List.nth (pred (nat_of_P n)) fv 0 - end. - - -End domain. - -Ltac equalities_to_goal := - lazymatch goal with - | H: (@eq _ ?x 0) |- _ => try revert H - | H: (@eq _ 0 ?x) |- _ => - try generalize (sym_equal H); clear H - | H: (@eq _ ?x ?y) |- _ => - try generalize (@psos_r1 _ _ _ _ H); clear H - end. - -Ltac nsatz_domain_begin tacsimpl:= - intros; - try apply (@psos_r1b _ _); - repeat equalities_to_goal; - tacsimpl. - -Ltac generalise_eq_hyps:= - repeat - (match goal with - |h : (?p = ?q)|- _ => revert h - end). - -Ltac lpol_goal t := - match t with - | ?a = ring0 -> ?b => - let r:= lpol_goal b in - constr:(a::r) - | ?a = ring0 => constr:(a::nil) - end. - -(* lp est incluse dans fv. La met en tete. *) - -Ltac parametres_en_tete fv lp := - match fv with - | (@nil _) => lp - | (@cons _ ?x ?fv1) => - let res := AddFvTail x lp in - parametres_en_tete fv1 res - end. - -Ltac append1 a l := - match l with - | (@nil _) => constr:(cons a l) - | (cons ?x ?l) => let l' := append1 a l in constr:(cons x l') - end. - -Ltac rev l := - match l with - |(@nil _) => l - | (cons ?x ?l) => let l' := rev l in append1 x l' - end. - -Ltac nsatz_call_n info nparam p rr lp kont := - let ll := constr:(PEc info :: PEc nparam :: PEpow p rr :: lp) in - nsatz_compute ll; - match goal with - | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ => - intros _; - set (lci:=lci0); - set (lq:=lq0); - kont c rr lq lci - end. - -Ltac nsatz_call radicalmax info nparam p lp kont := - let rec try_n n := - lazymatch n with - | 0%N => fail - | _ => -(* idtac "Trying power: " n;*) - (let r := eval compute in (Nminus radicalmax (Npred n)) in - nsatz_call_n info nparam p r lp kont) || - let n' := eval compute in (Npred n) in try_n n' - end in - try_n radicalmax. - - -Set Implicit Arguments. -Class Cclosed_seq T (l:list T) := {}. -Instance Iclosed_nil T : Cclosed_seq (T:=T) nil. -Instance Iclosed_cons T t l `{Cclosed_seq (T:=T) l} : Cclosed_seq (T:=T) (t::l). - -Class Cfind_at (R:Type) (b:R) (l:list R) (i:nat) := {}. -Instance Ifind0 (R:Type) (b:R) l: Cfind_at b (b::l) 0. -Instance IfindS (R:Type) (b2 b1:R) l i `{Cfind_at R b1 l i} : Cfind_at b1 (b2::l) (S i) | 1. -Definition Ifind0' := Ifind0. -Definition IfindS' := IfindS. - -Definition li_find_at (R:Type) (b:R) l i `{Cfind_at R b l i} {H:Cclosed_seq (T:=R) l} := (l,i). - -Class Creify (R:Type) (e:PExpr Z) (l:list R) (b:R) := {}. -Instance Ireify_zero (R:Type) (Rd:Domain R) l : Creify (PEc 0%Z) l ring0. -Instance Ireify_one (R:Type) (Rd:Domain R) l : Creify (PEc 1%Z) l ring1. -Instance Ireify_plus (R:Type) (Rd:Domain R) e1 l b1 e2 b2 `{Creify R e1 l b1} `{Creify R e2 l b2} - : Creify (PEadd e1 e2) l (ring_plus b1 b2). -Instance Ireify_mult (R:Type) (Rd:Domain R) e1 l b1 e2 b2 `{Creify R e1 l b1} `{Creify R e2 l b2} - : Creify (PEmul e1 e2) l (ring_mult b1 b2). -Instance Ireify_sub (R:Type) (Rd:Domain R) e1 l b1 e2 b2 `{Creify R e1 l b1} `{Creify R e2 l b2} - : Creify (PEsub e1 e2) l (ring_sub b1 b2). -Instance Ireify_opp (R:Type) (Rd:Domain R) e1 l b1 `{Creify R e1 l b1} - : Creify (PEopp e1) l (ring_opp b1). -Instance Ireify_var (R:Type) b l i `{Cfind_at R b l i} - : Creify (PEX _ (P_of_succ_nat i)) l b | 100. - - -Class Creifylist (R:Type) (le:list (PExpr Z)) (l:list R) (lb:list R) := {}. -Instance Creify_nil (R:Type) l : Creifylist nil l (@nil R). -Instance Creify_cons (R:Type) e1 l b1 le2 lb2 `{Creify R e1 l b1} `{Creifylist R le2 l lb2} - : Creifylist (e1::le2) l (b1::lb2). - -Definition li_reifyl (R:Type) le l lb `{Creifylist R le l lb} - {H:Cclosed_seq (T:=R) l} := (l,le). - -Unset Implicit Arguments. - -Ltac lterm_goal g := - match g with - ?b1 = ?b2 => constr:(b1::b2::nil) - | ?b1 = ?b2 -> ?g => let l := lterm_goal g in constr:(b1::b2::l) - end. - -Ltac reify_goal l le lb:= - match le with - nil => idtac - | ?e::?le1 => - match lb with - ?b::?lb1 => - let x := fresh "B" in - set (x:= b) at 1; - change x with (@interpret3 _ _ e l); - clear x; - reify_goal l le1 lb1 - end - end. - -Ltac get_lpol g := - match g with - (interpret3 _ _ ?p _) = _ => constr:(p::nil) - | (interpret3 _ _ ?p _) = _ -> ?g => - let l := get_lpol g in constr:(p::l) - end. - -Ltac nsatz_domain_generic radicalmax info lparam lvar tacsimpl Rd := - match goal with - |- ?g => let lb := lterm_goal g in - (*idtac "lb"; idtac lb;*) - match eval red in (li_reifyl (lb:=lb)) with - | (?fv, ?le) => - let fv := match lvar with - (@nil _) => fv - | _ => lvar - end in - (* idtac "variables:";idtac fv;*) - let nparam := eval compute in (Z_of_nat (List.length lparam)) in - let fv := parametres_en_tete fv lparam in - (*idtac "variables:"; idtac fv; - idtac "nparam:"; idtac nparam;*) - match eval red in (li_reifyl (l:=fv) (lb:=lb)) with - | (?fv, ?le) => - idtac "variables:";idtac fv; - reify_goal fv le lb; - match goal with - |- ?g => - let lp := get_lpol g in - let lpol := eval compute in (List.rev lp) in - (*idtac "polynomes:"; idtac lpol;*) - tacsimpl; intros; - - let SplitPolyList kont := - match lpol with - | ?p2::?lp2 => kont p2 lp2 - | _ => idtac "polynomial not in the ideal" - end in - tacsimpl; - SplitPolyList ltac:(fun p lp => - set (p21:=p) ; - set (lp21:=lp); - (*idtac "lp:"; idtac lp; *) - nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => - set (q := PEmul c (PEpow p21 r)); - let Hg := fresh "Hg" in - assert (Hg:check lp21 q (lci,lq) = true); - [ (vm_compute;reflexivity) || idtac "invalid nsatz certificate" - | let Hg2 := fresh "Hg" in - assert (Hg2: interpret3 _ _ q fv = ring0); - [ tacsimpl; - apply (@check_correct _ Rd fv lp21 q (lci,lq) Hg); - tacsimpl; - repeat (split;[assumption|idtac]); exact I - | simpl in Hg2; tacsimpl; - apply Rdomain_pow with (interpret3 _ _ c fv) (Nnat.nat_of_N r); tacsimpl; - [ apply domain_axiom_one_zero || idtac "could not prove discrimination result" - | exact Hg2] - ] - ] -) -) -end end end end . - -Ltac nsatz_domainpv radicalmax info lparam lvar tacsimpl rd:= - nsatz_domain_begin tacsimpl; - nsatz_domain_generic radicalmax info lparam lvar tacsimpl rd. - -Ltac nsatz_domain:= - intros; - match goal with - |- (@eq ?r _ _ ) => - let a := constr:(@Ireify_zero _ _ (@nil r)) in - match a with - (@Ireify_zero _ ?rd _) => - nsatz_domainpv 6%N 1%Z (@nil r) (@nil r) ltac:(simpl) rd - end - end. - - - -(* Dans Z *) -Instance Zri : Ring Z := { - ring0 := 0%Z; - ring1 := 1%Z; - ring_plus := Zplus; - ring_mult := Zmult; - ring_sub := Zminus; - ring_opp := Zopp; - ring_ring := Zth}. - -Lemma Zaxiom_one_zero: 1%Z <> 0%Z. -discriminate. -Qed. - -Instance Zdi : Domain Z := { - domain_ring := Zri; - domain_axiom_product := Zmult_integral; - domain_axiom_one_zero := Zaxiom_one_zero}. - - -Ltac simplZ:= - simpl; -replace 0%Z with (@ring0 _ (@domain_ring _ Zdi));[idtac|reflexivity]; -replace 1%Z with (@ring1 _ (@domain_ring _ Zdi));[idtac|reflexivity]; -replace Zplus with (@ring_plus _ (@domain_ring _ Zdi));[idtac|reflexivity]; -replace Zmult with (@ring_mult _ (@domain_ring _ Zdi));[idtac|reflexivity]; -replace Zminus with (@ring_sub _ (@domain_ring _ Zdi));[idtac|reflexivity]; -replace Zopp with (@ring_opp _ (@domain_ring _ Zdi));[idtac|reflexivity]. - -Ltac nsatz_domainZ:= nsatz_domainpv 6%N 1%Z (@nil Z) (@nil Z) ltac:simplZ Zdi. - - -(* Dans R *) -Require Import Reals. -Require Import RealField. - -Instance Rri : Ring R := { - ring0 := 0%R; - ring1 := 1%R; - ring_plus := Rplus; - ring_mult := Rmult; - ring_sub := Rminus; - ring_opp := Ropp; - ring_ring := RTheory}. - -Lemma Raxiom_one_zero: 1%R <> 0%R. -discrR. -Qed. - -Instance Rdi : Domain R := { - domain_ring := Rri; - domain_axiom_product := Rmult_integral; - domain_axiom_one_zero := Raxiom_one_zero}. - - -Ltac simplR:= - simpl; -replace 0%R with (@ring0 _ (@domain_ring _ Rdi));[idtac|reflexivity]; -replace 1%R with (@ring1 _ (@domain_ring _ Rdi));[idtac|reflexivity]; -replace Rplus with (@ring_plus _ (@domain_ring _ Rdi));[idtac|reflexivity]; -replace Rmult with (@ring_mult _ (@domain_ring _ Rdi));[idtac|reflexivity]; -replace Rminus with (@ring_sub _ (@domain_ring _ Rdi));[idtac|reflexivity]; -replace Ropp with (@ring_opp _ (@domain_ring _ Rdi));[idtac|reflexivity]. - -Ltac nsatz_domainR:= nsatz_domainpv 6%N 1%Z (@List.nil R) (@List.nil R) ltac:simplR Rdi. diff --git a/plugins/nsatz/vo.itarget b/plugins/nsatz/vo.itarget index 4af4786d..06fc8834 100644 --- a/plugins/nsatz/vo.itarget +++ b/plugins/nsatz/vo.itarget @@ -1,3 +1 @@ -NsatzR.vo -Nsatz_domain.vo -NsatzZ.vo +Nsatz.vo -- cgit v1.2.3