From 7d220f8b61649646692983872626d6a8042446a9 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 20 Mar 2009 01:22:58 +0000 Subject: Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/micromega/EnvRing.v | 1403 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1403 insertions(+) create mode 100644 plugins/micromega/EnvRing.v (limited to 'plugins/micromega/EnvRing.v') diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v new file mode 100644 index 000000000..04e68272e --- /dev/null +++ b/plugins/micromega/EnvRing.v @@ -0,0 +1,1403 @@ +(************************************************************************) +(* V * The Coq Proof Assistant / The Coq Development Team *) +(* R->R) (ropp : R->R). + Variable req : R -> R -> Prop. + + (* Ring properties *) + Variable Rsth : Setoid_Theory R req. + Variable Reqe : ring_eq_ext radd rmul ropp req. + Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req. + + (* Coefficients *) + Variable C: Type. + Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C). + Variable ceqb : C->C->bool. + Variable phi : C -> R. + Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req + cO cI cadd cmul csub copp ceqb phi. + + (* Power coefficients *) + Variable Cpow : Set. + 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). + + (* 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. + 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. + + (* Definition of multivariable polynomials with coefficients in C : + Type [Pol] represents [X1 ... Xn]. + The representation is Horner's where a [n] variable polynomial + (C[X1..Xn]) is seen as a polynomial on [X1] which coefficients + are polynomials with [n-1] variables (C[X2..Xn]). + There are several optimisations to make the repr compacter: + - [Pc c] is the constant polynomial of value c + == c*X1^0*..*Xn^0 + - [Pinj j Q] is a polynomial constant w.r.t the [j] first variables. + variable indices are shifted of j in Q. + == X1^0 *..* Xj^0 * Q{X1 <- Xj+1;..; Xn-j <- Xn} + - [PX P i Q] is an optimised Horner form of P*X^i + Q + with P not the null polynomial + == P * X1^i + Q{X1 <- X2; ..; Xn-1 <- Xn} + + In addition: + - polynomials of the form (PX (PX P i (Pc 0)) j Q) are forbidden + since they can be represented by the simpler form (PX P (i+j) Q) + - (Pinj i (Pinj j P)) is (Pinj (i+j) P) + - (Pinj i (Pc c)) is (Pc c) + *) + + Inductive Pol : Type := + | Pc : C -> Pol + | Pinj : positive -> Pol -> Pol + | PX : Pol -> positive -> Pol -> Pol. + + Definition P0 := Pc cO. + Definition P1 := Pc cI. + + Fixpoint Peq (P P' : Pol) {struct P'} : bool := + match P, P' with + | Pc c, Pc c' => c ?=! c' + | Pinj j Q, Pinj j' Q' => + match Pcompare j j' Eq with + | Eq => Peq Q Q' + | _ => false + end + | PX P i Q, PX P' i' Q' => + match Pcompare i i' Eq with + | Eq => if Peq P P' then Peq Q Q' else false + | _ => false + end + | _, _ => false + end. + + Notation " P ?== P' " := (Peq P P'). + + Definition mkPinj j P := + match P with + | Pc _ => P + | Pinj j' Q => Pinj ((j + j'):positive) Q + | _ => Pinj j P + end. + + Definition mkPinj_pred j P:= + match j with + | xH => P + | xO j => Pinj (Pdouble_minus_one j) P + | xI j => Pinj (xO j) P + end. + + Definition mkPX P i Q := + match P with + | Pc c => if c ?=! cO then mkPinj xH Q else PX P i Q + | Pinj _ _ => PX P i Q + | PX P' i' Q' => if Q' ?== P0 then PX P' (i' + i) Q else PX P i Q + end. + + Definition mkXi i := PX P1 i P0. + + Definition mkX := mkXi 1. + + (** Opposite of addition *) + + Fixpoint Popp (P:Pol) : Pol := + match P with + | Pc c => Pc (-! c) + | Pinj j Q => Pinj j (Popp Q) + | PX P i Q => PX (Popp P) i (Popp Q) + end. + + Notation "-- P" := (Popp P). + + (** Addition et subtraction *) + + Fixpoint PaddC (P:Pol) (c:C) {struct P} : 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 := + match P with + | Pc c1 => Pc (c1 -! c) + | Pinj j Q => Pinj j (PsubC Q c) + | PX P i Q => PX P i (PsubC Q c) + end. + + Section PopI. + + Variable Pop : Pol -> Pol -> Pol. + Variable Q : Pol. + + Fixpoint PaddI (j:positive) (P:Pol){struct P} : Pol := + match P with + | Pc c => mkPinj j (PaddC Q c) + | Pinj j' Q' => + match ZPminus 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') + end + | 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') + | xI j => PX P i (PaddI (xO j) Q') + end + end. + + Fixpoint PsubI (j:positive) (P:Pol){struct P} : Pol := + match P with + | Pc c => mkPinj j (PaddC (--Q) c) + | Pinj j' Q' => + match ZPminus 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') + end + | 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') + | xI j => PX P i (PsubI (xO j) Q') + end + end. + + Variable P' : Pol. + + Fixpoint PaddX (i':positive) (P:Pol) {struct P} : 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') + | xI j => PX P' i' (Pinj (xO j) Q') + end + | PX P i Q' => + match ZPminus 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 := + 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') + | xI j => PX (--P') i' (Pinj (xO j) Q') + end + | PX P i Q' => + match ZPminus 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' + end + end. + + + End PopI. + + Fixpoint Padd (P P': Pol) {struct P'} : Pol := + match P' with + | Pc c' => PaddC P c' + | Pinj j' Q' => PaddI Padd Q' j' P + | PX P' i' Q' => + match P with + | Pc c => PX P' i' (PaddC Q' c) + | 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') + | xI j => PX P' i' (Padd (Pinj (xO j) Q) Q') + end + | PX P i Q => + match ZPminus 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'). + + Fixpoint Psub (P P': Pol) {struct P'} : Pol := + match P' with + | Pc c' => PsubC P c' + | Pinj j' Q' => PsubI Psub Q' j' P + | PX P' i' Q' => + match P with + | Pc c => PX (--P') i' (*(--(PsubC Q' c))*) (PaddC (--Q') c) + | 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') + | xI j => PX (--P') i' (Psub (Pinj (xO j) Q) Q') + end + | PX P i Q => + match ZPminus 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'). + + (** Multiplication *) + + Fixpoint PmulC_aux (P:Pol) (c:C) {struct P} : Pol := + match P with + | Pc c' => Pc (c' *! c) + | Pinj j Q => mkPinj j (PmulC_aux Q c) + | PX P i Q => mkPX (PmulC_aux P c) i (PmulC_aux Q c) + end. + + Definition PmulC P c := + if c ?=! cO then P0 else + if c ?=! cI then P else PmulC_aux P c. + + Section PmulI. + Variable Pmul : Pol -> Pol -> Pol. + Variable Q : Pol. + Fixpoint PmulI (j:positive) (P:Pol) {struct P} : Pol := + match P with + | Pc c => mkPinj j (PmulC Q c) + | Pinj j' Q' => + match ZPminus 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') + end + | 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') + | 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 + | Pc c => PmulC P c + | Pinj j' Q' => PmulI Pmul Q' j' P + | PX P' i' Q' => + match P with + | Pc c => PmulC P'' c + | Pinj j Q => + let QQ' := + match j with + | xH => Pmul Q Q' + | xO j => Pmul (Pinj (Pdouble_minus_one j) Q) Q' + | xI j => Pmul (Pinj (xO j) Q) Q' + end in + mkPX (Pmul P P') i' QQ' + | PX P i Q=> + let QQ' := Pmul Q Q' in + let PQ' := PmulI Pmul Q' xH P in + let QP' := Pmul (mkPinj xH Q) P' in + let PP' := Pmul P P' in + (mkPX (mkPX PP' i P0 ++ QP') i' P0) ++ mkPX PQ' i QQ' + 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'). + + Fixpoint Psquare (P:Pol) : Pol := + match P with + | Pc c => Pc (c *! c) + | Pinj j Q => Pinj j (Psquare Q) + | PX P i Q => + let twoPQ := Pmul P (mkPinj xH (PmulC Q (cI +! cI))) in + let Q2 := Psquare Q in + let P2 := Psquare P in + mkPX (mkPX P2 i P0 ++ twoPQ) i Q2 + end. + + (** Monomial **) + + Inductive Mon: Set := + 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. + + Definition mkVmon i M := + match M with + | mon0 => vmon i mon0 + | zmon j m => vmon i (zmon_pred j m) + | vmon i' m => vmon (i+i') m + end. + + Fixpoint MFactor (P: Pol) (M: Mon) {struct P}: Pol * Pol := + match P, M with + _, mon0 => (Pc cO, P) + | Pc _, _ => (P, Pc cO) + | Pinj j1 P1, zmon j2 M1 => + match (j1 ?= j2) Eq with + Eq => let (R,S) := MFactor P1 M1 in + (mkPinj j1 R, mkPinj j1 S) + | Lt => let (R,S) := MFactor P1 (zmon (j2 - j1) M1) in + (mkPinj j1 R, mkPinj j1 S) + | Gt => (P, Pc cO) + end + | Pinj _ _, vmon _ _ => (P, Pc cO) + | PX P1 i Q1, zmon j M1 => + let M2 := zmon_pred j M1 in + let (R1, S1) := MFactor P1 M in + let (R2, S2) := MFactor Q1 M2 in + (mkPX R1 i R2, mkPX S1 i S2) + | PX P1 i Q1, vmon j M1 => + match (i ?= j) Eq with + Eq => let (R1,S1) := MFactor P1 (mkZmon xH M1) in + (mkPX R1 i Q1, S1) + | Lt => let (R1,S1) := MFactor P1 (vmon (j - i) M1) in + (mkPX R1 i Q1, S1) + | Gt => let (R1,S1) := MFactor P1 (mkZmon xH M1) in + (mkPX R1 i Q1, mkPX S1 (i-j) (Pc cO)) + end + end. + + Definition POneSubst (P1: Pol) (M1: Mon) (P2: Pol): option Pol := + let (Q1,R1) := MFactor P1 M1 in + match R1 with + (Pc c) => if c ?=! cO then None + else Some (Padd Q1 (Pmul P2 R1)) + | _ => Some (Padd Q1 (Pmul P2 R1)) + end. + + Fixpoint PNSubst1 (P1: Pol) (M1: Mon) (P2: Pol) (n: nat) {struct n}: Pol := + match POneSubst P1 M1 P2 with + Some P3 => match n with S n1 => PNSubst1 P3 M1 P2 n1 | _ => P3 end + | _ => P1 + end. + + Definition PNSubst (P1: Pol) (M1: Mon) (P2: Pol) (n: nat): option Pol := + match POneSubst P1 M1 P2 with + Some P3 => match n with S n1 => Some (PNSubst1 P3 M1 P2 n1) | _ => None end + | _ => None + end. + + Fixpoint PSubstL1 (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}: + 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 := + match LM1 with + cons (M1,P2) LM2 => + match PNSubst P1 M1 P2 n with + Some P3 => Some (PSubstL1 P3 LM2 n) + | None => PSubstL P1 LM2 n + end + | _ => None + end. + + Fixpoint PNSubstL (P1: Pol) (LM1: list (Mon * Pol)) (m n: nat) {struct m}: Pol := + match PSubstL P1 LM1 n with + Some P3 => match m with S m1 => PNSubstL P3 LM1 m1 n | _ => P3 end + | _ => P1 + end. + + (** Evaluation of a polynomial towards R *) + + Fixpoint Pphi(l:Env R) (P:Pol) {struct P} : 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) + 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 + end. + 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. + Qed. + + Lemma Peq_ok : forall P P', + (P ?== P') = true -> forall l, P@l == P'@ l. + Proof. + induction P;destruct P';simpl;intros;try discriminate;trivial. + apply (morph_eq CRmorph);trivial. + assert (H1 := Pcompare_Eq_eq p p0); destruct ((p ?= p0)%positive Eq); + try discriminate H. + rewrite (IHP P' H); rewrite H1;trivial;rrefl. + assert (H1 := Pcompare_Eq_eq p p0); destruct ((p ?= p0)%positive Eq); + 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. + Qed. + + Lemma Pphi0 : forall l, P0@l == 0. + Proof. + intros;simpl;apply (morph0 CRmorph). + Qed. + +Lemma env_morph : forall 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. +Qed. + +Lemma Pjump_Pplus : forall 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. +Qed. + +Lemma Pjump_xO_tail : forall 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. +Qed. + +Lemma Pjump_Pdouble_minus_one : forall P p l, + P @ (jump (Pdouble_minus_one 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. +Qed. + + + + Lemma Pphi1 : forall l, P1@l == 1. + Proof. + intros;simpl;apply (morph1 CRmorph). + Qed. + + Lemma mkPinj_ok : forall j l P, (mkPinj j P)@l == P@(jump j l). + Proof. + intros j l p;destruct p;simpl;rsimpl. + rewrite Pjump_Pplus. + reflexivity. + 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). + 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. + 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]. + Proof. + induction P;simpl;intros;Esimpl;trivial. + rewrite IHP2;rsimpl. + Qed. + + Lemma PsubC_ok : forall c P l, (PsubC P c)@l == P@l - [c]. + Proof. + 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]. + Proof. + induction P;simpl;intros;Esimpl;trivial. + rewrite IHP1;rewrite IHP2;rsimpl. + mul_push ([c]);rrefl. + Qed. + + Lemma PmulC_ok : forall 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. + Qed. + + Lemma Popp_ok : forall P l, (--P)@l == - P@l. + Proof. + induction P;simpl;intros. + Esimpl. + apply IHP. + rewrite IHP1;rewrite IHP2;rsimpl. + 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. + 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. + 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. + 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). + 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. + 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). + 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. + Qed. + + Lemma Pmul_aux_ok : forall P' P l,(Pmul_aux 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. + Qed. +*) + +(* Proof for the symmetric version *) + Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * 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. + Qed. + +(* +Lemma Pmul_ok : forall 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. + Qed. +*) + + Lemma Psquare_ok : forall 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. + Qed. + + Lemma Mphi_morph : forall P env env', (forall x, env x = env' x ) -> + Mphi env P = Mphi env' P. + 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. + Qed. + +Lemma Mjump_xO_tail : forall M p l, + Mphi (jump (xO p) (tail l)) M = Mphi (jump (xI p) l) M. +Proof. + intros. + apply Mphi_morph. + intros. + rewrite (@jump_simpl R (xI p)). + rewrite (@jump_simpl R (xO p)). + reflexivity. +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. +Proof. + intros. + apply Mphi_morph. + intros. + rewrite jump_Pdouble_minus_one. + rewrite (@jump_simpl R (xO p)). + reflexivity. +Qed. + +Lemma Mjump_Pplus : forall M i j l, Mphi (jump (i + j) l ) M = Mphi (jump j (jump i l)) M. +Proof. + intros. apply Mphi_morph. intros. rewrite <- jump_Pplus. + rewrite Pplus_comm. + reflexivity. +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. + Qed. + + Lemma zmon_pred_ok : forall M j l, + Mphi (tail l) (zmon_pred j M) == Mphi l (zmon j M). + 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. + Qed. + + Lemma mkVmon_ok : forall M i l, Mphi l (mkVmon i M) == Mphi l M*pow_pos rmul (hd 0 l) i. + Proof. + destruct M;simpl;intros;rsimpl. + rewrite zmon_pred_ok;simpl;rsimpl. + rewrite Pplus_comm;rewrite pow_pos_Pplus;rsimpl. + Qed. + + + Lemma Mphi_ok: forall P M l, + let (Q,R) := MFactor P M in + P@l == Q@l + (Mphi l M) * (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) Eq); intros He; simpl. + rewrite (Pcompare_Eq_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) Eq); intros He; simpl. + rewrite (Pcompare_Eq_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. + 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. + 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. + Qed. +*) + Lemma PNSubst1_ok: forall n P1 M1 P2 l, + Mphi l M1 == 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. + 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. + 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. + 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. + + Lemma PSubstL1_ok: forall 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. + Qed. + + Lemma PSubstL_ok: forall 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. + Qed. + + Lemma PNSubstL_ok: forall 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. + Qed. + + (** Definition of polynomial expressions *) + + Inductive PExpr : Type := + | PEc : C -> PExpr + | PEX : positive -> PExpr + | PEadd : PExpr -> PExpr -> PExpr + | PEsub : PExpr -> PExpr -> PExpr + | PEmul : PExpr -> PExpr -> PExpr + | PEopp : PExpr -> PExpr + | PEpow : PExpr -> N -> PExpr. + + (** evaluation of polynomial expressions towards R *) + Definition mk_X j := mkPinj_pred j mkX. + + (** evaluation of polynomial expressions towards R *) + + Fixpoint PEeval (l:Env R) (pe:PExpr) {struct pe} : R := + match pe with + | PEc c => phi c + | PEX j => nth j l + | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2) + | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2) + | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2) + | PEopp pe1 => - (PEeval l pe1) + | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n) + end. + + (** Correctness proofs *) + + Lemma mkX_ok : forall 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. + 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. *) + +Section POWER. + Variable subst_l : Pol -> Pol. + Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol := + match p with + | xH => subst_l (Pmul 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) + end. + + Definition Ppow_N P n := + match n with + | N0 => P1 + | 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. + 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. + 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. + + End POWER. + + (** Normalization and rewriting *) + + Section NORM_SUBST_REC. + Variable n : nat. + Variable lmp:list (Mon*Pol). + Let subst_l P := PNSubstL P lmp n n. + Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2). + Let Ppow_subst := Ppow_N subst_l. + + Fixpoint norm_aux (pe:PExpr) : Pol := + match pe with + | PEc c => Pc c + | PEX j => mk_X j + | PEadd (PEopp pe1) pe2 => Psub (norm_aux pe2) (norm_aux pe1) + | PEadd pe1 (PEopp pe2) => + Psub (norm_aux pe1) (norm_aux pe2) + | PEadd pe1 pe2 => Padd (norm_aux pe1) (norm_aux pe2) + | PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2) + | PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2) + | PEopp pe1 => Popp (norm_aux pe1) + | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n + end. + + 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_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. + 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. + Qed. + + + End NORM_SUBST_REC. + + +End MakeRingPol. + -- cgit v1.2.3