diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/nsatz/NsatzR.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/nsatz/NsatzR.v')
-rw-r--r-- | plugins/nsatz/NsatzR.v | 407 |
1 files changed, 407 insertions, 0 deletions
diff --git a/plugins/nsatz/NsatzR.v b/plugins/nsatz/NsatzR.v new file mode 100644 index 00000000..c68c9584 --- /dev/null +++ b/plugins/nsatz/NsatzR.v @@ -0,0 +1,407 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* + Tactic nsatz: proofs of polynomials equalities with variables in R. + Uses Hilbert Nullstellensatz and Buchberger algorithm. + Thanks to B.Gregoire and L.Thery for help on ring tactic, + and to B.Barras for modularization of the ocaml code. + Example: see test-suite/success/Nsatz.v + L.Pottier, june 2010 +*) + +Require Import List. +Require Import Setoid. +Require Import BinPos. +Require Import BinList. +Require Import Znumtheory. +Require Import RealField Rdefinitions Rfunctions RIneq DiscrR. +Require Import Ring_polynom Ring_tac InitialRing. + +Declare ML Module "nsatz_plugin". + +Local Open Scope R_scope. + +Lemma psos_r1b: forall x y, x - y = 0 -> 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). + + |