diff options
Diffstat (limited to 'plugins/micromega/EnvRing.v')
| -rw-r--r-- | plugins/micromega/EnvRing.v | 1257 |
1 files changed, 468 insertions, 789 deletions
diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index 309ebdef..786c3393 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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,26 @@ 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 := - 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 - end. - 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 +412,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 +449,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 +461,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 +477,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,726 +485,446 @@ 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). + + (** Evaluation of a monomial towards 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 => Mphi (tail l) M1 * (hd l) ^ i + end. + + Notation "M @@ l" := (Mphi l M) (at level 10, no associativity). + (** 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. - 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. + 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_ok : forall P P', - (P ?== P') = true -> forall l, P@l == P'@ l. + Lemma Peq_spec P P' : + BoolSpec (forall l, P@l == P'@l) True (P ?== P'). 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. + generalize (Peq_ok P P'). destruct (P ?== P'); auto. Qed. - Lemma Pphi0 : forall l, P0@l == 0. + Lemma Pphi0 l : P0@l == 0. Proof. - intros;simpl;apply (morph0 CRmorph). + simpl;apply (morph0 CRmorph). Qed. -Lemma env_morph : forall p e1 e2, (forall x, e1 x = e2 x) -> - p @ e1 = p @ e2. + Lemma Pphi1 l : P1@l == 1. + Proof. + simpl;apply (morph1 CRmorph). + Qed. + +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. - - Ltac Esimpl := - repeat (progress ( - match goal with - | |- context [P0@?l] => rewrite (Pphi0 l) - | |- context [P1@?l] => rewrite (Pphi1 l) - | |- context [(mkPinj ?j ?P)@?l] => rewrite (mkPinj_ok j l P) - | |- context [(mkPX ?P ?i ?Q)@?l] => rewrite (mkPX_ok l P i Q) - | |- context [[cO]] => rewrite (morph0 CRmorph) - | |- context [[cI]] => rewrite (morph1 CRmorph) - | |- context [[?x +! ?y]] => rewrite ((morph_add CRmorph) x y) - | |- context [[?x *! ?y]] => rewrite ((morph_mul CRmorph) x y) - | |- context [[?x -! ?y]] => rewrite ((morph_sub CRmorph) x y) - | |- context [[-! ?x]] => rewrite ((morph_opp CRmorph) x) - end)); - rsimpl; simpl. - - Lemma PaddC_ok : forall c P l, (PaddC P c)@l == P@l + [c]. + Lemma mkPX_ok l P i Q : + (mkPX P i Q)@l == P@l * (hd l)^i + Q@(tail l). Proof. - induction P;simpl;intros;Esimpl;trivial. - rewrite IHP2;rsimpl. + 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. - Lemma PsubC_ok : forall c P l, (PsubC P c)@l == P@l - [c]. + Hint Rewrite + Pphi0 + Pphi1 + mkPinj_ok + mkPX_ok + (morph0 CRmorph) + (morph1 CRmorph) + (morph0 CRmorph) + (morph_add CRmorph) + (morph_mul CRmorph) + (morph_sub CRmorph) + (morph_opp CRmorph) + : Esimpl. + + (* Quicker than autorewrite with Esimpl :-) *) + Ltac Esimpl := try rewrite_db Esimpl; rsimpl; simpl. + + Lemma PaddC_ok c P l : (PaddC P c)@l == P@l + [c]. Proof. - induction P;simpl;intros. - Esimpl. - rewrite IHP;rsimpl. + revert l;induction P;simpl;intros;Esimpl;trivial. rewrite IHP2;rsimpl. Qed. - Lemma PmulC_aux_ok : forall c P l, (PmulC_aux 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;trivial. - rewrite IHP1;rewrite IHP2;rsimpl. - mul_push ([c]);rrefl. + revert l;induction P;simpl;intros. + - Esimpl. + - rewrite IHP;rsimpl. + - rewrite IHP2;rsimpl. Qed. - Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c]. + Lemma PmulC_aux_ok c P l : (PmulC_aux 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. + revert l;induction P;simpl;intros;Esimpl;trivial. + rewrite IHP1, IHP2;rsimpl. add_permut. mul_permut. Qed. - Lemma Popp_ok : forall P l, (--P)@l == - P@l. + Lemma PmulC_ok c P l : (PmulC P c)@l == P@l * [c]. Proof. - induction P;simpl;intros. - Esimpl. - apply IHP. - rewrite IHP1;rewrite IHP2;rsimpl. + unfold PmulC. + case ceqb_spec; intros H. + - rewrite H; Esimpl. + - case ceqb_spec; intros H'. + + rewrite H'; Esimpl. + + apply PmulC_aux_ok. Qed. - Ltac Esimpl2 := - Esimpl; - repeat (progress ( - match goal with - | |- context [(PaddC ?P ?c)@?l] => rewrite (PaddC_ok c P l) - | |- context [(PsubC ?P ?c)@?l] => rewrite (PsubC_ok c P l) - | |- context [(PmulC ?P ?c)@?l] => rewrite (PmulC_ok c P l) - | |- context [(--?P)@?l] => rewrite (Popp_ok P l) - end)); Esimpl. - - - - - Lemma Padd_ok : forall P' P l, (P ++ P')@l == P@l + P'@l. + Lemma Popp_ok 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. + revert l;induction P;simpl;intros. + - Esimpl. + - apply IHP. + - rewrite IHP1, IHP2;rsimpl. Qed. - Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l. + Hint Rewrite PaddC_ok PsubC_ok PmulC_ok Popp_ok : Esimpl. + + 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 ->;Esimpl. + + 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;Esimpl. + - revert p l; induction P;simpl;intros. + + Esimpl; 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. + + Esimpl. add_permut. + + destruct p0;simpl;Esimpl; 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 ->; Esimpl. + * 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 ->; Esimpl. + + 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;Esimpl. + - revert p l; induction P;simpl;intros. + + Esimpl; 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. + + Esimpl; add_permut. + + destruct p0;simpl;Esimpl; 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 ->; Esimpl. + * 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. + - Esimpl; mul_permut. + - destr_pos_sub; intros ->;Esimpl. + + now rewrite IHP'. + + now rewrite IHP', Pjump_add. + + now rewrite IHP, Pjump_add. + - destruct p0;Esimpl; 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). Esimpl. + + Esimpl. rewrite IHP'1;Esimpl. 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. simpl. Esimpl. + 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;Esimpl. + - apply IHP. + - rewrite Padd_ok, Pmul_ok;Esimpl. + 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. simpl. Esimpl. 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'. replace P3 with (R1 ++ P2 ** S1). + - rewrite EQ', Padd_ok, Pmul_ok; rsimpl. + - revert EQ. destruct S1; try now injection 1. + case ceqb_spec; now inversion 2. 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; inversion_clear 1. + intros. rewrite <- 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 => (M1@@l == 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 +943,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 +956,23 @@ 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. *) + Hint Rewrite Padd_ok Psub_ok : Esimpl. 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 +981,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,62 +1026,57 @@ Section POWER. Definition norm_subst pe := subst_l (norm_aux pe). - (* - Fixpoint norm_subst (pe:PExpr) : Pol := + (** Internally, [norm_aux] is expanded in a large number of cases. + To speed-up proofs, we use an alternative definition. *) + + Definition get_PEopp pe := 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 + | PEopp pe' => Some pe' + | _ => None end. - Lemma norm_subst_spec : - forall l pe, MPcond lmp l -> - PEeval l pe == (norm_subst pe)@l. + Lemma norm_aux_PEadd pe1 pe2 : + norm_aux (PEadd pe1 pe2) = + match get_PEopp pe1, get_PEopp pe2 with + | Some pe1', _ => (norm_aux pe2) -- (norm_aux pe1') + | None, Some pe2' => (norm_aux pe1) -- (norm_aux pe2') + | None, None => (norm_aux pe1) ++ (norm_aux pe2) + end. 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. + simpl (norm_aux (PEadd _ _)). + destruct pe1; [ | | | | | reflexivity | ]; + destruct pe2; simpl get_PEopp; reflexivity. Qed. -*) - Lemma norm_aux_spec : - forall l pe, (*MPcond lmp l ->*) - PEeval l pe == (norm_aux pe)@l. + + Lemma norm_aux_PEopp pe : + match get_PEopp pe with + | Some pe' => norm_aux pe = -- (norm_aux pe') + | None => True + end. 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. + now destruct pe. Qed. + Lemma norm_aux_spec l pe : + PEeval l pe == (norm_aux pe)@l. + Proof. + intros. + induction pe. + - reflexivity. + - apply mkX_ok. + - simpl PEeval. rewrite IHpe1, IHpe2. + assert (H1 := norm_aux_PEopp pe1). + assert (H2 := norm_aux_PEopp pe2). + rewrite norm_aux_PEadd. + do 2 destruct get_PEopp; rewrite ?H1, ?H2; Esimpl; add_permut. + - simpl. rewrite IHpe1, IHpe2. Esimpl. + - simpl. rewrite IHpe1, IHpe2. now rewrite Pmul_ok. + - simpl. rewrite IHpe. Esimpl. + - simpl. rewrite Ppow_N_ok by reflexivity. + rewrite pow_th.(rpow_pow_N). destruct n0; simpl; Esimpl. + induction p;simpl; now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok. + Qed. End NORM_SUBST_REC. - End MakeRingPol. - |