diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:16 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:16 +0000 |
| commit | fc2613e871dffffa788d90044a81598f671d0a3b (patch) | |
| tree | f6f308b3d6b02e1235446b2eb4a2d04b135a0462 /plugins/micromega | |
| parent | f93f073df630bb46ddd07802026c0326dc72dafd (diff) | |
ZArith + other : favor the use of modern names instead of compat notations
- For instance, refl_equal --> eq_refl
- Npos, Zpos, Zneg now admit more uniform qualified aliases
N.pos, Z.pos, Z.neg.
- A new module BinInt.Pos2Z with results about injections from
positive to Z
- A result about Z.pow pushed in the generic layer
- Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
- Using tactic Z.le_elim instead of Zle_lt_or_eq
- Some cleanup in ring, field, micromega
(use of "Equivalence", "Proper" ...)
- Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
- In ZMake and ZMake, functor parameters are now named NN and ZZ
instead of N and Z for avoiding confusions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/Env.v | 151 | ||||
| -rw-r--r-- | plugins/micromega/EnvRing.v | 1179 | ||||
| -rw-r--r-- | plugins/micromega/MExtraction.v | 2 | ||||
| -rw-r--r-- | plugins/micromega/Psatz.v | 6 | ||||
| -rw-r--r-- | plugins/micromega/QMicromega.v | 8 | ||||
| -rw-r--r-- | plugins/micromega/RMicromega.v | 28 | ||||
| -rw-r--r-- | plugins/micromega/RingMicromega.v | 48 | ||||
| -rw-r--r-- | plugins/micromega/ZCoeff.v | 14 | ||||
| -rw-r--r-- | plugins/micromega/ZMicromega.v | 214 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 21 |
10 files changed, 621 insertions, 1050 deletions
diff --git a/plugins/micromega/Env.v b/plugins/micromega/Env.v index 5f6c60beb..2ebdf3072 100644 --- a/plugins/micromega/Env.v +++ b/plugins/micromega/Env.v @@ -12,10 +12,9 @@ (* *) (************************************************************************) -Require Import ZArith. -Require Import Coq.Arith.Max. -Require Import List. +Require Import BinInt List. Set Implicit Arguments. +Local Open Scope positive_scope. Section S. @@ -23,154 +22,78 @@ Section S. Definition Env := positive -> D. - Definition jump (j:positive) (e:Env) := fun x => e (Pplus x j). + Definition jump (j:positive) (e:Env) := fun x => e (x+j). - Definition nth (n:positive) (e : Env ) := e n. + Definition nth (n:positive) (e:Env) := e n. - Definition hd (x:D) (e: Env) := nth xH e. + Definition hd (e:Env) := nth 1 e. - Definition tail (e: Env) := jump xH e. + Definition tail (e:Env) := jump 1 e. - Lemma psucc : forall p, (match p with - | xI y' => xO (Psucc y') - | xO y' => xI y' - | 1%positive => 2%positive - end) = (p+1)%positive. + Lemma jump_add i j l x : jump (i + j) l x = jump i (jump j l) x. Proof. - destruct p. - auto with zarith. - rewrite xI_succ_xO. - auto with zarith. - reflexivity. + unfold jump. f_equal. apply Pos.add_assoc. Qed. - Lemma jump_Pplus : forall i j l, - forall x, jump (i + j) l x = jump i (jump j l) x. - Proof. - unfold jump. - intros. - rewrite Pplus_assoc. - reflexivity. - Qed. - - Lemma jump_simpl : forall p l, - forall x, jump p l x = + Lemma jump_simpl p l x : + jump p l x = match p with | xH => tail l x | xO p => jump p (jump p l) x | xI p => jump p (jump p (tail l)) x end. Proof. - destruct p ; unfold tail ; intros ; repeat rewrite <- jump_Pplus. - (* xI p = p + p + 1 *) - rewrite xI_succ_xO. - rewrite Pplus_diag. - rewrite <- Pplus_one_succ_r. - reflexivity. - (* xO p = p + p *) - rewrite Pplus_diag. - reflexivity. - reflexivity. + destruct p; unfold tail; rewrite <- ?jump_add; f_equal; + now rewrite Pos.add_diag. Qed. - Ltac jump_s := - repeat - match goal with - | |- context [jump xH ?e] => rewrite (jump_simpl xH) - | |- context [jump (xO ?p) ?e] => rewrite (jump_simpl (xO p)) - | |- context [jump (xI ?p) ?e] => rewrite (jump_simpl (xI p)) - end. - - Lemma jump_tl : forall j l, forall x, tail (jump j l) x = jump j (tail l) x. + Lemma jump_tl j l x : tail (jump j l) x = jump j (tail l) x. Proof. - unfold tail. - intros. - repeat rewrite <- jump_Pplus. - rewrite Pplus_comm. - reflexivity. + unfold tail. rewrite <- !jump_add. f_equal. apply Pos.add_comm. Qed. - Lemma jump_Psucc : forall j l, - forall x, (jump (Psucc j) l x) = (jump 1 (jump j l) x). + Lemma jump_succ j l x : jump (Pos.succ j) l x = jump 1 (jump j l) x. Proof. - intros. - rewrite <- jump_Pplus. - rewrite Pplus_one_succ_r. - rewrite Pplus_comm. - reflexivity. + rewrite <- jump_add. f_equal. symmetry. apply Pos.add_1_l. Qed. - Lemma jump_Pdouble_minus_one : forall i l, - forall x, (jump (Pdouble_minus_one i) (tail l)) x = (jump i (jump i l)) x. + Lemma jump_pred_double i l x : + jump (Pos.pred_double i) (tail l) x = jump i (jump i l) x. Proof. - unfold tail. - intros. - repeat rewrite <- jump_Pplus. - rewrite <- Pplus_one_succ_r. - rewrite Psucc_o_double_minus_one_eq_xO. - rewrite Pplus_diag. - reflexivity. + unfold tail. rewrite <- !jump_add. f_equal. + now rewrite Pos.add_1_r, Pos.succ_pred_double, Pos.add_diag. Qed. - Lemma jump_x0_tail : forall p l, forall x, jump (xO p) (tail l) x = jump (xI p) l x. - Proof. - intros. - unfold jump. - unfold tail. - unfold jump. - rewrite <- Pplus_assoc. - simpl. - reflexivity. - Qed. - - Lemma nth_spec : forall p l x, + Lemma nth_spec p l : nth p l = match p with - | xH => hd x l + | xH => hd l | xO p => nth p (jump p l) | xI p => nth p (jump p (tail l)) end. Proof. - unfold nth. - destruct p. - intros. - unfold jump, tail. - unfold jump. - rewrite Pplus_diag. - rewrite xI_succ_xO. - simpl. - reflexivity. - unfold jump. - rewrite Pplus_diag. - reflexivity. - unfold hd. - unfold nth. - reflexivity. + unfold hd, nth, tail, jump. + destruct p; f_equal; now rewrite Pos.add_diag. Qed. - - Lemma nth_jump : forall p l x, nth p (tail l) = hd x (jump p l). + Lemma nth_jump p l : nth p (tail l) = hd (jump p l). Proof. - unfold tail. - unfold hd. - unfold jump. - unfold nth. - intros. - rewrite Pplus_comm. - reflexivity. + unfold hd, nth, tail, jump. f_equal. apply Pos.add_comm. Qed. - Lemma nth_Pdouble_minus_one : - forall p l, nth (Pdouble_minus_one p) (tail l) = nth p (jump p l). + Lemma nth_pred_double p l : + nth (Pos.pred_double p) (tail l) = nth p (jump p l). Proof. - intros. - unfold tail. - unfold nth, jump. - rewrite Pplus_diag. - rewrite <- Psucc_o_double_minus_one_eq_xO. - rewrite Pplus_one_succ_r. - reflexivity. + unfold nth, tail, jump. f_equal. + now rewrite Pos.add_1_r, Pos.succ_pred_double, Pos.add_diag. Qed. End S. +Ltac jump_simpl := + repeat + match goal with + | |- appcontext [jump xH] => rewrite (jump_simpl xH) + | |- appcontext [jump (xO ?p)] => rewrite (jump_simpl (xO p)) + | |- appcontext [jump (xI ?p)] => rewrite (jump_simpl (xI p)) + end. diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index 309ebdef1..c404919af 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -11,15 +11,10 @@ Set Implicit Arguments. -Require Import Setoid. -Require Import BinList. -Require Import Env. -Require Import BinPos. -Require Import BinNat. -Require Import BinInt. +Require Import Setoid Morphisms Env BinPos BinNat BinInt. Require Export Ring_theory. -Open Local Scope positive_scope. +Local Open Scope positive_scope. Import RingSyntax. Section MakeRingPol. @@ -30,7 +25,7 @@ Section MakeRingPol. Variable req : R -> R -> Prop. (* Ring properties *) - Variable Rsth : Setoid_Theory R req. + Variable Rsth : Equivalence req. Variable Reqe : ring_eq_ext radd rmul ropp req. Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req. @@ -42,35 +37,55 @@ Section MakeRingPol. Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi. - (* Power coefficients *) + (* Power coefficients *) Variable Cpow : Type. Variable Cp_phi : N -> Cpow. Variable rpow : R -> Cpow -> R. Variable pow_th : power_theory rI rmul req Cp_phi rpow. - (* R notations *) Notation "0" := rO. Notation "1" := rI. - Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y). - Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). - Notation "x == y" := (req x y). + Infix "+" := radd. Infix "*" := rmul. + Infix "-" := rsub. Notation "- x" := (ropp x). + Infix "==" := req. + Infix "^" := (pow_pos rmul). (* C notations *) - Notation "x +! y" := (cadd x y). Notation "x *! y " := (cmul x y). - Notation "x -! y " := (csub x y). Notation "-! x" := (copp x). - Notation " x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x). - - (* Usefull tactics *) - Add Setoid R req Rsth as R_set1. - Ltac rrefl := gen_reflexivity Rsth. - Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. - Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. + Infix "+!" := cadd. Infix "*!" := cmul. + Infix "-! " := csub. Notation "-! x" := (copp x). + Infix "?=!" := ceqb. Notation "[ x ]" := (phi x). + + (* Useful tactics *) + Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. + Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac rsimpl := gen_srewrite Rsth Reqe ARth. + Ltac add_push := gen_add_push radd Rsth Reqe ARth. Ltac mul_push := gen_mul_push rmul Rsth Reqe ARth. + Ltac add_permut_rec t := + match t with + | ?x + ?y => add_permut_rec y || add_permut_rec x + | _ => add_push t; apply (Radd_ext Reqe); [|reflexivity] + end. + + Ltac add_permut := + repeat (reflexivity || + match goal with |- ?t == _ => add_permut_rec t end). + + Ltac mul_permut_rec t := + match t with + | ?x * ?y => mul_permut_rec y || mul_permut_rec x + | _ => mul_push t; apply (Rmul_ext Reqe); [|reflexivity] + end. + + Ltac mul_permut := + repeat (reflexivity || + match goal with |- ?t == _ => mul_permut_rec t end). + + (* Definition of multivariable polynomials with coefficients in C : Type [Pol] represents [X1 ... Xn]. The representation is Horner's where a [n] variable polynomial @@ -117,19 +132,19 @@ Section MakeRingPol. | _, _ => false end. - Notation " P ?== P' " := (Peq P P'). + Infix "?==" := Peq. Definition mkPinj j P := match P with | Pc _ => P - | Pinj j' Q => Pinj ((j + j'):positive) Q + | Pinj j' Q => Pinj (j + j') Q | _ => Pinj j P end. Definition mkPinj_pred j P:= match j with | xH => P - | xO j => Pinj (Pdouble_minus_one j) P + | xO j => Pinj (Pos.pred_double j) P | xI j => Pinj (xO j) P end. @@ -157,14 +172,14 @@ Section MakeRingPol. (** Addition et subtraction *) - Fixpoint PaddC (P:Pol) (c:C) {struct P} : Pol := + Fixpoint PaddC (P:Pol) (c:C) : Pol := match P with | Pc c1 => Pc (c1 +! c) | Pinj j Q => Pinj j (PaddC Q c) | PX P i Q => PX P i (PaddC Q c) end. - Fixpoint PsubC (P:Pol) (c:C) {struct P} : Pol := + Fixpoint PsubC (P:Pol) (c:C) : Pol := match P with | Pc c1 => Pc (c1 -! c) | Pinj j Q => Pinj j (PsubC Q c) @@ -176,11 +191,11 @@ Section MakeRingPol. Variable Pop : Pol -> Pol -> Pol. Variable Q : Pol. - Fixpoint PaddI (j:positive) (P:Pol){struct P} : Pol := + Fixpoint PaddI (j:positive) (P:Pol) : Pol := match P with | Pc c => mkPinj j (PaddC Q c) | Pinj j' Q' => - match ZPminus j' j with + match Z.pos_sub j' j with | Zpos k => mkPinj j (Pop (Pinj k Q') Q) | Z0 => mkPinj j (Pop Q' Q) | Zneg k => mkPinj j' (PaddI k Q') @@ -188,16 +203,16 @@ Section MakeRingPol. | PX P i Q' => match j with | xH => PX P i (Pop Q' Q) - | xO j => PX P i (PaddI (Pdouble_minus_one j) Q') + | xO j => PX P i (PaddI (Pos.pred_double j) Q') | xI j => PX P i (PaddI (xO j) Q') end end. - Fixpoint PsubI (j:positive) (P:Pol){struct P} : Pol := + Fixpoint PsubI (j:positive) (P:Pol) : Pol := match P with | Pc c => mkPinj j (PaddC (--Q) c) | Pinj j' Q' => - match ZPminus j' j with + match Z.pos_sub j' j with | Zpos k => mkPinj j (Pop (Pinj k Q') Q) | Z0 => mkPinj j (Pop Q' Q) | Zneg k => mkPinj j' (PsubI k Q') @@ -205,41 +220,41 @@ Section MakeRingPol. | PX P i Q' => match j with | xH => PX P i (Pop Q' Q) - | xO j => PX P i (PsubI (Pdouble_minus_one j) Q') + | xO j => PX P i (PsubI (Pos.pred_double j) Q') | xI j => PX P i (PsubI (xO j) Q') end end. Variable P' : Pol. - Fixpoint PaddX (i':positive) (P:Pol) {struct P} : Pol := + Fixpoint PaddX (i':positive) (P:Pol) : Pol := match P with | Pc c => PX P' i' P | Pinj j Q' => match j with | xH => PX P' i' Q' - | xO j => PX P' i' (Pinj (Pdouble_minus_one j) Q') + | xO j => PX P' i' (Pinj (Pos.pred_double j) Q') | xI j => PX P' i' (Pinj (xO j) Q') end | PX P i Q' => - match ZPminus i i' with + match Z.pos_sub i i' with | Zpos k => mkPX (Pop (PX P k P0) P') i' Q' | Z0 => mkPX (Pop P P') i Q' | Zneg k => mkPX (PaddX k P) i Q' end end. - Fixpoint PsubX (i':positive) (P:Pol) {struct P} : Pol := + Fixpoint PsubX (i':positive) (P:Pol) : Pol := match P with | Pc c => PX (--P') i' P | Pinj j Q' => match j with | xH => PX (--P') i' Q' - | xO j => PX (--P') i' (Pinj (Pdouble_minus_one j) Q') + | xO j => PX (--P') i' (Pinj (Pos.pred_double j) Q') | xI j => PX (--P') i' (Pinj (xO j) Q') end | PX P i Q' => - match ZPminus i i' with + match Z.pos_sub i i' with | Zpos k => mkPX (Pop (PX P k P0) P') i' Q' | Z0 => mkPX (Pop P P') i Q' | Zneg k => mkPX (PsubX k P) i Q' @@ -259,18 +274,18 @@ Section MakeRingPol. | Pinj j Q => match j with | xH => PX P' i' (Padd Q Q') - | xO j => PX P' i' (Padd (Pinj (Pdouble_minus_one j) Q) Q') + | xO j => PX P' i' (Padd (Pinj (Pos.pred_double j) Q) Q') | xI j => PX P' i' (Padd (Pinj (xO j) Q) Q') end | PX P i Q => - match ZPminus i i' with + match Z.pos_sub i i' with | Zpos k => mkPX (Padd (PX P k P0) P') i' (Padd Q Q') | Z0 => mkPX (Padd P P') i (Padd Q Q') | Zneg k => mkPX (PaddX Padd P' k P) i (Padd Q Q') end end end. - Notation "P ++ P'" := (Padd P P'). + Infix "++" := Padd. Fixpoint Psub (P P': Pol) {struct P'} : Pol := match P' with @@ -282,22 +297,22 @@ Section MakeRingPol. | Pinj j Q => match j with | xH => PX (--P') i' (Psub Q Q') - | xO j => PX (--P') i' (Psub (Pinj (Pdouble_minus_one j) Q) Q') + | xO j => PX (--P') i' (Psub (Pinj (Pos.pred_double j) Q) Q') | xI j => PX (--P') i' (Psub (Pinj (xO j) Q) Q') end | PX P i Q => - match ZPminus i i' with + match Z.pos_sub i i' with | Zpos k => mkPX (Psub (PX P k P0) P') i' (Psub Q Q') | Z0 => mkPX (Psub P P') i (Psub Q Q') | Zneg k => mkPX (PsubX Psub P' k P) i (Psub Q Q') end end end. - Notation "P -- P'" := (Psub P P'). + Infix "--" := Psub. (** Multiplication *) - Fixpoint PmulC_aux (P:Pol) (c:C) {struct P} : Pol := + Fixpoint PmulC_aux (P:Pol) (c:C) : Pol := match P with | Pc c' => Pc (c' *! c) | Pinj j Q => mkPinj j (PmulC_aux Q c) @@ -311,11 +326,11 @@ Section MakeRingPol. Section PmulI. Variable Pmul : Pol -> Pol -> Pol. Variable Q : Pol. - Fixpoint PmulI (j:positive) (P:Pol) {struct P} : Pol := + Fixpoint PmulI (j:positive) (P:Pol) : Pol := match P with | Pc c => mkPinj j (PmulC Q c) | Pinj j' Q' => - match ZPminus j' j with + match Z.pos_sub j' j with | Zpos k => mkPinj j (Pmul (Pinj k Q') Q) | Z0 => mkPinj j (Pmul Q' Q) | Zneg k => mkPinj j' (PmulI k Q') @@ -323,13 +338,12 @@ Section MakeRingPol. | PX P' i' Q' => match j with | xH => mkPX (PmulI xH P') i' (Pmul Q' Q) - | xO j' => mkPX (PmulI j P') i' (PmulI (Pdouble_minus_one j') Q') + | xO j' => mkPX (PmulI j P') i' (PmulI (Pos.pred_double j') Q') | xI j' => mkPX (PmulI j P') i' (PmulI (xO j') Q') end end. End PmulI. -(* A symmetric version of the multiplication *) Fixpoint Pmul (P P'' : Pol) {struct P''} : Pol := match P'' with @@ -342,7 +356,7 @@ Section MakeRingPol. let QQ' := match j with | xH => Pmul Q Q' - | xO j => Pmul (Pinj (Pdouble_minus_one j) Q) Q' + | xO j => Pmul (Pinj (Pos.pred_double j) Q) Q' | xI j => Pmul (Pinj (xO j) Q) Q' end in mkPX (Pmul P P') i' QQ' @@ -355,25 +369,7 @@ Section MakeRingPol. end end. -(* Non symmetric *) -(* - Fixpoint Pmul_aux (P P' : Pol) {struct P'} : Pol := - match P' with - | Pc c' => PmulC P c' - | Pinj j' Q' => PmulI Pmul_aux Q' j' P - | PX P' i' Q' => - (mkPX (Pmul_aux P P') i' P0) ++ (PmulI Pmul_aux Q' xH P) - end. - - Definition Pmul P P' := - match P with - | Pc c => PmulC P' c - | Pinj j Q => PmulI Pmul_aux Q j P' - | PX P i Q => - (mkPX (Pmul_aux P P') i P0) ++ (PmulI Pmul_aux Q xH P') - end. -*) - Notation "P ** P'" := (Pmul P P'). + Infix "**" := Pmul. Fixpoint Psquare (P:Pol) : Pol := match P with @@ -388,26 +384,35 @@ Section MakeRingPol. (** Monomial **) + (** A monomial is X1^k1...Xi^ki. Its representation + is a simplified version of the polynomial representation: + + - [mon0] correspond to the polynom [P1]. + - [(zmon j M)] corresponds to [(Pinj j ...)], + i.e. skip j variable indices. + - [(vmon i M)] is X^i*M with X the current variable, + its corresponds to (PX P1 i ...)] + *) + Inductive Mon: Set := - mon0: Mon + | mon0: Mon | zmon: positive -> Mon -> Mon | vmon: positive -> Mon -> Mon. - Fixpoint Mphi(l:Env R) (M: Mon) {struct M} : R := + Fixpoint Mphi (l:Env R)(M: Mon) : R := match M with - mon0 => rI - | zmon j M1 => Mphi (jump j l) M1 - | vmon i M1 => - let x := hd 0 l in - let xi := pow_pos rmul x i in - (Mphi (tail l) M1) * xi + | mon0 => rI + | zmon j M1 => Mphi (jump j l) M1 + | vmon i M1 => Mphi (tail l) M1 * (hd l) ^ i end. + Notation "M @@ l" := (Mphi l M) (at level 10, no associativity). + Definition mkZmon j M := match M with mon0 => mon0 | _ => zmon j M end. Definition zmon_pred j M := - match j with xH => M | _ => mkZmon (Ppred j) M end. + match j with xH => M | _ => mkZmon (Pos.pred j) M end. Definition mkVmon i M := match M with @@ -416,7 +421,7 @@ Section MakeRingPol. | vmon i' m => vmon (i+i') m end. - Fixpoint MFactor (P: Pol) (M: Mon) {struct P}: Pol * Pol := + Fixpoint MFactor (P: Pol) (M: Mon) : Pol * Pol := match P, M with _, mon0 => (Pc cO, P) | Pc _, _ => (P, Pc cO) @@ -453,7 +458,7 @@ Section MakeRingPol. | _ => Some (Padd Q1 (Pmul P2 R1)) end. - Fixpoint PNSubst1 (P1: Pol) (M1: Mon) (P2: Pol) (n: nat) {struct n}: Pol := + Fixpoint PNSubst1 (P1: Pol) (M1: Mon) (P2: Pol) (n: nat) : Pol := match POneSubst P1 M1 P2 with Some P3 => match n with S n1 => PNSubst1 P3 M1 P2 n1 | _ => P3 end | _ => P1 @@ -465,14 +470,13 @@ Section MakeRingPol. | _ => None end. - Fixpoint PSubstL1 (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}: - Pol := + Fixpoint PSubstL1 (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) : Pol := match LM1 with cons (M1,P2) LM2 => PSubstL1 (PNSubst1 P1 M1 P2 n) LM2 n | _ => P1 end. - Fixpoint PSubstL (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}: option Pol := + Fixpoint PSubstL (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) : option Pol := match LM1 with cons (M1,P2) LM2 => match PNSubst P1 M1 P2 n with @@ -482,7 +486,7 @@ Section MakeRingPol. | _ => None end. - Fixpoint PNSubstL (P1: Pol) (LM1: list (Mon * Pol)) (m n: nat) {struct m}: Pol := + Fixpoint PNSubstL (P1: Pol) (LM1: list (Mon * Pol)) (m n: nat) : Pol := match PSubstL P1 LM1 n with Some P3 => match m with S m1 => PNSubstL P3 LM1 m1 n | _ => P3 end | _ => P1 @@ -490,146 +494,112 @@ Section MakeRingPol. (** Evaluation of a polynomial towards R *) - Fixpoint Pphi(l:Env R) (P:Pol) {struct P} : R := + Fixpoint Pphi(l:Env R) (P:Pol) : R := match P with | Pc c => [c] | Pinj j Q => Pphi (jump j l) Q - | PX P i Q => - let x := hd 0 l in - let xi := pow_pos rmul x i in - (Pphi l P) * xi + (Pphi (tail l) Q) + | PX P i Q => Pphi l P * (hd l) ^ i + Pphi (tail l) Q end. Reserved Notation "P @ l " (at level 10, no associativity). Notation "P @ l " := (Pphi l P). + (** Proofs *) - Lemma ZPminus_spec : forall x y, - match ZPminus x y with - | Z0 => x = y - | Zpos k => x = (y + k)%positive - | Zneg k => y = (x + k)%positive + + Ltac destr_pos_sub := + match goal with |- context [Z.pos_sub ?x ?y] => + generalize (Z.pos_sub_discr x y); destruct (Z.pos_sub x y) end. + + Lemma Peq_ok P P' : (P ?== P') = true -> forall l, P@l == P'@ l. + Proof. + revert P';induction P;destruct P';simpl; intros H l; try easy. + - now apply (morph_eq CRmorph). + - destruct (Pos.compare_spec p p0); [ subst | easy | easy ]. + now rewrite IHP. + - specialize (IHP1 P'1); specialize (IHP2 P'2). + destruct (Pos.compare_spec p p0); [ subst | easy | easy ]. + destruct (P2 ?== P'1); [|easy]. + rewrite H in *. + now rewrite IHP1, IHP2. + Qed. + + Lemma Peq_spec P P' : + BoolSpec (forall l, P@l == P'@l) True (P ?== P'). Proof. - induction x;destruct y. - replace (ZPminus (xI x) (xI y)) with (Zdouble (ZPminus x y));trivial. - assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;trivial. - replace (ZPminus (xI x) (xO y)) with (Zdouble_plus_one (ZPminus x y));trivial. - assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble_plus_one;rewrite H;trivial. - apply Pplus_xI_double_minus_one. - simpl;trivial. - replace (ZPminus (xO x) (xI y)) with (Zdouble_minus_one (ZPminus x y));trivial. - assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble_minus_one;rewrite H;trivial. - apply Pplus_xI_double_minus_one. - replace (ZPminus (xO x) (xO y)) with (Zdouble (ZPminus x y));trivial. - assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;trivial. - replace (ZPminus (xO x) xH) with (Zpos (Pdouble_minus_one x));trivial. - rewrite <- Pplus_one_succ_l. - rewrite Psucc_o_double_minus_one_eq_xO;trivial. - replace (ZPminus xH (xI y)) with (Zneg (xO y));trivial. - replace (ZPminus xH (xO y)) with (Zneg (Pdouble_minus_one y));trivial. - rewrite <- Pplus_one_succ_l. - rewrite Psucc_o_double_minus_one_eq_xO;trivial. - simpl;trivial. + generalize (Peq_ok P P'). destruct (P ?== P'); auto. Qed. - Lemma Peq_ok : forall P P', - (P ?== P') = true -> forall l, P@l == P'@ l. + Lemma Pphi0 l : P0@l == 0. Proof. - induction P;destruct P';simpl;intros;try discriminate;trivial. - apply (morph_eq CRmorph);trivial. - assert (H1 := Pos.compare_eq p p0); destruct (p ?= p0); - try discriminate H. - rewrite (IHP P' H); rewrite H1;trivial;rrefl. - assert (H1 := Pos.compare_eq p p0); destruct (p ?= p0); - try discriminate H. - rewrite H1;trivial. clear H1. - assert (H1 := IHP1 P'1);assert (H2 := IHP2 P'2); - destruct (P2 ?== P'1);[destruct (P3 ?== P'2); [idtac|discriminate H] - |discriminate H]. - rewrite (H1 H);rewrite (H2 H);rrefl. + simpl;apply (morph0 CRmorph). Qed. - Lemma Pphi0 : forall l, P0@l == 0. + Lemma Pphi1 l : P1@l == 1. Proof. - intros;simpl;apply (morph0 CRmorph). + simpl;apply (morph1 CRmorph). Qed. -Lemma env_morph : forall p e1 e2, (forall x, e1 x = e2 x) -> - p @ e1 = p @ e2. +Lemma env_morph p e1 e2 : + (forall x, e1 x = e2 x) -> p @ e1 = p @ e2. Proof. - induction p ; simpl. - reflexivity. - intros. - apply IHp. - intros. - unfold jump. - apply H. - intros. - rewrite (IHp1 e1 e2) ; auto. - rewrite (IHp2 (tail e1) (tail e2)) ; auto. - unfold hd. unfold nth. rewrite H. reflexivity. - unfold tail. unfold jump. intros ; apply H. + revert e1 e2. induction p ; simpl. + - reflexivity. + - intros e1 e2 EQ. apply IHp. intros. apply EQ. + - intros e1 e2 EQ. f_equal; [f_equal|]. + + now apply IHp1. + + f_equal. apply EQ. + + apply IHp2. intros; apply EQ. Qed. -Lemma Pjump_Pplus : forall P i j l, P @ (jump (i + j) l ) = P @ (jump j (jump i l)). +Lemma Pjump_add P i j l : + P @ (jump (i + j) l) = P @ (jump j (jump i l)). Proof. - intros. apply env_morph. intros. rewrite <- jump_Pplus. - rewrite Pplus_comm. - reflexivity. + apply env_morph. intros. rewrite <- jump_add. f_equal. + apply Pos.add_comm. Qed. -Lemma Pjump_xO_tail : forall P p l, +Lemma Pjump_xO_tail P p l : P @ (jump (xO p) (tail l)) = P @ (jump (xI p) l). Proof. - intros. - apply env_morph. - intros. - rewrite (@jump_simpl R (xI p)). - rewrite (@jump_simpl R (xO p)). - reflexivity. + apply env_morph. intros. now jump_simpl. Qed. -Lemma Pjump_Pdouble_minus_one : forall P p l, - P @ (jump (Pdouble_minus_one p) (tail l)) = P @ (jump (xO p) l). +Lemma Pjump_pred_double P p l : + P @ (jump (Pos.pred_double p) (tail l)) = P @ (jump (xO p) l). Proof. - intros. - apply env_morph. - intros. - rewrite jump_Pdouble_minus_one. - rewrite (@jump_simpl R (xO p)). - reflexivity. + apply env_morph. intros. + rewrite jump_pred_double. now jump_simpl. Qed. - - - Lemma Pphi1 : forall l, P1@l == 1. + Lemma mkPinj_ok j l P : (mkPinj j P)@l == P@(jump j l). Proof. - intros;simpl;apply (morph1 CRmorph). + destruct P;simpl;rsimpl. + now rewrite Pjump_add. Qed. - Lemma mkPinj_ok : forall j l P, (mkPinj j P)@l == P@(jump j l). + Lemma pow_pos_add x i j : x^(j + i) == x^i * x^j. Proof. - intros j l p;destruct p;simpl;rsimpl. - rewrite Pjump_Pplus. - reflexivity. + rewrite Pos.add_comm. + apply (pow_pos_add Rsth Reqe.(Rmul_ext) ARth.(ARmul_assoc)). Qed. - Let pow_pos_Pplus := - pow_pos_Pplus rmul Rsth Reqe.(Rmul_ext) ARth.(ARmul_comm) ARth.(ARmul_assoc). - - Lemma mkPX_ok : forall l P i Q, - (mkPX P i Q)@l == P@l*(pow_pos rmul (hd 0 l) i) + Q@(tail l). + Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c ?=! c'). Proof. - intros l P i Q;unfold mkPX. - destruct P;try (simpl;rrefl). - assert (H := morph_eq CRmorph c cO);destruct (c ?=! cO);simpl;try rrefl. - rewrite (H (refl_equal true));rewrite (morph0 CRmorph). - rewrite mkPinj_ok;rsimpl;simpl;rrefl. - assert (H := @Peq_ok P3 P0);destruct (P3 ?== P0);simpl;try rrefl. - rewrite (H (refl_equal true));trivial. - rewrite Pphi0. rewrite pow_pos_Pplus;rsimpl. + generalize (morph_eq CRmorph c c'). + destruct (c ?=! c'); auto. Qed. + Lemma mkPX_ok l P i Q : + (mkPX P i Q)@l == P@l * (hd l)^i + Q@(tail l). + Proof. + unfold mkPX. destruct P. + - case ceqb_spec; intros H; simpl; try reflexivity. + rewrite H, (morph0 CRmorph), mkPinj_ok; rsimpl. + - reflexivity. + - case Peq_spec; intros H; simpl; try reflexivity. + rewrite H, Pphi0, Pos.add_comm, pow_pos_add; rsimpl. + Qed. Ltac Esimpl := repeat (progress ( @@ -647,43 +617,42 @@ Qed. end)); rsimpl; simpl. - Lemma PaddC_ok : forall c P l, (PaddC P c)@l == P@l + [c]. + Lemma PaddC_ok c P l : (PaddC P c)@l == P@l + [c]. Proof. - induction P;simpl;intros;Esimpl;trivial. + revert l;induction P;simpl;intros;Esimpl;trivial. rewrite IHP2;rsimpl. Qed. - Lemma PsubC_ok : forall c P l, (PsubC P c)@l == P@l - [c]. + Lemma PsubC_ok c P l : (PsubC P c)@l == P@l - [c]. Proof. - induction P;simpl;intros. - Esimpl. - rewrite IHP;rsimpl. - rewrite IHP2;rsimpl. + revert l;induction P;simpl;intros. + - Esimpl. + - rewrite IHP;rsimpl. + - rewrite IHP2;rsimpl. Qed. - Lemma PmulC_aux_ok : forall c P l, (PmulC_aux P c)@l == P@l * [c]. + Lemma PmulC_aux_ok c P l : (PmulC_aux P c)@l == P@l * [c]. Proof. - induction P;simpl;intros;Esimpl;trivial. - rewrite IHP1;rewrite IHP2;rsimpl. - mul_push ([c]);rrefl. + revert l;induction P;simpl;intros;Esimpl;trivial. + rewrite IHP1, IHP2;rsimpl. add_permut. mul_permut. Qed. - Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c]. + Lemma PmulC_ok c P l : (PmulC P c)@l == P@l * [c]. Proof. - intros c P l; unfold PmulC. - assert (H:= morph_eq CRmorph c cO);destruct (c ?=! cO). - rewrite (H (refl_equal true));Esimpl. - assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI). - rewrite (H1 (refl_equal true));Esimpl. - apply PmulC_aux_ok. + unfold PmulC. + case ceqb_spec; intros H. + - rewrite H; Esimpl. + - case ceqb_spec; intros H'. + + rewrite H'; Esimpl. + + apply PmulC_aux_ok. Qed. - Lemma Popp_ok : forall P l, (--P)@l == - P@l. + Lemma Popp_ok P l : (--P)@l == - P@l. Proof. - induction P;simpl;intros. - Esimpl. - apply IHP. - rewrite IHP1;rewrite IHP2;rsimpl. + revert l;induction P;simpl;intros. + - Esimpl. + - apply IHP. + - rewrite IHP1, IHP2;rsimpl. Qed. Ltac Esimpl2 := @@ -696,520 +665,273 @@ Qed. | |- context [(--?P)@?l] => rewrite (Popp_ok P l) end)); Esimpl. - - - - Lemma Padd_ok : forall P' P l, (P ++ P')@l == P@l + P'@l. - Proof. - induction P';simpl;intros;Esimpl2. - generalize P p l;clear P p l. - induction P;simpl;intros. - Esimpl2;apply (ARadd_comm ARth). - assert (H := ZPminus_spec p p0);destruct (ZPminus p p0). - rewrite H;Esimpl. rewrite IHP';rrefl. - rewrite H;Esimpl. rewrite IHP';Esimpl. - rewrite Pjump_Pplus. rrefl. - rewrite H;Esimpl. rewrite IHP. - rewrite Pjump_Pplus. rrefl. - destruct p0;simpl. - rewrite IHP2;simpl. rsimpl. - rewrite Pjump_xO_tail. Esimpl. - rewrite IHP2;simpl. - rewrite Pjump_Pdouble_minus_one. - rsimpl. - rewrite IHP'. - rsimpl. - destruct P;simpl. - Esimpl2;add_push [c];rrefl. - destruct p0;simpl;Esimpl2. - rewrite IHP'2;simpl. - rewrite Pjump_xO_tail. - rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl. - rewrite IHP'2;simpl. - rewrite Pjump_Pdouble_minus_one. rsimpl. - add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl. - rewrite IHP'2;rsimpl. - unfold tail. - add_push (P @ (jump 1 l));rrefl. - assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2. - rewrite IHP'1;rewrite IHP'2;rsimpl. - add_push (P3 @ (tail l));rewrite H;rrefl. - rewrite IHP'1;rewrite IHP'2;simpl;Esimpl. - rewrite H;rewrite Pplus_comm. - rewrite pow_pos_Pplus;rsimpl. - add_push (P3 @ (tail l));rrefl. - assert (forall P k l, - (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow_pos rmul (hd 0 l) k). - induction P;simpl;intros;try apply (ARadd_comm ARth). - destruct p2; simpl; try apply (ARadd_comm ARth). - rewrite Pjump_xO_tail. - apply (ARadd_comm ARth). - rewrite Pjump_Pdouble_minus_one. - apply (ARadd_comm ARth). - assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2. - rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tail l0));rrefl. - rewrite IHP'1;simpl;Esimpl. - rewrite H1;rewrite Pplus_comm. - rewrite pow_pos_Pplus;simpl;Esimpl. - add_push (P5 @ (tail l0));rrefl. - rewrite IHP1;rewrite H1;rewrite Pplus_comm. - rewrite pow_pos_Pplus;simpl;rsimpl. - add_push (P5 @ (tail l0));rrefl. - rewrite H0;rsimpl. - add_push (P3 @ (tail l)). - rewrite H;rewrite Pplus_comm. - rewrite IHP'2;rewrite pow_pos_Pplus;rsimpl. - add_push (P3 @ (tail l));rrefl. - Qed. - - Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l. + Lemma PaddX_ok P' P k l : + (forall P l, (P++P')@l == P@l + P'@l) -> + (PaddX Padd P' k P) @ l == P@l + P'@l * (hd l)^k. Proof. - induction P';simpl;intros;Esimpl2;trivial. - generalize P p l;clear P p l. - induction P;simpl;intros. - Esimpl2;apply (ARadd_comm ARth). - assert (H := ZPminus_spec p p0);destruct (ZPminus p p0). - rewrite H;Esimpl. rewrite IHP';rsimpl. - rewrite H;Esimpl. rewrite IHP';Esimpl. - rewrite <- Pjump_Pplus;rewrite Pplus_comm;rrefl. - rewrite H;Esimpl. rewrite IHP. - rewrite <- Pjump_Pplus;rewrite Pplus_comm;rrefl. - destruct p0;simpl. - rewrite IHP2;simpl; try rewrite Pjump_xO_tail ; rsimpl. - rewrite IHP2;simpl. - rewrite Pjump_Pdouble_minus_one;rsimpl. - unfold tail ; rsimpl. - rewrite IHP';rsimpl. - destruct P;simpl. - repeat rewrite Popp_ok;Esimpl2;rsimpl;add_push [c];try rrefl. - destruct p0;simpl;Esimpl2. - rewrite IHP'2;simpl;rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));trivial. - rewrite Pjump_xO_tail. - add_push (P @ ((jump (xI p0) l)));rrefl. - rewrite IHP'2;simpl;rewrite Pjump_Pdouble_minus_one;rsimpl. - add_push (- (P'1 @ l * pow_pos rmul (hd 0 l) p));rrefl. - unfold tail. - rewrite IHP'2;rsimpl;add_push (P @ (jump 1 l));rrefl. - assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2. - rewrite IHP'1; rewrite IHP'2;rsimpl. - add_push (P3 @ (tail l));rewrite H;rrefl. - rewrite IHP'1; rewrite IHP'2;rsimpl;simpl;Esimpl. - rewrite H;rewrite Pplus_comm. - rewrite pow_pos_Pplus;rsimpl. - add_push (P3 @ (tail l));rrefl. - assert (forall P k l, - (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow_pos rmul (hd 0 l) k). - induction P;simpl;intros. - rewrite Popp_ok;rsimpl;apply (ARadd_comm ARth);trivial. - destruct p2;simpl; rewrite Popp_ok;rsimpl. - rewrite Pjump_xO_tail. - apply (ARadd_comm ARth);trivial. - rewrite Pjump_Pdouble_minus_one. - apply (ARadd_comm ARth);trivial. - apply (ARadd_comm ARth);trivial. - assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2;rsimpl. - rewrite IHP'1;rsimpl;add_push (P5 @ (tail l0));rewrite H1;rrefl. - rewrite IHP'1;rewrite H1;rewrite Pplus_comm. - rewrite pow_pos_Pplus;simpl;Esimpl. - add_push (P5 @ (tail l0));rrefl. - rewrite IHP1;rewrite H1;rewrite Pplus_comm. - rewrite pow_pos_Pplus;simpl;rsimpl. - add_push (P5 @ (tail l0));rrefl. - rewrite H0;rsimpl. - rewrite IHP'2;rsimpl;add_push (P3 @ (tail l)). - rewrite H;rewrite Pplus_comm. - rewrite pow_pos_Pplus;rsimpl. + intros IHP'. + revert k l. induction P;simpl;intros. + - add_permut. + - destruct p; simpl; + rewrite ?Pjump_xO_tail, ?Pjump_pred_double; add_permut. + - destr_pos_sub; intros ->;Esimpl2. + + rewrite IHP';rsimpl. add_permut. + + rewrite IHP', pow_pos_add;simpl;Esimpl. add_permut. + + rewrite IHP1, pow_pos_add;rsimpl. add_permut. Qed. -(* Proof for the symmetric version *) - Lemma PmulI_ok : - forall P', - (forall (P : Pol) (l : Env R), (Pmul P P') @ l == P @ l * P' @ l) -> - forall (P : Pol) (p : positive) (l : Env R), - (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l). + Lemma Padd_ok P' P l : (P ++ P')@l == P@l + P'@l. Proof. - induction P;simpl;intros. - Esimpl2;apply (ARmul_comm ARth). - assert (H1 := ZPminus_spec p p0);destruct (ZPminus p p0);Esimpl2. - rewrite H1; rewrite H;rrefl. - rewrite H1; rewrite H. - rewrite Pjump_Pplus;simpl;rrefl. - rewrite H1. - rewrite Pjump_Pplus;rewrite IHP;rrefl. - destruct p0;Esimpl2. - rewrite IHP1;rewrite IHP2;rsimpl. - rewrite Pjump_xO_tail. - mul_push (pow_pos rmul (hd 0 l) p);rrefl. - rewrite IHP1;rewrite IHP2;simpl;rsimpl. - mul_push (pow_pos rmul (hd 0 l) p); rewrite Pjump_Pdouble_minus_one. - rrefl. - rewrite IHP1;simpl;rsimpl. - mul_push (pow_pos rmul (hd 0 l) p). - rewrite H;rrefl. + revert P l; induction P';simpl;intros;Esimpl2. + - revert p l; induction P;simpl;intros. + + Esimpl2; add_permut. + + destr_pos_sub; intros ->;Esimpl. + * now rewrite IHP'. + * rewrite IHP';Esimpl. now rewrite Pjump_add. + * rewrite IHP. now rewrite Pjump_add. + + destruct p0;simpl. + * rewrite IHP2;simpl. rsimpl. rewrite Pjump_xO_tail. Esimpl. + * rewrite IHP2;simpl. rewrite Pjump_pred_double. rsimpl. + * rewrite IHP'. rsimpl. + - destruct P;simpl. + + Esimpl2. add_permut. + + destruct p0;simpl;Esimpl2; rewrite IHP'2; simpl. + * rewrite Pjump_xO_tail. rsimpl. add_permut. + * rewrite Pjump_pred_double. rsimpl. add_permut. + * rsimpl. unfold tail. add_permut. + + destr_pos_sub; intros ->; Esimpl2. + * rewrite IHP'1, IHP'2;rsimpl. add_permut. + * rewrite IHP'1, IHP'2;simpl;Esimpl. + rewrite pow_pos_add;rsimpl. add_permut. + * rewrite PaddX_ok by trivial; rsimpl. + rewrite IHP'2, pow_pos_add; rsimpl. add_permut. Qed. -(* - Lemma PmulI_ok : - forall P', - (forall (P : Pol) (l : list R), (Pmul_aux P P') @ l == P @ l * P' @ l) -> - forall (P : Pol) (p : positive) (l : list R), - (PmulI Pmul_aux P' p P) @ l == P @ l * P' @ (jump p l). + Lemma PsubX_ok P' P k l : + (forall P l, (P--P')@l == P@l - P'@l) -> + (PsubX Psub P' k P) @ l == P@l - P'@l * (hd l)^k. Proof. - induction P;simpl;intros. - Esimpl2;apply (ARmul_comm ARth). - assert (H1 := ZPminus_spec p p0);destruct (ZPminus p p0);Esimpl2. - rewrite H1; rewrite H;rrefl. - rewrite H1; rewrite H. - rewrite Pplus_comm. - rewrite jump_Pplus;simpl;rrefl. - rewrite H1;rewrite Pplus_comm. - rewrite jump_Pplus;rewrite IHP;rrefl. - destruct p0;Esimpl2. - rewrite IHP1;rewrite IHP2;simpl;rsimpl. - mul_push (pow_pos rmul (hd 0 l) p);rrefl. - rewrite IHP1;rewrite IHP2;simpl;rsimpl. - mul_push (pow_pos rmul (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl. - rewrite IHP1;simpl;rsimpl. - mul_push (pow_pos rmul (hd 0 l) p). - rewrite H;rrefl. + intros IHP'. + revert k l. induction P;simpl;intros. + - rewrite Popp_ok;rsimpl; add_permut. + - destruct p; simpl; + rewrite Popp_ok;rsimpl; + rewrite ?Pjump_xO_tail, ?Pjump_pred_double; add_permut. + - destr_pos_sub; intros ->; Esimpl2; rsimpl. + + rewrite IHP';rsimpl. add_permut. + + rewrite IHP', pow_pos_add;simpl;Esimpl. add_permut. + + rewrite IHP1, pow_pos_add;rsimpl. add_permut. Qed. - Lemma Pmul_aux_ok : forall P' P l,(Pmul_aux P P')@l == P@l * P'@l. + Lemma Psub_ok P' P l : (P -- P')@l == P@l - P'@l. Proof. - induction P';simpl;intros. - Esimpl2;trivial. - apply PmulI_ok;trivial. - rewrite Padd_ok;Esimpl2. - rewrite (PmulI_ok P'2 IHP'2). rewrite IHP'1. rrefl. + revert P l; induction P';simpl;intros;Esimpl2. + - revert p l; induction P;simpl;intros. + + Esimpl2; add_permut. + + destr_pos_sub; intros ->;Esimpl. + * rewrite IHP';rsimpl. + * rewrite IHP';Esimpl. now rewrite Pjump_add. + * rewrite IHP. now rewrite Pjump_add. + + destruct p0;simpl. + * rewrite IHP2;simpl. rsimpl. rewrite Pjump_xO_tail. Esimpl. + * rewrite IHP2;simpl. rewrite Pjump_pred_double. rsimpl. + * rewrite IHP'. rsimpl. + - destruct P;simpl. + + Esimpl2; add_permut. + + destruct p0;simpl;Esimpl2; rewrite IHP'2; simpl. + * rewrite Pjump_xO_tail. rsimpl. add_permut. + * rewrite Pjump_pred_double. rsimpl. add_permut. + * rsimpl. unfold tail. add_permut. + + destr_pos_sub; intros ->; Esimpl2. + * rewrite IHP'1, IHP'2;rsimpl. add_permut. + * rewrite IHP'1, IHP'2;simpl;Esimpl. + rewrite pow_pos_add;rsimpl. add_permut. + * rewrite PsubX_ok by trivial;rsimpl. + rewrite IHP'2, pow_pos_add;rsimpl. add_permut. Qed. -*) -(* Proof for the symmetric version *) - Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. + Lemma PmulI_ok P' : + (forall P l, (Pmul P P') @ l == P @ l * P' @ l) -> + forall P p l, (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l). Proof. - intros P P';generalize P;clear P;induction P';simpl;intros. - apply PmulC_ok. apply PmulI_ok;trivial. - destruct P. - rewrite (ARmul_comm ARth);Esimpl2;Esimpl2. - Esimpl2. rewrite IHP'1;Esimpl2. - assert (match p0 with - | xI j => Pinj (xO j) P ** P'2 - | xO j => Pinj (Pdouble_minus_one j) P ** P'2 - | 1 => P ** P'2 - end @ (tail l) == P @ (jump p0 l) * P'2 @ (tail l)). - destruct p0;rewrite IHP'2;Esimpl. - rewrite Pjump_xO_tail. reflexivity. - rewrite Pjump_Pdouble_minus_one;Esimpl. - rewrite H;Esimpl. - rewrite Padd_ok; Esimpl2. rewrite Padd_ok; Esimpl2. - repeat (rewrite IHP'1 || rewrite IHP'2);simpl. - rewrite PmulI_ok;trivial. - unfold tail. - mul_push (P'1@l). simpl. mul_push (P'2 @ (jump 1 l)). Esimpl. + intros IHP'. + induction P;simpl;intros. + - Esimpl2; mul_permut. + - destr_pos_sub; intros ->;Esimpl2. + + now rewrite IHP'. + + now rewrite IHP', Pjump_add. + + now rewrite IHP, Pjump_add. + - destruct p0;Esimpl2; rewrite ?IHP1, ?IHP2; rsimpl. + + rewrite Pjump_xO_tail. f_equiv. mul_permut. + + rewrite Pjump_pred_double. f_equiv. mul_permut. + + rewrite IHP'. f_equiv. mul_permut. Qed. -(* -Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. + Lemma Pmul_ok P P' l : (P**P')@l == P@l * P'@l. Proof. - destruct P;simpl;intros. - Esimpl2;apply (ARmul_comm ARth). - rewrite (PmulI_ok P (Pmul_aux_ok P)). - apply (ARmul_comm ARth). - rewrite Padd_ok; Esimpl2. - rewrite (PmulI_ok P3 (Pmul_aux_ok P3));trivial. - rewrite Pmul_aux_ok;mul_push (P' @ l). - rewrite (ARmul_comm ARth (P' @ l));rrefl. + revert P l;induction P';simpl;intros. + - apply PmulC_ok. + - apply PmulI_ok;trivial. + - destruct P. + + rewrite (ARmul_comm ARth). Esimpl2; Esimpl2. + + Esimpl2. rewrite IHP'1;Esimpl2. f_equiv. + destruct p0;rewrite IHP'2;Esimpl. + * now rewrite Pjump_xO_tail. + * rewrite Pjump_pred_double; Esimpl. + + rewrite Padd_ok, !mkPX_ok, Padd_ok, !mkPX_ok, + !IHP'1, !IHP'2, PmulI_ok; trivial. Esimpl2. + unfold tail. + add_permut; f_equiv; mul_permut. Qed. -*) - Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l. + Lemma Psquare_ok P l : (Psquare P)@l == P@l * P@l. Proof. - induction P;simpl;intros;Esimpl2. - apply IHP. rewrite Padd_ok. rewrite Pmul_ok;Esimpl2. - rewrite IHP1;rewrite IHP2. - mul_push (pow_pos rmul (hd 0 l) p). mul_push (P2@l). - rrefl. + revert l;induction P;simpl;intros;Esimpl2. + - apply IHP. + - rewrite Padd_ok, Pmul_ok;Esimpl2. + rewrite IHP1, IHP2. + mul_push ((hd l)^p). now mul_push (P2@l). Qed. - Lemma Mphi_morph : forall P env env', (forall x, env x = env' x ) -> - Mphi env P = Mphi env' P. + Lemma Mphi_morph M e1 e2 : + (forall x, e1 x = e2 x) -> M @@ e1 = M @@ e2. Proof. - induction P ; simpl. - reflexivity. - intros. - apply IHP. - intros. - unfold jump. - apply H. - (**) - intros. - replace (Mphi (tail env) P) with (Mphi (tail env') P). - unfold hd. unfold nth. - rewrite H. - reflexivity. - apply IHP. - unfold tail,jump. - intros. symmetry. apply H. + revert e1 e2; induction M; simpl; intros e1 e2 EQ; trivial. + - apply IHM. intros; apply EQ. + - f_equal. + * apply IHM. intros; apply EQ. + * f_equal. apply EQ. Qed. -Lemma Mjump_xO_tail : forall M p l, - Mphi (jump (xO p) (tail l)) M = Mphi (jump (xI p) l) M. +Lemma Mjump_xO_tail M p l : + M @@ (jump (xO p) (tail l)) = M @@ (jump (xI p) l). Proof. - intros. - apply Mphi_morph. - intros. - rewrite (@jump_simpl R (xI p)). - rewrite (@jump_simpl R (xO p)). - reflexivity. + apply Mphi_morph. intros. now jump_simpl. Qed. -Lemma Mjump_Pdouble_minus_one : forall M p l, - Mphi (jump (Pdouble_minus_one p) (tail l)) M = Mphi (jump (xO p) l) M. +Lemma Mjump_pred_double M p l : + M @@ (jump (Pos.pred_double p) (tail l)) = M @@ (jump (xO p) l). Proof. - intros. - apply Mphi_morph. - intros. - rewrite jump_Pdouble_minus_one. - rewrite (@jump_simpl R (xO p)). - reflexivity. + apply Mphi_morph. intros. + rewrite jump_pred_double. now jump_simpl. Qed. -Lemma Mjump_Pplus : forall M i j l, Mphi (jump (i + j) l ) M = Mphi (jump j (jump i l)) M. +Lemma Mjump_add M i j l : + M @@ (jump (i + j) l) = M @@ (jump j (jump i l)). Proof. - intros. apply Mphi_morph. intros. rewrite <- jump_Pplus. - rewrite Pplus_comm. - reflexivity. + apply Mphi_morph. intros. now rewrite <- jump_add, Pos.add_comm. Qed. - - - Lemma mkZmon_ok: forall M j l, - Mphi l (mkZmon j M) == Mphi l (zmon j M). - intros M j l; case M; simpl; intros; rsimpl. + Lemma mkZmon_ok M j l : + (mkZmon j M) @@ l == (zmon j M) @@ l. + Proof. + destruct M; simpl; rsimpl. Qed. - Lemma zmon_pred_ok : forall M j l, - Mphi (tail l) (zmon_pred j M) == Mphi l (zmon j M). + Lemma zmon_pred_ok M j l : + (zmon_pred j M) @@ (tail l) == (zmon j M) @@ l. Proof. - destruct j; simpl;intros l; rsimpl. - rewrite mkZmon_ok;rsimpl. - simpl. - rewrite Mjump_xO_tail. - reflexivity. - rewrite mkZmon_ok;simpl. - rewrite Mjump_Pdouble_minus_one; rsimpl. + destruct j; simpl; rewrite ?mkZmon_ok; simpl; rsimpl. + - now rewrite Mjump_xO_tail. + - rewrite Mjump_pred_double; rsimpl. Qed. - Lemma mkVmon_ok : forall M i l, Mphi l (mkVmon i M) == Mphi l M*pow_pos rmul (hd 0 l) i. + Lemma mkVmon_ok M i l : + (mkVmon i M)@@l == M@@l * (hd l)^i. Proof. destruct M;simpl;intros;rsimpl. - rewrite zmon_pred_ok;simpl;rsimpl. - rewrite Pplus_comm;rewrite pow_pos_Pplus;rsimpl. + - rewrite zmon_pred_ok;simpl;rsimpl. + - rewrite pow_pos_add;rsimpl. Qed. + Ltac destr_mfactor R S := match goal with + | H : context [MFactor ?P _] |- context [MFactor ?P ?M] => + specialize (H M); destruct MFactor as (R,S) + end. - Lemma Mphi_ok: forall P M l, - let (Q,R) := MFactor P M in - P@l == Q@l + (Mphi l M) * (R@l). + Lemma Mphi_ok P M l : + let (Q,R) := MFactor P M in + P@l == Q@l + M@@l * R@l. Proof. - intros P; elim P; simpl; auto; clear P. - intros c M l; case M; simpl; auto; try intro p; try intro m; - try rewrite (morph0 CRmorph); rsimpl. - - intros i P Hrec M l; case M; simpl; clear M. - rewrite (morph0 CRmorph); rsimpl. - intros j M. - case_eq (i ?= j); intros He; simpl. - rewrite (Pos.compare_eq _ _ He). - generalize (Hrec M (jump j l)); case (MFactor P M); - simpl; intros P2 Q2 H; repeat rewrite mkPinj_ok; auto. - generalize (Hrec (zmon (j -i) M) (jump i l)); - case (MFactor P (zmon (j -i) M)); simpl. - intros P2 Q2 H; repeat rewrite mkPinj_ok; auto. - rewrite <- (Pplus_minus _ _ (ZC2 _ _ He)). - rewrite Mjump_Pplus; auto. - rewrite (morph0 CRmorph); rsimpl. - intros P2 m; rewrite (morph0 CRmorph); rsimpl. - - intros P2 Hrec1 i Q2 Hrec2 M l; case M; simpl; auto. - rewrite (morph0 CRmorph); rsimpl. - intros j M1. - generalize (Hrec1 (zmon j M1) l); - case (MFactor P2 (zmon j M1)). - intros R1 S1 H1. - generalize (Hrec2 (zmon_pred j M1) (tail l)); - case (MFactor Q2 (zmon_pred j M1)); simpl. - intros R2 S2 H2; rewrite H1; rewrite H2. - repeat rewrite mkPX_ok; simpl. - rsimpl. - apply radd_ext; rsimpl. - rewrite (ARadd_comm ARth); rsimpl. - apply radd_ext; rsimpl. - rewrite (ARadd_comm ARth); rsimpl. - rewrite zmon_pred_ok;rsimpl. - intros j M1. - case_eq (i ?= j); intros He; simpl. - rewrite (Pos.compare_eq _ _ He). - generalize (Hrec1 (mkZmon xH M1) l); case (MFactor P2 (mkZmon xH M1)); - simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. - rewrite H; rewrite mkPX_ok; rsimpl. - repeat (rewrite <-(ARadd_assoc ARth)). - apply radd_ext; rsimpl. - rewrite (ARadd_comm ARth); rsimpl. - apply radd_ext; rsimpl. - repeat (rewrite <-(ARmul_assoc ARth)). - rewrite mkZmon_ok. - apply rmul_ext; rsimpl. - rewrite (ARmul_comm ARth); rsimpl. - generalize (Hrec1 (vmon (j - i) M1) l); - case (MFactor P2 (vmon (j - i) M1)); - simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. - rewrite H; rsimpl; repeat rewrite mkPinj_ok; auto. - rewrite mkPX_ok; rsimpl. - repeat (rewrite <-(ARadd_assoc ARth)). - apply radd_ext; rsimpl. - rewrite (ARadd_comm ARth); rsimpl. - apply radd_ext; rsimpl. - repeat (rewrite <-(ARmul_assoc ARth)). - apply rmul_ext; rsimpl. - rewrite (ARmul_comm ARth); rsimpl. - apply rmul_ext; rsimpl. - rewrite <- pow_pos_Pplus. - rewrite (Pplus_minus _ _ (ZC2 _ _ He)); rsimpl. - generalize (Hrec1 (mkZmon 1 M1) l); - case (MFactor P2 (mkZmon 1 M1)); - simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. - rewrite H; rsimpl. - rewrite mkPX_ok; rsimpl. - repeat (rewrite <-(ARadd_assoc ARth)). - apply radd_ext; rsimpl. - rewrite (ARadd_comm ARth); rsimpl. - apply radd_ext; rsimpl. - rewrite mkZmon_ok. - repeat (rewrite <-(ARmul_assoc ARth)). - apply rmul_ext; rsimpl. - rewrite (ARmul_comm ARth); rsimpl. - rewrite mkPX_ok; simpl; rsimpl. - rewrite (morph0 CRmorph); rsimpl. - repeat (rewrite <-(ARmul_assoc ARth)). - rewrite (ARmul_comm ARth (Q3@l)); rsimpl. - apply rmul_ext; rsimpl. - rewrite <- pow_pos_Pplus. - rewrite (Pplus_minus _ _ He); rsimpl. + revert M l; induction P; destruct M; intros l; simpl; auto; Esimpl. + - case Pos.compare_spec; intros He; simpl. + * destr_mfactor R1 S1. now rewrite IHP, He, !mkPinj_ok. + * destr_mfactor R1 S1. rewrite IHP; simpl. + now rewrite !mkPinj_ok, <- Mjump_add, Pos.add_comm, Pos.sub_add. + * Esimpl. + - destr_mfactor R1 S1. destr_mfactor R2 S2. + rewrite IHP1, IHP2, !mkPX_ok, zmon_pred_ok; simpl; rsimpl. + add_permut. + - case Pos.compare_spec; intros He; simpl; destr_mfactor R1 S1; + rewrite ?He, IHP1, mkPX_ok, ?mkZmon_ok; simpl; rsimpl; + unfold tail; add_permut; mul_permut. + * rewrite <- pow_pos_add, Pos.add_comm, Pos.sub_add by trivial; rsimpl. + * rewrite mkPX_ok; Esimpl2. mul_permut. + rewrite <- pow_pos_add, Pos.sub_add by trivial; rsimpl. Qed. -(* Proof for the symmetric version *) - - Lemma POneSubst_ok: forall P1 M1 P2 P3 l, - POneSubst P1 M1 P2 = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l. + Lemma POneSubst_ok P1 M1 P2 P3 l : + POneSubst P1 M1 P2 = Some P3 -> M1@@l == P2@l -> + P1@l == P3@l. Proof. - intros P2 M1 P3 P4 l; unfold POneSubst. - generalize (Mphi_ok P2 M1 l); case (MFactor P2 M1); simpl; auto. - intros Q1 R1; case R1. - intros c H; rewrite H. - generalize (morph_eq CRmorph c cO); - case (c ?=! cO); simpl; auto. - intros H1 H2; rewrite H1; auto; rsimpl. - discriminate. - intros _ H1 H2; injection H1; intros; subst. - rewrite H2; rsimpl. - (* new version *) - rewrite Padd_ok; rewrite PmulC_ok; rsimpl. - intros i P5 H; rewrite H. - intros HH H1; injection HH; intros; subst; rsimpl. - rewrite Padd_ok; rewrite PmulI_ok by (intros;apply Pmul_ok). rewrite H1; rsimpl. - intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3. - assert (P4 = Q1 ++ P3 ** PX i P5 P6). - injection H2; intros; subst;trivial. - rewrite H;rewrite Padd_ok;rewrite Pmul_ok;rsimpl. -Qed. -(* - Lemma POneSubst_ok: forall P1 M1 P2 P3 l, - POneSubst P1 M1 P2 = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l. -Proof. - intros P2 M1 P3 P4 l; unfold POneSubst. - generalize (Mphi_ok P2 M1 l); case (MFactor P2 M1); simpl; auto. - intros Q1 R1; case R1. - intros c H; rewrite H. - generalize (morph_eq CRmorph c cO); - case (c ?=! cO); simpl; auto. - intros H1 H2; rewrite H1; auto; rsimpl. - discriminate. - intros _ H1 H2; injection H1; intros; subst. - rewrite H2; rsimpl. - rewrite Padd_ok; rewrite Pmul_ok; rsimpl. - intros i P5 H; rewrite H. - intros HH H1; injection HH; intros; subst; rsimpl. - rewrite Padd_ok; rewrite Pmul_ok. rewrite H1; rsimpl. - intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3. - injection H2; intros; subst; rsimpl. - rewrite Padd_ok. - rewrite Pmul_ok; rsimpl. + unfold POneSubst. + assert (H := Mphi_ok P1). destr_mfactor R1 S1. rewrite H; clear H. + intros EQ EQ'. + assert (EQ'' : P3 = R1 ++ P2 ** S1). + { revert EQ. destruct S1; try now injection 1. + case ceqb_spec; try discriminate. now injection 2. } + rewrite EQ', EQ''; clear EQ EQ' EQ''. + rewrite Padd_ok, Pmul_ok; rsimpl. Qed. -*) - Lemma PNSubst1_ok: forall n P1 M1 P2 l, - Mphi l M1 == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l. + + Lemma PNSubst1_ok n P1 M1 P2 l : + M1@@l == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l. Proof. - intros n; elim n; simpl; auto. - intros P2 M1 P3 l H. - generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l); - case (POneSubst P2 M1 P3); [idtac | intros; rsimpl]. - intros P4 Hrec; rewrite (Hrec P4); auto; rsimpl. - intros n1 Hrec P2 M1 P3 l H. - generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l); - case (POneSubst P2 M1 P3); [idtac | intros; rsimpl]. - intros P4 Hrec1; rewrite (Hrec1 P4); auto; rsimpl. + revert P1. induction n; simpl; intros P1; + generalize (POneSubst_ok P1 M1 P2); destruct POneSubst; + intros; rewrite <- ?IHn; auto; reflexivity. Qed. - Lemma PNSubst_ok: forall n P1 M1 P2 l P3, - PNSubst P1 M1 P2 n = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l. + Lemma PNSubst_ok n P1 M1 P2 l P3 : + PNSubst P1 M1 P2 n = Some P3 -> M1@@l == P2@l -> P1@l == P3@l. Proof. - intros n P2 M1 P3 l P4; unfold PNSubst. - generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l); - case (POneSubst P2 M1 P3); [idtac | intros; discriminate]. - intros P5 H1; case n; try (intros; discriminate). - intros n1 H2; injection H2; intros; subst. - rewrite <- PNSubst1_ok; auto. + unfold PNSubst. + assert (H := POneSubst_ok P1 M1 P2); destruct POneSubst; try discriminate. + destruct n; [discriminate | injection 1; intros EQ']. + intros. rewrite <- EQ', <- PNSubst1_ok; auto. Qed. - Fixpoint MPcond (LM1: list (Mon * Pol)) (l: Env R) {struct LM1} : Prop := - match LM1 with - cons (M1,P2) LM2 => (Mphi l M1 == P2@l) /\ (MPcond LM2 l) - | _ => True - end. + Fixpoint MPcond (LM1: list (Mon * Pol)) (l: Env R) : Prop := + match LM1 with + | cons (M1,P2) LM2 => (Mphi l M1 == P2@l) /\ (MPcond LM2 l) + | _ => True + end. - Lemma PSubstL1_ok: forall n LM1 P1 l, - MPcond LM1 l -> P1@l == (PSubstL1 P1 LM1 n)@l. + Lemma PSubstL1_ok n LM1 P1 l : + MPcond LM1 l -> P1@l == (PSubstL1 P1 LM1 n)@l. Proof. - intros n LM1; elim LM1; simpl; auto. - intros; rsimpl. - intros (M2,P2) LM2 Hrec P3 l [H H1]. - rewrite <- Hrec; auto. - apply PNSubst1_ok; auto. + revert P1; induction LM1 as [|(M2,P2) LM2 IH]; simpl; intros. + - reflexivity. + - rewrite <- IH by intuition. now apply PNSubst1_ok. Qed. - Lemma PSubstL_ok: forall n LM1 P1 P2 l, - PSubstL P1 LM1 n = Some P2 -> MPcond LM1 l -> P1@l == P2@l. + Lemma PSubstL_ok n LM1 P1 P2 l : + PSubstL P1 LM1 n = Some P2 -> MPcond LM1 l -> P1@l == P2@l. Proof. - intros n LM1; elim LM1; simpl; auto. - intros; discriminate. - intros (M2,P2) LM2 Hrec P3 P4 l. - generalize (PNSubst_ok n P3 M2 P2); case (PNSubst P3 M2 P2 n). - intros P5 H0 H1 [H2 H3]; injection H1; intros; subst. - rewrite <- PSubstL1_ok; auto. - intros l1 H [H1 H2]; auto. + revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros. + - discriminate. + - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. + * injection H; intros <-. rewrite <- PSubstL1_ok; intuition. + * now apply IH. Qed. - Lemma PNSubstL_ok: forall m n LM1 P1 l, - MPcond LM1 l -> P1@l == (PNSubstL P1 LM1 m n)@l. + Lemma PNSubstL_ok m n LM1 P1 l : + MPcond LM1 l -> P1@l == (PNSubstL P1 LM1 m n)@l. Proof. - intros m; elim m; simpl; auto. - intros n LM1 P2 l H; generalize (fun P3 => @PSubstL_ok n LM1 P2 P3 l); - case (PSubstL P2 LM1 n); intros; rsimpl; auto. - intros m1 Hrec n LM1 P2 l H. - generalize (fun P3 => @PSubstL_ok n LM1 P2 P3 l); - case (PSubstL P2 LM1 n); intros; rsimpl; auto. - rewrite <- Hrec; auto. + revert LM1 P1. induction m; simpl; intros; + assert (H' := PSubstL_ok n LM1 P2); destruct PSubstL; + auto; try reflexivity. + rewrite <- IHm; auto. Qed. (** Definition of polynomial expressions *) @@ -1228,7 +950,7 @@ Proof. (** evaluation of polynomial expressions towards R *) - Fixpoint PEeval (l:Env R) (pe:PExpr) {struct pe} : R := + Fixpoint PEeval (l:Env R) (pe:PExpr) : R := match pe with | PEc c => phi c | PEX j => nth j l @@ -1241,60 +963,27 @@ Proof. (** Correctness proofs *) - Lemma mkX_ok : forall p l, nth p l == (mk_X p) @ l. + Lemma mkX_ok p l : nth p l == (mk_X p) @ l. Proof. destruct p;simpl;intros;Esimpl;trivial. rewrite nth_spec ; auto. unfold hd. - rewrite <- nth_Pdouble_minus_one. - rewrite (nth_jump (Pdouble_minus_one p) l 1). - reflexivity. + now rewrite <- nth_pred_double, nth_jump. Qed. Ltac Esimpl3 := repeat match goal with | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P2 P1 l) | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P2 P1 l) - end;Esimpl2;try rrefl;try apply (ARadd_comm ARth). - -(* Power using the chinise algorithm *) -(*Section POWER. - Variable subst_l : Pol -> Pol. - Fixpoint Ppow_pos (P:Pol) (p:positive){struct p} : Pol := - match p with - | xH => P - | xO p => subst_l (Psquare (Ppow_pos P p)) - | xI p => subst_l (Pmul P (Psquare (Ppow_pos P p))) - end. - - Definition Ppow_N P n := - match n with - | N0 => P1 - | Npos p => Ppow_pos P p - end. - - Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) -> - forall P p, (Ppow_pos P p)@l == (pow_pos Pmul P p)@l. - Proof. - intros l subst_l_ok P. - induction p;simpl;intros;try rrefl;try rewrite subst_l_ok. - repeat rewrite Pmul_ok;rewrite Psquare_ok;rewrite IHp;rrefl. - repeat rewrite Pmul_ok;rewrite Psquare_ok;rewrite IHp;rrefl. - Qed. - - Lemma Ppow_N_ok : forall l, (forall P, subst_l P@l == P@l) -> - forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l. - Proof. destruct n;simpl. rrefl. apply Ppow_pos_ok. trivial. Qed. - - End POWER. *) + end;Esimpl2;try reflexivity;try apply (ARadd_comm ARth). Section POWER. Variable subst_l : Pol -> Pol. - Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol := + Fixpoint Ppow_pos (res P:Pol) (p:positive) : Pol := match p with - | xH => subst_l (Pmul res P) + | xH => subst_l (res ** P) | xO p => Ppow_pos (Ppow_pos res P p) P p - | xI p => subst_l (Pmul (Ppow_pos (Ppow_pos res P p) P p) P) + | xI p => subst_l ((Ppow_pos (Ppow_pos res P p) P p) ** P) end. Definition Ppow_N P n := @@ -1303,17 +992,23 @@ Section POWER. | Npos p => Ppow_pos P1 P p end. - Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) -> - forall res P p, (Ppow_pos res P p)@l == res@l * (pow_pos Pmul P p)@l. + Lemma Ppow_pos_ok l : + (forall P, subst_l P@l == P@l) -> + forall res P p, (Ppow_pos res P p)@l == res@l * (pow_pos Pmul P p)@l. Proof. - intros l subst_l_ok res P p. generalize res;clear res. - induction p;simpl;intros;try rewrite subst_l_ok; repeat rewrite Pmul_ok;repeat rewrite IHp. - rsimpl. mul_push (P@l);rsimpl. rsimpl. rrefl. + intros subst_l_ok res P p. revert res. + induction p;simpl;intros; rewrite ?subst_l_ok, ?Pmul_ok, ?IHp; + mul_permut. Qed. - Lemma Ppow_N_ok : forall l, (forall P, subst_l P@l == P@l) -> - forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l. - Proof. destruct n;simpl. rrefl. rewrite Ppow_pos_ok. trivial. Esimpl. auto. Qed. + Lemma Ppow_N_ok l : + (forall P, subst_l P@l == P@l) -> + forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l. + Proof. + destruct n;simpl. + - reflexivity. + - rewrite Ppow_pos_ok by trivial. Esimpl. + Qed. End POWER. @@ -1342,57 +1037,23 @@ Section POWER. Definition norm_subst pe := subst_l (norm_aux pe). - (* - Fixpoint norm_subst (pe:PExpr) : Pol := - match pe with - | PEc c => Pc c - | PEX j => subst_l (mk_X j) - | PEadd (PEopp pe1) pe2 => Psub (norm_subst pe2) (norm_subst pe1) - | PEadd pe1 (PEopp pe2) => - Psub (norm_subst pe1) (norm_subst pe2) - | PEadd pe1 pe2 => Padd (norm_subst pe1) (norm_subst pe2) - | PEsub pe1 pe2 => Psub (norm_subst pe1) (norm_subst pe2) - | PEmul pe1 pe2 => Pmul_subst (norm_subst pe1) (norm_subst pe2) - | PEopp pe1 => Popp (norm_subst pe1) - | PEpow pe1 n => Ppow_subst (norm_subst pe1) n - end. + Lemma norm_aux_opp pe : + norm_aux (PEopp pe) = Popp (norm_aux pe). + Proof. reflexivity. Qed. - Lemma norm_subst_spec : - forall l pe, MPcond lmp l -> - PEeval l pe == (norm_subst pe)@l. - Proof. - intros;assert (subst_l_ok:forall P, (subst_l P)@l == P@l). - unfold subst_l;intros. - rewrite <- PNSubstL_ok;trivial. rrefl. - assert (Pms_ok:forall P1 P2, (Pmul_subst P1 P2)@l == P1@l*P2@l). - intros;unfold Pmul_subst;rewrite subst_l_ok;rewrite Pmul_ok;rrefl. - induction pe;simpl;Esimpl3. - rewrite subst_l_ok;apply mkX_ok. - rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3. - rewrite IHpe1;rewrite IHpe2;rrefl. - rewrite Pms_ok;rewrite IHpe1;rewrite IHpe2;rrefl. - rewrite IHpe;rrefl. - unfold Ppow_subst. rewrite Ppow_N_ok. trivial. - rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3. - induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; - repeat rewrite Pmul_ok;rrefl. - Qed. -*) - Lemma norm_aux_spec : - forall l pe, (*MPcond lmp l ->*) - PEeval l pe == (norm_aux pe)@l. + Lemma norm_aux_spec l pe : PEeval l pe == (norm_aux pe)@l. Proof. - intros. - induction pe;simpl;Esimpl3. - apply mkX_ok. - rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3. - rewrite IHpe1;rewrite IHpe2;rrefl. - rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. rrefl. - rewrite IHpe;rrefl. - rewrite Ppow_N_ok by reflexivity. - rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3. - induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; - repeat rewrite Pmul_ok;rrefl. + induction pe. + - reflexivity. + - apply mkX_ok. + - simpl PEeval. rewrite IHpe1, IHpe2. + simpl. destruct pe1, pe2; Esimpl3. + - simpl. now rewrite IHpe1, IHpe2, Psub_ok. + - simpl. now rewrite IHpe1, IHpe2, Pmul_ok. + - simpl. rewrite IHpe. Esimpl2. + - simpl. rewrite Ppow_N_ok by reflexivity. + rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl2. + induction p;simpl; now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok. Qed. diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 19a98f876..dcaccaa9f 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -51,7 +51,7 @@ Extract Constant Rinv => "fun x -> 1 / x". Extraction "micromega.ml" List.map simpl_cone (*map_cone indexes*) denorm Qpower - n_of_Z N_of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. + n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index 7f6cf79be..114ac0ab4 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -81,14 +81,14 @@ Ltac lra := first [ psatzl R | psatzl Q ]. Ltac lia := - zify ; unfold Zsucc in * ; - (*cbv delta - [Zplus Zminus Zopp Zmult Zpower Zgt Zge Zle Zlt iff not] ;*) xlia ; + zify ; unfold Z.succ in * ; + (*cbv delta - [Z.add Z.sub Z.opp Z.mul Z.pow Z.gt Z.ge Z.le Z.lt iff not] ;*) xlia ; intros __wit __varmap __ff ; change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity. Ltac nia := - zify ; unfold Zsucc in * ; + zify ; unfold Z.succ in * ; xnlia ; intros __wit __varmap __ff ; change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v index f64504a54..74961f1b5 100644 --- a/plugins/micromega/QMicromega.v +++ b/plugins/micromega/QMicromega.v @@ -60,7 +60,7 @@ Proof. Qed. -(*Definition Zeval_expr := eval_pexpr 0 Zplus Zmult Zminus Zopp (fun x => x) (fun x => Z_of_N x) (Zpower).*) +(*Definition Zeval_expr := eval_pexpr 0 Z.add Z.mul Z.sub Z.opp (fun x => x) (fun x => Z.of_N x) (Z.pow).*) Require Import EnvRing. Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q := @@ -71,7 +71,7 @@ Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q := | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2) | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2) | PEopp pe1 => - (Qeval_expr env pe1) - | PEpow pe1 n => Qpower (Qeval_expr env pe1) (Z_of_N n) + | PEpow pe1 n => Qpower (Qeval_expr env pe1) (Z.of_N n) end. Lemma Qeval_expr_simpl : forall env e, @@ -83,7 +83,7 @@ Lemma Qeval_expr_simpl : forall env e, | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2) | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2) | PEopp pe1 => - (Qeval_expr env pe1) - | PEpow pe1 n => Qpower (Qeval_expr env pe1) (Z_of_N n) + | PEpow pe1 n => Qpower (Qeval_expr env pe1) (Z.of_N n) end. Proof. destruct e ; reflexivity. @@ -91,7 +91,7 @@ Qed. Definition Qeval_expr' := eval_pexpr Qplus Qmult Qminus Qopp (fun x => x) (fun x => x) (pow_N 1 Qmult). -Lemma QNpower : forall r n, r ^ Z_of_N n = pow_N 1 Qmult r n. +Lemma QNpower : forall r n, r ^ Z.of_N n = pow_N 1 Qmult r n. Proof. destruct n ; reflexivity. Qed. diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index 2be99da1e..e575ed29e 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -85,17 +85,17 @@ Qed. Ltac INR_nat_of_P := match goal with - | H : context[INR (nat_of_P ?X)] |- _ => + | H : context[INR (Pos.to_nat ?X)] |- _ => revert H ; let HH := fresh in - assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (nat_of_P X)) - | |- context[INR (nat_of_P ?X)] => + assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (Pos.to_nat X)) + | |- context[INR (Pos.to_nat ?X)] => let HH := fresh in - assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (nat_of_P X)) + assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (Pos.to_nat X)) end. Ltac add_eq expr val := set (temp := expr) ; - generalize (refl_equal temp) ; + generalize (eq_refl temp) ; unfold temp at 1 ; generalize temp ; intro val ; clear temp. Ltac Rinv_elim := @@ -210,7 +210,7 @@ Proof. rewrite plus_IZR in *. rewrite mult_IZR in *. simpl. - rewrite nat_of_P_mult_morphism. + rewrite Pos2Nat.inj_mul. rewrite mult_INR. rewrite mult_IZR. simpl. @@ -244,7 +244,7 @@ Proof. simpl. repeat rewrite mult_IZR. simpl. - rewrite nat_of_P_mult_morphism. + rewrite Pos2Nat.inj_mul. rewrite mult_INR. repeat INR_nat_of_P. intros. field ; split ; apply Rlt_neq ; auto. @@ -275,7 +275,7 @@ Proof. apply Rlt_neq ; auto. simpl in H. exfalso. - rewrite Pmult_comm in H. + rewrite Pos.mul_comm in H. compute in H. discriminate. Qed. @@ -291,7 +291,7 @@ Proof. destruct x. unfold Qopp. simpl. - rewrite Zopp_involutive. + rewrite Z.opp_involutive. reflexivity. Qed. @@ -348,7 +348,7 @@ Proof. intros. assert ( 0 > x \/ 0 < x)%Q. destruct x ; unfold Qlt, Qeq in * ; simpl in *. - rewrite Zmult_1_r in *. + rewrite Z.mul_1_r in *. destruct Qnum ; simpl in * ; intuition auto. right. reflexivity. left ; reflexivity. @@ -379,7 +379,7 @@ Proof. Qed. -Notation to_nat := N.to_nat. (*Nnat.nat_of_N*) +Notation to_nat := N.to_nat. Lemma QSORaddon : @SORaddon R @@ -471,7 +471,7 @@ Definition INZ (n:N) : R := | Npos p => IZR (Zpos p) end. -Definition Reval_expr := eval_pexpr Rplus Rmult Rminus Ropp R_of_Rcst nat_of_N pow. +Definition Reval_expr := eval_pexpr Rplus Rmult Rminus Ropp R_of_Rcst N.to_nat pow. Definition Reval_op2 (o:Op2) : R -> R -> Prop := @@ -490,10 +490,10 @@ Definition Reval_formula (e: PolEnv R) (ff : Formula Rcst) := Definition Reval_formula' := - eval_sformula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt nat_of_N pow R_of_Rcst. + eval_sformula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt N.to_nat pow R_of_Rcst. Definition QReval_formula := - eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IQR nat_of_N pow . + eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IQR N.to_nat pow . Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f. Proof. diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 4af650861..48bf3e2ac 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -142,7 +142,7 @@ Qed. Definition PolC := Pol C. (* polynomials in generalized Horner form, defined in Ring_polynom or EnvRing *) Definition PolEnv := Env R. (* For interpreting PolC *) Definition eval_pol (env : PolEnv) (p:PolC) : R := - Pphi 0 rplus rtimes phi env p. + Pphi rplus rtimes phi env p. Inductive Op1 : Set := (* relations with 0 *) | Equal (* == 0 *) @@ -320,7 +320,7 @@ Definition map_option2 (A B C : Type) (f : A -> B -> option C) Arguments map_option2 [A B C] f o o'. -Definition Rops_wd := mk_reqe rplus rtimes ropp req +Definition Rops_wd := mk_reqe (*rplus rtimes ropp req*) sor.(SORplus_wd) sor.(SORtimes_wd) sor.(SORopp_wd). @@ -469,17 +469,11 @@ Fixpoint ge_bool (n m : nat) : bool := end end. -Lemma ge_bool_cases : forall n m, (if ge_bool n m then n >= m else n < m)%nat. +Lemma ge_bool_cases : forall n m, + (if ge_bool n m then n >= m else n < m)%nat. Proof. - induction n ; simpl. - destruct m ; simpl. - constructor. - omega. - destruct m. - constructor. - omega. - generalize (IHn m). - destruct (ge_bool n m) ; omega. + induction n; destruct m ; simpl; auto with arith. + specialize (IHn m). destruct (ge_bool); auto with arith. Qed. @@ -593,7 +587,7 @@ Definition paddC := PaddC cplus. Definition psubC := PsubC cminus. Definition PsubC_ok : forall c P env, eval_pol env (psubC P c) == eval_pol env P - [c] := - let Rops_wd := mk_reqe rplus rtimes ropp req + let Rops_wd := mk_reqe (*rplus rtimes ropp req*) sor.(SORplus_wd) sor.(SORtimes_wd) sor.(SORopp_wd) in @@ -601,7 +595,7 @@ Definition PsubC_ok : forall c P env, eval_pol env (psubC P c) == eval_pol env addon.(SORrm). Definition PaddC_ok : forall c P env, eval_pol env (paddC P c) == eval_pol env P + [c] := - let Rops_wd := mk_reqe rplus rtimes ropp req + let Rops_wd := mk_reqe (*rplus rtimes ropp req*) sor.(SORplus_wd) sor.(SORtimes_wd) sor.(SORopp_wd) in @@ -882,13 +876,14 @@ Qed. Fixpoint xdenorm (jmp : positive) (p: Pol C) : PExpr C := match p with | Pc c => PEc c - | Pinj j p => xdenorm (Pplus j jmp ) p + | Pinj j p => xdenorm (Pos.add j jmp ) p | PX p j q => PEadd (PEmul (xdenorm jmp p) (PEpow (PEX _ jmp) (Npos j))) - (xdenorm (Psucc jmp) q) + (xdenorm (Pos.succ jmp) q) end. -Lemma xdenorm_correct : forall p i env, eval_pol (jump i env) p == eval_pexpr env (xdenorm (Psucc i) p). +Lemma xdenorm_correct : forall p i env, + eval_pol (jump i env) p == eval_pexpr env (xdenorm (Pos.succ i) p). Proof. unfold eval_pol. induction p. @@ -896,22 +891,21 @@ Proof. (* Pinj *) simpl. intros. - rewrite Pplus_succ_permute_r. + rewrite Pos.add_succ_r. rewrite <- IHp. symmetry. - rewrite Pplus_comm. - rewrite Pjump_Pplus. reflexivity. + rewrite Pos.add_comm. + rewrite Pjump_add. reflexivity. (* PX *) simpl. intros. - rewrite <- IHp1. - rewrite <- IHp2. + rewrite <- IHp1, <- IHp2. unfold Env.tail , Env.hd. - rewrite <- Pjump_Pplus. - rewrite <- Pplus_one_succ_r. + rewrite <- Pjump_add. + rewrite Pos.add_1_r. unfold Env.nth. unfold jump at 2. - rewrite Pplus_one_succ_l. + rewrite <- Pos.add_1_l. rewrite addon.(SORpower).(rpow_pow_N). unfold pow_N. ring. Qed. @@ -924,14 +918,14 @@ Proof. induction p. reflexivity. simpl. - rewrite <- Pplus_one_succ_r. + rewrite Pos.add_1_r. apply xdenorm_correct. simpl. intros. rewrite IHp1. unfold Env.tail. rewrite xdenorm_correct. - change (Psucc xH) with 2%positive. + change (Pos.succ xH) with 2%positive. rewrite addon.(SORpower).(rpow_pow_N). simpl. reflexivity. Qed. diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v index 2bf3d8c35..b43ce6f04 100644 --- a/plugins/micromega/ZCoeff.v +++ b/plugins/micromega/ZCoeff.v @@ -109,7 +109,7 @@ Qed. Lemma Zring_morph : ring_morph 0 1 rplus rtimes rminus ropp req - 0%Z 1%Z Zplus Zmult Zminus Zopp + 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool gen_order_phi_Z. Proof. exact (gen_phiZ_morph sor.(SORsetoid) ring_ops_wd sor.(SORrt)). @@ -122,7 +122,7 @@ try apply (Rplus_pos_pos sor); try apply (Rtimes_pos_pos sor); try apply (Rplus_ try apply (Rlt_0_1 sor); assumption. Qed. -Lemma phi_pos1_succ : forall x : positive, phi_pos1 (Psucc x) == 1 + phi_pos1 x. +Lemma phi_pos1_succ : forall x : positive, phi_pos1 (Pos.succ x) == 1 + phi_pos1 x. Proof. exact (ARgen_phiPOS_Psucc sor.(SORsetoid) ring_ops_wd (Rth_ARth sor.(SORsetoid) ring_ops_wd sor.(SORrt))). @@ -130,7 +130,7 @@ Qed. Lemma clt_pos_morph : forall x y : positive, (x < y)%positive -> phi_pos1 x < phi_pos1 y. Proof. -intros x y H. pattern y; apply Plt_ind with x. +intros x y H. pattern y; apply Pos.lt_ind with x. rewrite phi_pos1_succ; apply (Rlt_succ_r sor). clear y H; intros y _ H. rewrite phi_pos1_succ. now apply (Rlt_lt_succ sor). assumption. @@ -150,9 +150,9 @@ apply -> (Ropp_lt_mono sor); apply clt_pos_morph. red. now rewrite Pos.compare_antisym. Qed. -Lemma Zcleb_morph : forall x y : Z, Zle_bool x y = true -> [x] <= [y]. +Lemma Zcleb_morph : forall x y : Z, Z.leb x y = true -> [x] <= [y]. Proof. -unfold Zle_bool; intros x y H. +unfold Z.leb; intros x y H. case_eq (x ?= y)%Z; intro H1; rewrite H1 in H. le_equal. apply Zring_morph.(morph_eq). unfold Zeq_bool; now rewrite H1. le_less. now apply clt_morph. @@ -162,9 +162,9 @@ Qed. Lemma Zcneqb_morph : forall x y : Z, Zeq_bool x y = false -> [x] ~= [y]. Proof. intros x y H. unfold Zeq_bool in H. -case_eq (Zcompare x y); intro H1; rewrite H1 in *; (discriminate || clear H). +case_eq (Z.compare x y); intro H1; rewrite H1 in *; (discriminate || clear H). apply (Rlt_neq sor). now apply clt_morph. -fold (x > y)%Z in H1. rewrite Zgt_iff_lt in H1. +fold (x > y)%Z in H1. rewrite Z.gt_lt_iff in H1. apply (Rneq_symm sor). apply (Rlt_neq sor). now apply clt_morph. Qed. diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index 461f53b54..b65774406 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -34,20 +34,20 @@ Require Import EnvRing. Open Scope Z_scope. -Lemma Zsor : SOR 0 1 Zplus Zmult Zminus Zopp (@eq Z) Zle Zlt. +Lemma Zsor : SOR 0 1 Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt. Proof. constructor ; intros ; subst ; try (intuition (auto with zarith)). apply Zsth. apply Zth. - destruct (Ztrichotomy n m) ; intuition (auto with zarith). - apply Zmult_lt_0_compat ; auto. + destruct (Z.lt_trichotomy n m) ; intuition. + apply Z.mul_pos_pos ; auto. Qed. Lemma ZSORaddon : - SORaddon 0 1 Zplus Zmult Zminus Zopp (@eq Z) Zle (* ring elements *) - 0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *) - Zeq_bool Zle_bool - (fun x => x) (fun x => x) (pow_N 1 Zmult). + SORaddon 0 1 Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le (* ring elements *) + 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (* coefficients *) + Zeq_bool Z.leb + (fun x => x) (fun x => x) (pow_N 1 Z.mul). Proof. constructor. constructor ; intros ; try reflexivity. @@ -65,20 +65,20 @@ Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z := | PEX x => env x | PEadd e1 e2 => Zeval_expr env e1 + Zeval_expr env e2 | PEmul e1 e2 => Zeval_expr env e1 * Zeval_expr env e2 - | PEpow e1 n => Zpower (Zeval_expr env e1) (Z_of_N n) + | PEpow e1 n => Z.pow (Zeval_expr env e1) (Z.of_N n) | PEsub e1 e2 => (Zeval_expr env e1) - (Zeval_expr env e2) - | PEopp e => Zopp (Zeval_expr env e) + | PEopp e => Z.opp (Zeval_expr env e) end. -Definition eval_expr := eval_pexpr Zplus Zmult Zminus Zopp (fun x => x) (fun x => x) (pow_N 1 Zmult). +Definition eval_expr := eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x => x) (fun x => x) (pow_N 1 Z.mul). -Lemma ZNpower : forall r n, r ^ Z_of_N n = pow_N 1 Zmult r n. +Lemma ZNpower : forall r n, r ^ Z.of_N n = pow_N 1 Z.mul r n. Proof. destruct n. reflexivity. simpl. - unfold Zpower_pos. - replace (pow_pos Zmult r p) with (1 * (pow_pos Zmult r p)) by ring. + unfold Z.pow_pos. + replace (pow_pos Z.mul r p) with (1 * (pow_pos Z.mul r p)) by ring. generalize 1. induction p; simpl ; intros ; repeat rewrite IHp ; ring. Qed. @@ -94,10 +94,10 @@ Definition Zeval_op2 (o : Op2) : Z -> Z -> Prop := match o with | OpEq => @eq Z | OpNEq => fun x y => ~ x = y -| OpLe => Zle -| OpGe => Zge -| OpLt => Zlt -| OpGt => Zgt +| OpLe => Z.le +| OpGe => Z.ge +| OpLt => Z.lt +| OpGt => Z.gt end. Definition Zeval_formula (env : PolEnv Z) (f : Formula Z):= @@ -105,23 +105,23 @@ Definition Zeval_formula (env : PolEnv Z) (f : Formula Z):= (Zeval_op2 op) (Zeval_expr env lhs) (Zeval_expr env rhs). Definition Zeval_formula' := - eval_formula Zplus Zmult Zminus Zopp (@eq Z) Zle Zlt (fun x => x) (fun x => x) (pow_N 1 Zmult). + eval_formula Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt (fun x => x) (fun x => x) (pow_N 1 Z.mul). Lemma Zeval_formula_compat : forall env f, Zeval_formula env f <-> Zeval_formula' env f. Proof. destruct f ; simpl. rewrite Zeval_expr_compat. rewrite Zeval_expr_compat. unfold eval_expr. - generalize (eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x) - (fun x : N => x) (pow_N 1 Zmult) env Flhs). - generalize ((eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x) - (fun x : N => x) (pow_N 1 Zmult) env Frhs)). + generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) + (fun x : N => x) (pow_N 1 Z.mul) env Flhs). + generalize ((eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) + (fun x : N => x) (pow_N 1 Z.mul) env Frhs)). destruct Fop ; simpl; intros ; intuition (auto with zarith). Qed. Definition eval_nformula := - eval_nformula 0 Zplus Zmult (@eq Z) Zle Zlt (fun x => x) . + eval_nformula 0 Z.add Z.mul (@eq Z) Z.le Z.lt (fun x => x) . Definition Zeval_op1 (o : Op1) : Z -> Prop := match o with @@ -140,7 +140,7 @@ Qed. Definition ZWitness := Psatz Z. -Definition ZWeakChecker := check_normalised_formulas 0 1 Zplus Zmult Zeq_bool Zle_bool. +Definition ZWeakChecker := check_normalised_formulas 0 1 Z.add Z.mul Zeq_bool Z.leb. Lemma ZWeakChecker_sound : forall (l : list (NFormula Z)) (cm : ZWitness), ZWeakChecker l cm = true -> @@ -154,13 +154,13 @@ Proof. exact H. Qed. -Definition psub := psub Z0 Zplus Zminus Zopp Zeq_bool. +Definition psub := psub Z0 Z.add Z.sub Z.opp Zeq_bool. -Definition padd := padd Z0 Zplus Zeq_bool. +Definition padd := padd Z0 Z.add Zeq_bool. -Definition norm := norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool. +Definition norm := norm 0 1 Z.add Z.mul Z.sub Z.opp Zeq_bool. -Definition eval_pol := eval_pol 0 Zplus Zmult (fun x => x). +Definition eval_pol := eval_pol Z.add Z.mul (fun x => x). Lemma eval_pol_sub : forall env lhs rhs, eval_pol env (psub lhs rhs) = eval_pol env lhs - eval_pol env rhs. Proof. @@ -211,10 +211,10 @@ Proof. repeat rewrite eval_pol_add; repeat rewrite <- eval_pol_norm ; simpl in *; unfold eval_expr; - generalize ( eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x) - (fun x : N => x) (pow_N 1 Zmult) env lhs); - generalize (eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x) - (fun x : N => x) (pow_N 1 Zmult) env rhs) ; intros z1 z2 ; intros ; subst; + generalize ( eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) + (fun x : N => x) (pow_N 1 Z.mul) env lhs); + generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) + (fun x : N => x) (pow_N 1 Z.mul) env rhs) ; intros z1 z2 ; intros ; subst; intuition (auto with zarith). Transparent padd. Qed. @@ -248,17 +248,17 @@ Proof. repeat rewrite eval_pol_add; repeat rewrite <- eval_pol_norm ; simpl in *; unfold eval_expr; - generalize ( eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x) - (fun x : N => x) (pow_N 1 Zmult) env lhs); - generalize (eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x) - (fun x : N => x) (pow_N 1 Zmult) env rhs) ; intros z1 z2 ; intros ; subst; + generalize ( eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) + (fun x : N => x) (pow_N 1 Z.mul) env lhs); + generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) + (fun x : N => x) (pow_N 1 Z.mul) env rhs) ; intros z1 z2 ; intros ; subst; intuition (auto with zarith). Transparent padd. Qed. -Definition Zunsat := check_inconsistent 0 Zeq_bool Zle_bool. +Definition Zunsat := check_inconsistent 0 Zeq_bool Z.leb. -Definition Zdeduce := nformula_plus_nformula 0 Zplus Zeq_bool. +Definition Zdeduce := nformula_plus_nformula 0 Z.add Zeq_bool. Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z)) : bool := @@ -270,7 +270,7 @@ Require Import Zdiv. Open Scope Z_scope. Definition ceiling (a b:Z) : Z := - let (q,r) := Zdiv_eucl a b in + let (q,r) := Z.div_eucl a b in match r with | Z0 => q | _ => q + 1 @@ -279,47 +279,38 @@ Definition ceiling (a b:Z) : Z := Require Import Znumtheory. -Lemma Zdivide_ceiling : forall a b, (b | a) -> ceiling a b = Zdiv a b. +Lemma Zdivide_ceiling : forall a b, (b | a) -> ceiling a b = Z.div a b. Proof. unfold ceiling. intros. apply Zdivide_mod in H. - case_eq (Zdiv_eucl a b). + case_eq (Z.div_eucl a b). intros. change z with (fst (z,z0)). rewrite <- H0. - change (fst (Zdiv_eucl a b)) with (Zdiv a b). + change (fst (Z.div_eucl a b)) with (Z.div a b). change z0 with (snd (z,z0)). rewrite <- H0. - change (snd (Zdiv_eucl a b)) with (Zmod a b). + change (snd (Z.div_eucl a b)) with (Z.modulo a b). rewrite H. reflexivity. Qed. -Lemma narrow_interval_lower_bound : forall a b x, a > 0 -> a * x >= b -> x >= ceiling b a. +Lemma narrow_interval_lower_bound a b x : + a > 0 -> a * x >= b -> x >= ceiling b a. Proof. + rewrite !Z.ge_le_iff. unfold ceiling. - intros. - generalize (Z_div_mod b a H). - destruct (Zdiv_eucl b a). - intros. - destruct H1. - destruct H2. - subst. - destruct (Ztrichotomy z0 0) as [ HH1 | [HH2 | HH3]]; destruct z0 ; try auto with zarith ; try discriminate. - assert (HH :x >= z \/ x < z) by (destruct (Ztrichotomy x z) ; auto with zarith). - destruct HH ;auto. - generalize (Zmult_lt_compat_l _ _ _ H3 H1). - auto with zarith. - clear H2. - assert (HH :x >= z +1 \/ x <= z) by (destruct (Ztrichotomy x z) ; intuition (auto with zarith)). - destruct HH ;auto. - assert (0 < a) by auto with zarith. - generalize (Zmult_lt_0_le_compat_r _ _ _ H2 H1). - intros. - rewrite Zmult_comm in H4. - rewrite (Zmult_comm z) in H4. - auto with zarith. + intros Ha H. + generalize (Z_div_mod b a Ha). + destruct (Z.div_eucl b a) as (q,r). intros (->,(H1,H2)). + destruct r as [|r|r]. + - rewrite Z.add_0_r in H. + apply Z.mul_le_mono_pos_l in H; auto with zarith. + - assert (0 < Z.pos r) by easy. + rewrite Z.add_1_r, Z.le_succ_l. + apply Z.mul_lt_mono_pos_l with a; auto with zarith. + - now elim H1. Qed. (** NB: narrow_interval_upper_bound is Zdiv.Zdiv_le_lower_bound *) @@ -360,7 +351,7 @@ Proof. destruct x ; simpl ; intuition congruence. Qed. -Definition ZgcdM (x y : Z) := Zmax (Zgcd x y) 1. +Definition ZgcdM (x y : Z) := Z.max (Z.gcd x y) 1. Fixpoint Zgcd_pol (p : PolC Z) : (Z * Z) := @@ -378,7 +369,7 @@ Fixpoint Zgcd_pol (p : PolC Z) : (Z * Z) := Fixpoint Zdiv_pol (p:PolC Z) (x:Z) : PolC Z := match p with - | Pc c => Pc (Zdiv c x) + | Pc c => Pc (Z.div c x) | Pinj j p => Pinj j (Zdiv_pol p x) | PX p j q => PX (Zdiv_pol p x) j (Zdiv_pol q x) end. @@ -421,10 +412,10 @@ Proof. intros. simpl. unfold ZgcdM. - generalize (Zgcd_is_pos z1 z2). - generalize (Zmax_spec (Zgcd z1 z2) 1). - generalize (Zgcd_is_pos (Zmax (Zgcd z1 z2) 1) z). - generalize (Zmax_spec (Zgcd (Zmax (Zgcd z1 z2) 1) z) 1). + generalize (Z.gcd_nonneg z1 z2). + generalize (Zmax_spec (Z.gcd z1 z2) 1). + generalize (Z.gcd_nonneg (Z.max (Z.gcd z1 z2) 1) z). + generalize (Zmax_spec (Z.gcd (Z.max (Z.gcd z1 z2) 1) z) 1). auto with zarith. Qed. @@ -433,7 +424,7 @@ Proof. intros. induction H. constructor. - apply Zdivide_trans with (1:= H0) ; assumption. + apply Z.divide_trans with (1:= H0) ; assumption. constructor. auto. constructor ; auto. Qed. @@ -444,20 +435,20 @@ Proof. exists c. ring. Qed. -Lemma Zgcd_minus : forall a b c, (a | c - b ) -> (Zgcd a b | c). +Lemma Zgcd_minus : forall a b c, (a | c - b ) -> (Z.gcd a b | c). Proof. intros a b c (q,Hq). destruct (Zgcd_is_gcd a b) as [(a',Ha) (b',Hb) _]. - set (g:=Zgcd a b) in *; clearbody g. + set (g:=Z.gcd a b) in *; clearbody g. exists (q * a' + b'). - symmetry in Hq. rewrite <- Zeq_plus_swap in Hq. + symmetry in Hq. rewrite <- Z.add_move_r in Hq. rewrite <- Hq, Hb, Ha. ring. Qed. Lemma Zdivide_pol_sub : forall p a b, - 0 < Zgcd a b -> - Zdivide_pol a (PsubC Zminus p b) -> - Zdivide_pol (Zgcd a b) p. + 0 < Z.gcd a b -> + Zdivide_pol a (PsubC Z.sub p b) -> + Zdivide_pol (Z.gcd a b) p. Proof. induction p. simpl. @@ -477,7 +468,7 @@ Proof. Qed. Lemma Zdivide_pol_sub_0 : forall p a, - Zdivide_pol a (PsubC Zminus p 0) -> + Zdivide_pol a (PsubC Z.sub p 0) -> Zdivide_pol a p. Proof. induction p. @@ -496,7 +487,7 @@ Qed. Lemma Zgcd_pol_div : forall p g c, - Zgcd_pol p = (g, c) -> Zdivide_pol g (PsubC Zminus p c). + Zgcd_pol p = (g, c) -> Zdivide_pol g (PsubC Z.sub p c). Proof. induction p ; simpl. (* Pc *) @@ -511,12 +502,12 @@ Proof. case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros. inv H1. unfold ZgcdM at 1. - destruct (Zmax_spec (Zgcd (ZgcdM z1 z2) z) 1) as [HH1 | HH1]; + destruct (Zmax_spec (Z.gcd (ZgcdM z1 z2) z) 1) as [HH1 | HH1]; destruct HH1 as [HH1 HH1'] ; rewrite HH1'. constructor. apply Zdivide_pol_Zdivide with (x:= ZgcdM z1 z2). unfold ZgcdM. - destruct (Zmax_spec (Zgcd z1 z2) 1) as [HH2 | HH2]. + destruct (Zmax_spec (Z.gcd z1 z2) 1) as [HH2 | HH2]. destruct HH2. rewrite H2. apply Zdivide_pol_sub ; auto. @@ -524,9 +515,9 @@ Proof. destruct HH2. rewrite H2. apply Zdivide_pol_one. unfold ZgcdM in HH1. unfold ZgcdM. - destruct (Zmax_spec (Zgcd z1 z2) 1) as [HH2 | HH2]. + destruct (Zmax_spec (Z.gcd z1 z2) 1) as [HH2 | HH2]. destruct HH2. rewrite H2 in *. - destruct (Zgcd_is_gcd (Zgcd z1 z2) z); auto. + destruct (Zgcd_is_gcd (Z.gcd z1 z2) z); auto. destruct HH2. rewrite H2. destruct (Zgcd_is_gcd 1 z); auto. apply Zdivide_pol_Zdivide with (x:= z). @@ -539,7 +530,7 @@ Qed. -Lemma Zgcd_pol_correct_lt : forall p env g c, Zgcd_pol p = (g,c) -> 0 < g -> eval_pol env p = g * (eval_pol env (Zdiv_pol (PsubC Zminus p c) g)) + c. +Lemma Zgcd_pol_correct_lt : forall p env g c, Zgcd_pol p = (g,c) -> 0 < g -> eval_pol env p = g * (eval_pol env (Zdiv_pol (PsubC Z.sub p c) g)) + c. Proof. intros. rewrite <- Zdiv_pol_correct ; auto. @@ -553,8 +544,8 @@ Qed. Definition makeCuttingPlane (p : PolC Z) : PolC Z * Z := let (g,c) := Zgcd_pol p in - if Zgt_bool g Z0 - then (Zdiv_pol (PsubC Zminus p c) g , Zopp (ceiling (Zopp c) g)) + if Z.gtb g Z0 + then (Zdiv_pol (PsubC Z.sub p c) g , Z.opp (ceiling (Z.opp c) g)) else (p,Z0). @@ -562,13 +553,13 @@ Definition genCuttingPlane (f : NFormula Z) : option (PolC Z * Z * Op1) := let (e,op) := f in match op with | Equal => let (g,c) := Zgcd_pol e in - if andb (Zgt_bool g Z0) (andb (negb (Zeq_bool c Z0)) (negb (Zeq_bool (Zgcd g c) g))) + if andb (Z.gtb g Z0) (andb (negb (Zeq_bool c Z0)) (negb (Zeq_bool (Z.gcd g c) g))) then None (* inconsistent *) else (* Could be optimised Zgcd_pol is recomputed *) let (p,c) := makeCuttingPlane e in Some (p,c,Equal) | NonEqual => Some (e,Z0,op) - | Strict => let (p,c) := makeCuttingPlane (PsubC Zminus e 1) in + | Strict => let (p,c) := makeCuttingPlane (PsubC Z.sub e 1) in Some (p,c,NonStrict) | NonStrict => let (p,c) := makeCuttingPlane e in Some (p,c,NonStrict) @@ -595,7 +586,7 @@ Qed. Definition eval_Psatz : list (NFormula Z) -> ZWitness -> option (NFormula Z) := - eval_Psatz 0 1 Zplus Zmult Zeq_bool Zle_bool. + eval_Psatz 0 1 Z.add Z.mul Zeq_bool Z.leb. Definition valid_cut_sign (op:Op1) := @@ -634,9 +625,9 @@ Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof) {struct pf} : bool : (fix label (pfs:list ZArithProof) := fun lb ub => match pfs with - | nil => if Zgt_bool lb ub then true else false - | pf::rsr => andb (ZChecker ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Zplus lb 1%Z) ub) - end) pf (Zopp z1) z2 + | nil => if Z.gtb lb ub then true else false + | pf::rsr => andb (ZChecker ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Z.add lb 1%Z) ub) + end) pf (Z.opp z1) z2 else false | _ , _ => true end @@ -710,12 +701,12 @@ Proof. unfold makeCuttingPlane in H0. revert H0. case_eq (Zgcd_pol e) ; intros g c0. - generalize (Zgt_cases g 0) ; destruct (Zgt_bool g 0). + generalize (Zgt_cases g 0) ; destruct (Z.gtb g 0). intros. inv H2. - change (RingMicromega.eval_pol 0 Zplus Zmult (fun x : Z => x)) with eval_pol in *. + change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in *. apply Zgcd_pol_correct_lt with (env:=env) in H1. - generalize (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Zminus e c0) g)) H0). + generalize (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Z.sub e c0) g)) H0). auto with zarith. auto with zarith. (* g <= 0 *) @@ -733,7 +724,7 @@ Proof. (* Equal *) destruct p as [[e' z] op]. case_eq (Zgcd_pol e) ; intros g c. - case_eq (Zgt_bool g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Zgcd g c) g))) ; [discriminate|]. + case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))) ; [discriminate|]. case_eq (makeCuttingPlane e). intros. inv H3. @@ -741,7 +732,7 @@ Proof. rewrite H1 in H. revert H. change (eval_pol env e = 0) in H2. - case_eq (Zgt_bool g 0). + case_eq (Z.gtb g 0). intros. rewrite <- Zgt_is_gt_bool in H. rewrite Zgcd_pol_correct_lt with (1:= H1) in H2; auto with zarith. @@ -749,7 +740,7 @@ Proof. change (eval_pol env (padd e' (Pc z)) = 0). inv H3. rewrite eval_pol_add. - set (x:=eval_pol env (Zdiv_pol (PsubC Zminus e c) g)) in *; clearbody x. + set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub e c) g)) in *; clearbody x. simpl. rewrite andb_false_iff in H0. destruct H0. @@ -759,8 +750,7 @@ Proof. rewrite negb_false_iff in H0. apply Zeq_bool_eq in H0. subst. simpl. - rewrite Zplus_0_r in H2. - apply Zmult_integral in H2. + rewrite Z.add_0_r, Z.mul_eq_0 in H2. intuition auto with zarith. rewrite negb_false_iff in H0. apply Zeq_bool_eq in H0. @@ -769,7 +759,7 @@ Proof. inv HH. apply Zdivide_opp_r in H4. rewrite Zdivide_ceiling ; auto. - apply Zeq_minus. + apply Z.sub_move_0_r. apply Z.div_unique_exact ; auto with zarith. intros. unfold nformula_of_cutting_plane. @@ -789,7 +779,7 @@ Proof. simpl. auto with zarith. (* Strict *) destruct p as [[e' z] op]. - case_eq (makeCuttingPlane (PsubC Zminus e 1)). + case_eq (makeCuttingPlane (PsubC Z.sub e 1)). intros. inv H1. apply makeCuttingPlane_ns_sound with (env:=env) (2:= H). @@ -813,7 +803,7 @@ Proof. destruct f. destruct o. case_eq (Zgcd_pol p) ; intros g c. - case_eq (Zgt_bool g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Zgcd g c) g))). + case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))). intros. flatten_bool. rewrite negb_true_iff in H5. @@ -823,16 +813,16 @@ Proof. apply Zeq_bool_neq in H. change (eval_pol env p = 0) in H2. rewrite Zgcd_pol_correct_lt with (1:= H0) in H2; auto with zarith. - set (x:=eval_pol env (Zdiv_pol (PsubC Zminus p c) g)) in *; clearbody x. + set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub p c) g)) in *; clearbody x. contradict H5. apply Zis_gcd_gcd; auto with zarith. constructor; auto with zarith. exists (-x). - rewrite <- Zopp_mult_distr_l, Zmult_comm; auto with zarith. + rewrite Z.mul_opp_l, Z.mul_comm; auto with zarith. (**) destruct (makeCuttingPlane p); discriminate. discriminate. - destruct (makeCuttingPlane (PsubC Zminus p 1)) ; discriminate. + destruct (makeCuttingPlane (PsubC Z.sub p 1)) ; discriminate. destruct (makeCuttingPlane p) ; discriminate. Qed. @@ -920,7 +910,7 @@ Proof. unfold nformula_of_cutting_plane in HCutR. unfold eval_nformula in HCutR. unfold RingMicromega.eval_nformula in HCutR. - change (RingMicromega.eval_pol 0 Zplus Zmult (fun x : Z => x)) with eval_pol in HCutR. + change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in HCutR. unfold eval_op1 in HCutR. destruct op1 ; simpl in Hop1 ; try discriminate; rewrite eval_pol_add in HCutR; simpl in HCutR; auto with zarith. @@ -933,7 +923,7 @@ Proof. unfold nformula_of_cutting_plane in HCutL. unfold eval_nformula in HCutL. unfold RingMicromega.eval_nformula in HCutL. - change (RingMicromega.eval_pol 0 Zplus Zmult (fun x : Z => x)) with eval_pol in HCutL. + change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in HCutL. unfold eval_op1 in HCutL. rewrite eval_pol_add in HCutL. simpl in HCutL. destruct op2 ; simpl in Hop2 ; try discriminate ; omega. @@ -944,14 +934,14 @@ Proof. intros. assert (HH :forall x, -z1 <= x <= z2 -> exists pr, (In pr pf /\ - ZChecker ((PsubC Zminus p1 x,Equal) :: l) pr = true)%Z). + ZChecker ((PsubC Z.sub p1 x,Equal) :: l) pr = true)%Z). clear HZ0 Hop1 Hop2 HCutL HCutR H0 H1. revert Hfix. generalize (-z1). clear z1. intro z1. revert z1 z2. induction pf;simpl ;intros. generalize (Zgt_cases z1 z2). - destruct (Zgt_bool z1 z2). + destruct (Z.gtb z1 z2). intros. apply False_ind ; omega. discriminate. @@ -972,7 +962,7 @@ Proof. zify. omega. (*/asser *) destruct (HH _ H1) as [pr [Hin Hcheker]]. - assert (make_impl (eval_nformula env) ((PsubC Zminus p1 (eval_pol env p1),Equal) :: l) False). + assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False). apply (H pr);auto. apply in_bdepth ; auto. rewrite <- make_conj_impl in H2. diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 68dc0319f..48b72f34b 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -301,6 +301,8 @@ struct ["Coq";"Reals" ; "Rpow_def"] ; ] + let z_modules = [["Coq";"ZArith";"BinInt"]] + (** * Initialization : a large amount of Caml symbols are derived from * ZMicromega.v @@ -310,6 +312,7 @@ struct let constant = gen_constant_in_modules "ZMicromega" coq_modules let bin_constant = gen_constant_in_modules "ZMicromega" bin_module let r_constant = gen_constant_in_modules "ZMicromega" r_modules + let z_constant = gen_constant_in_modules "ZMicromega" z_modules (* let constant = gen_constant_in_modules "Omicron" coq_modules *) let coq_and = lazy (init_constant "and") @@ -372,17 +375,17 @@ struct let coq_cutProof = lazy (constant "CutProof") let coq_enumProof = lazy (constant "EnumProof") - let coq_Zgt = lazy (constant "Zgt") - let coq_Zge = lazy (constant "Zge") - let coq_Zle = lazy (constant "Zle") - let coq_Zlt = lazy (constant "Zlt") + let coq_Zgt = lazy (z_constant "Z.gt") + let coq_Zge = lazy (z_constant "Z.ge") + let coq_Zle = lazy (z_constant "Z.le") + let coq_Zlt = lazy (z_constant "Z.lt") let coq_Eq = lazy (init_constant "eq") - let coq_Zplus = lazy (constant "Zplus") - let coq_Zminus = lazy (constant "Zminus") - let coq_Zopp = lazy (constant "Zopp") - let coq_Zmult = lazy (constant "Zmult") - let coq_Zpower = lazy (constant "Zpower") + let coq_Zplus = lazy (z_constant "Z.add") + let coq_Zminus = lazy (z_constant "Z.sub") + let coq_Zopp = lazy (z_constant "Z.opp") + let coq_Zmult = lazy (z_constant "Z.mul") + let coq_Zpower = lazy (z_constant "Z.pow") let coq_Qgt = lazy (constant "Qgt") let coq_Qge = lazy (constant "Qge") |