diff options
Diffstat (limited to 'plugins/setoid_ring/Ring_polynom.v')
| -rw-r--r-- | plugins/setoid_ring/Ring_polynom.v | 386 |
1 files changed, 193 insertions, 193 deletions
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index d88470369..faa83dedc 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -18,21 +18,21 @@ Open Local Scope positive_scope. Import RingSyntax. Section MakeRingPol. - - (* Ring elements *) + + (* Ring elements *) Variable R:Type. Variable (rO rI : R) (radd rmul rsub: R->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 *) + (* Coefficients *) Variable C: Type. Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C). - Variable ceqb : C->C->bool. + 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. @@ -40,7 +40,7 @@ Section MakeRingPol. (* Power coefficients *) Variable Cpow : Set. Variable Cp_phi : N -> Cpow. - Variable rpow : R -> Cpow -> R. + Variable rpow : R -> Cpow -> R. Variable pow_th : power_theory rI rmul req Cp_phi rpow. (* division is ok *) @@ -54,12 +54,12 @@ Section MakeRingPol. Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). Notation "x == y" := (req x y). - (* C notations *) + (* 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). - (* Useful tactics *) + (* Useful tactics *) Add Setoid R req Rsth as R_set1. Ltac rrefl := gen_reflexivity Rsth. Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. @@ -93,20 +93,20 @@ Section MakeRingPol. *) Inductive Pol : Type := - | Pc : C -> Pol - | Pinj : positive -> Pol -> Pol + | 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 := + + Fixpoint Peq (P P' : Pol) {struct P'} : bool := match P, P' with | Pc c, Pc c' => c ?=! c' - | Pinj j Q, Pinj j' Q' => + | Pinj j Q, Pinj j' Q' => match Pcompare j j' Eq with - | Eq => Peq Q Q' - | _ => false + | Eq => Peq Q Q' + | _ => false end | PX P i Q, PX P' i' Q' => match Pcompare i i' Eq with @@ -119,7 +119,7 @@ Section MakeRingPol. Notation " P ?== P' " := (Peq P P'). Definition mkPinj j P := - match P with + match P with | Pc _ => P | Pinj j' Q => Pinj ((j + j'):positive) Q | _ => Pinj j P @@ -132,7 +132,7 @@ Section MakeRingPol. | xI j => Pinj (xO j) P end. - Definition mkPX P i Q := + 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 @@ -142,20 +142,20 @@ Section MakeRingPol. Definition mkXi i := PX P1 i P0. Definition mkX := mkXi 1. - + (** Opposite of addition *) - - Fixpoint Popp (P:Pol) : Pol := + + 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) @@ -178,39 +178,39 @@ Section MakeRingPol. Fixpoint PaddI (j:positive) (P:Pol){struct P} : Pol := match P with | Pc c => mkPinj j (PaddC Q c) - | Pinj j' Q' => + | 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' => + | 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 end. Fixpoint PsubI (j:positive) (P:Pol){struct P} : Pol := match P with | Pc c => mkPinj j (PaddC (--Q) c) - | Pinj j' Q' => + | 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' => + | 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 end. - + Variable P' : Pol. - + Fixpoint PaddX (i':positive) (P:Pol) {struct P} : Pol := match P with | Pc c => PX P' i' P @@ -245,7 +245,7 @@ Section MakeRingPol. end end. - + End PopI. Fixpoint Padd (P P': Pol) {struct P'} : Pol := @@ -255,12 +255,12 @@ Section MakeRingPol. | PX P' i' Q' => match P with | Pc c => PX P' i' (PaddC Q' c) - | Pinj j Q => + | 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 + end | PX P i Q => match ZPminus i i' with | Zpos k => mkPX (Padd (PX P k P0) P') i' (Padd Q Q') @@ -278,12 +278,12 @@ Section MakeRingPol. | PX P' i' Q' => match P with | Pc c => PX (--P') i' (*(--(PsubC Q' c))*) (PaddC (--Q') c) - | Pinj j Q => + | 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 + end | PX P i Q => match ZPminus i i' with | Zpos k => mkPX (Psub (PX P k P0) P') i' (Psub Q Q') @@ -293,8 +293,8 @@ Section MakeRingPol. end end. Notation "P -- P'" := (Psub P P'). - - (** Multiplication *) + + (** Multiplication *) Fixpoint PmulC_aux (P:Pol) (c:C) {struct P} : Pol := match P with @@ -306,14 +306,14 @@ Section MakeRingPol. Definition PmulC P c := if c ?=! cO then P0 else if c ?=! cI then P else PmulC_aux P c. - - Section PmulI. + + 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' => + | Pinj j' Q' => match ZPminus j' j with | Zpos k => mkPinj j (Pmul (Pinj k Q') Q) | Z0 => mkPinj j (Pmul Q' Q) @@ -326,7 +326,7 @@ Section MakeRingPol. | xI j' => mkPX (PmulI j P') i' (PmulI (xO j') Q') end end. - + End PmulI. (* A symmetric version of the multiplication *) @@ -338,10 +338,10 @@ Section MakeRingPol. match P with | Pc c => PmulC P'' c | Pinj j Q => - let QQ' := + let QQ' := match j with | xH => Pmul Q Q' - | xO j => Pmul (Pinj (Pdouble_minus_one j) 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' @@ -352,15 +352,15 @@ Section MakeRingPol. let PP' := Pmul P P' in (mkPX (mkPX PP' i P0 ++ QP') i' P0) ++ mkPX PQ' i QQ' end - 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' => + | PX P' i' Q' => (mkPX (Pmul_aux P P') i' P0) ++ (PmulI Pmul_aux Q' xH P) end. @@ -368,7 +368,7 @@ Section MakeRingPol. match P with | Pc c => PmulC P' c | Pinj j Q => PmulI Pmul_aux Q j P' - | PX P i Q => + | PX P i Q => (mkPX (Pmul_aux P P') i P0) ++ (PmulI Pmul_aux Q xH P') end. *) @@ -378,7 +378,7 @@ Section MakeRingPol. match P with | Pc c => Pc (c *! c) | Pinj j Q => Pinj j (Psquare Q) - | PX P i 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 @@ -386,10 +386,10 @@ Section MakeRingPol. end. (** Monomial **) - + Inductive Mon: Set := - mon0: Mon - | zmon: positive -> Mon -> Mon + mon0: Mon + | zmon: positive -> Mon -> Mon | vmon: positive -> Mon -> Mon. Fixpoint Mphi(l:list R) (M: Mon) {struct M} : R := @@ -399,7 +399,7 @@ Section MakeRingPol. | vmon i M1 => let x := hd 0 l in let xi := pow_pos rmul x i in - (Mphi (tail l) M1) * xi + (Mphi (tail l) M1) * xi end. Definition mkZmon j M := @@ -409,8 +409,8 @@ Section MakeRingPol. match j with xH => M | _ => mkZmon (Ppred j) M end. Definition mkVmon i M := - match M with - | mon0 => vmon i mon0 + match M with + | mon0 => vmon i mon0 | zmon j m => vmon i (zmon_pred j m) | vmon i' m => vmon (i+i') m end. @@ -462,35 +462,35 @@ Section MakeRingPol. Definition POneSubst (P1: Pol) (cM1: C * Mon) (P2: Pol): option Pol := let (c,M1) := cM1 in let (Q1,R1) := MFactor P1 c M1 in - match R1 with - (Pc c) => if c ?=! cO then None + 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) (cM1: C * Mon) (P2: Pol) (n: nat) {struct n}: Pol := - match POneSubst P1 cM1 P2 with + match POneSubst P1 cM1 P2 with Some P3 => match n with S n1 => PNSubst1 P3 cM1 P2 n1 | _ => P3 end | _ => P1 end. Definition PNSubst (P1: Pol) (cM1: C * Mon) (P2: Pol) (n: nat): option Pol := - match POneSubst P1 cM1 P2 with + match POneSubst P1 cM1 P2 with Some P3 => match n with S n1 => Some (PNSubst1 P3 cM1 P2 n1) | _ => None end | _ => None end. - - Fixpoint PSubstL1 (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) {struct LM1}: + + Fixpoint PSubstL1 (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) {struct LM1}: Pol := - match LM1 with + match LM1 with cons (M1,P2) LM2 => PSubstL1 (PNSubst1 P1 M1 P2 n) LM2 n | _ => P1 end. Fixpoint PSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) {struct LM1}: option Pol := - match LM1 with + match LM1 with cons (M1,P2) LM2 => - match PNSubst P1 M1 P2 n with + match PNSubst P1 M1 P2 n with Some P3 => Some (PSubstL1 P3 LM2 n) | None => PSubstL P1 LM2 n end @@ -498,7 +498,7 @@ Section MakeRingPol. end. Fixpoint PNSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (m n: nat) {struct m}: Pol := - match PSubstL P1 LM1 n with + match PSubstL P1 LM1 n with Some P3 => match m with S m1 => PNSubstL P3 LM1 m1 n | _ => P3 end | _ => P1 end. @@ -509,10 +509,10 @@ Section MakeRingPol. match P with | Pc c => [c] | Pinj j Q => Pphi (jump j l) Q - | PX P i 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) + (Pphi l P) * xi + (Pphi (tail l) Q) end. Reserved Notation "P @ l " (at level 10, no associativity). @@ -546,8 +546,8 @@ Section MakeRingPol. rewrite Psucc_o_double_minus_one_eq_xO;trivial. simpl;trivial. Qed. - - Lemma Peq_ok : forall P P', + + 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. @@ -580,10 +580,10 @@ Section MakeRingPol. rewrite <-jump_Pplus;rewrite Pplus_comm;rrefl. Qed. - Let pow_pos_Pplus := + 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, + 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. @@ -616,8 +616,8 @@ Section MakeRingPol. | -! ?x => rewrite ((morph_opp CRmorph) x) end end)); - rsimpl; simpl. - + rsimpl; simpl. + Lemma PaddC_ok : forall c P l, (PaddC P c)@l == P@l + [c]. Proof. induction P;simpl;intros;Esimpl;trivial. @@ -637,7 +637,7 @@ Section MakeRingPol. induction P;simpl;intros;Esimpl;trivial. rewrite IHP1;rewrite IHP2;rsimpl. mul_push ([c]);rrefl. - Qed. + Qed. Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c]. Proof. @@ -660,7 +660,7 @@ Section MakeRingPol. Ltac Esimpl2 := Esimpl; repeat (progress ( - match goal with + 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) @@ -684,7 +684,7 @@ Section MakeRingPol. rewrite IHP2;simpl. rewrite jump_Pdouble_minus_one;rsimpl. rewrite IHP';rsimpl. - destruct P;simpl. + destruct P;simpl. Esimpl2;add_push [c];rrefl. destruct p0;simpl;Esimpl2. rewrite IHP'2;simpl. @@ -699,7 +699,7 @@ Section MakeRingPol. rewrite H;rewrite Pplus_comm. rewrite pow_pos_Pplus;rsimpl. add_push (P3 @ (tail l));rrefl. - assert (forall P k l, + 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). @@ -727,7 +727,7 @@ Section MakeRingPol. 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';rsimpl. rewrite H;Esimpl. rewrite IHP';Esimpl. rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl. rewrite H;Esimpl. rewrite IHP. @@ -736,8 +736,8 @@ Section MakeRingPol. rewrite IHP2;simpl;rsimpl. rewrite IHP2;simpl. rewrite jump_Pdouble_minus_one;rsimpl. - rewrite IHP';rsimpl. - destruct P;simpl. + 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. @@ -752,7 +752,7 @@ Section MakeRingPol. rewrite H;rewrite Pplus_comm. rewrite pow_pos_Pplus;rsimpl. add_push (P3 @ (tail l));rrefl. - assert (forall P k l, + 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. @@ -775,8 +775,8 @@ Section MakeRingPol. Qed. (* Proof for the symmetriv version *) - Lemma PmulI_ok : - forall P', + Lemma PmulI_ok : + forall P', (forall (P : Pol) (l : list R), (Pmul P P') @ l == P @ l * P' @ l) -> forall (P : Pol) (p : positive) (l : list R), (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l). @@ -801,8 +801,8 @@ Section MakeRingPol. Qed. (* - Lemma PmulI_ok : - forall P', + 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). @@ -846,7 +846,7 @@ Section MakeRingPol. 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 + | 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;simpl;rewrite IHP'2;Esimpl. @@ -886,8 +886,8 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@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, + + 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 auto; rsimpl. @@ -902,7 +902,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. rewrite Pplus_comm;rewrite pow_pos_Pplus;rsimpl. Qed. - Lemma Mcphi_ok: forall P c l, + Lemma Mcphi_ok: forall P c l, let (Q,R) := CFactor P c in P@l == Q@l + (phi c) * (R@l). Proof. @@ -924,7 +924,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. rewrite (ARadd_comm ARth); rsimpl. Qed. - Lemma Mphi_ok: forall P (cM: C * Mon) l, + Lemma Mphi_ok: forall P (cM: C * Mon) l, let (c,M) := cM in let (Q,R) := MFactor P c M in P@l == Q@l + (phi c) * (Mphi l M) * (R@l). @@ -951,7 +951,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. rewrite (Pcompare_Eq_eq _ _ He). generalize (Hrec (c, M) (jump j l)); case (MFactor P c M); simpl; intros P2 Q2 H; repeat rewrite mkPinj_ok; auto. - generalize (Hrec (c, (zmon (j -i) M)) (jump i l)); + generalize (Hrec (c, (zmon (j -i) M)) (jump i l)); case (MFactor P c (zmon (j -i) M)); simpl. intros P2 Q2 H; repeat rewrite mkPinj_ok; auto. rewrite <- (Pplus_minus _ _ (ZC2 _ _ He)). @@ -973,14 +973,14 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. apply (Radd_ext Reqe); rsimpl. rewrite (ARadd_comm ARth); rsimpl. intros j M1. - generalize (Hrec1 (c,zmon j M1) l); + generalize (Hrec1 (c,zmon j M1) l); case (MFactor P2 c (zmon j M1)). intros R1 S1 H1. - generalize (Hrec2 (c, zmon_pred j M1) (List.tail l)); + generalize (Hrec2 (c, zmon_pred j M1) (List.tail l)); case (MFactor Q2 c (zmon_pred j M1)); simpl. intros R2 S2 H2; rewrite H1; rewrite H2. repeat rewrite mkPX_ok; simpl. - rsimpl. + rsimpl. apply radd_ext; rsimpl. rewrite (ARadd_comm ARth); rsimpl. apply radd_ext; rsimpl. @@ -1002,7 +1002,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. repeat (rewrite <-(ARmul_assoc ARth)). apply rmul_ext; rsimpl. rewrite (ARmul_comm ARth); rsimpl. - generalize (Hrec1 (c, vmon (j - i) M1) l); + generalize (Hrec1 (c, vmon (j - i) M1) l); case (MFactor P2 c (vmon (j - i) M1)); simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. rewrite H; rsimpl; repeat rewrite mkPinj_ok; auto. @@ -1020,7 +1020,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. apply rmul_ext; rsimpl. rewrite <- pow_pos_Pplus. rewrite (Pplus_minus _ _ (ZC2 _ _ He)); rsimpl. - generalize (Hrec1 (c, mkZmon 1 M1) l); + generalize (Hrec1 (c, mkZmon 1 M1) l); case (MFactor P2 c (mkZmon 1 M1)); simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. rewrite H; rsimpl. @@ -1064,7 +1064,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. 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. + 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. @@ -1092,18 +1092,18 @@ Proof. injection H2; intros; subst; rsimpl. rewrite Padd_ok. rewrite Pmul_ok; rsimpl. - Qed. + Qed. *) Lemma PNSubst1_ok: forall n P1 M1 P2 l, [fst M1] * Mphi l (snd 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); + 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); + 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. @@ -1112,15 +1112,15 @@ Proof. PNSubst P1 M1 P2 n = Some P3 -> [fst M1] * Mphi l (snd M1) == P2@l -> P1@l == P3@l. Proof. intros n P2 (cc, M1) P3 l P4; unfold PNSubst. - generalize (fun P4 => @POneSubst_ok P2 (cc,M1) P3 P4 l); + generalize (fun P4 => @POneSubst_ok P2 (cc,M1) P3 P4 l); case (POneSubst P2 (cc,M1) P3); [idtac | intros; discriminate]. - intros P5 H1; case n; try (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 (C * Mon * Pol)) (l: list R) {struct LM1} : Prop := - match LM1 with + Fixpoint MPcond (LM1: list (C * Mon * Pol)) (l: list R) {struct LM1} : Prop := + match LM1 with cons (M1,P2) LM2 => ([fst M1] * Mphi l (snd M1) == P2@l) /\ (MPcond LM2 l) | _ => True end. @@ -1189,7 +1189,7 @@ Proof. Strategy expand [PEeval]. (** Correctness proofs *) - + Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l. Proof. destruct p;simpl;intros;Esimpl;trivial. @@ -1198,11 +1198,11 @@ Strategy expand [PEeval]. rewrite nth_Pdouble_minus_one;rrefl. Qed. - Ltac Esimpl3 := + 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). + end;Esimpl2;try rrefl;try apply (ARadd_comm ARth). (* Power using the chinise algorithm *) (*Section POWER. @@ -1213,13 +1213,13 @@ Strategy expand [PEeval]. | 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. @@ -1228,28 +1228,28 @@ Strategy expand [PEeval]. 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) + | 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. @@ -1257,11 +1257,11 @@ Section POWER. 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 by trivial. Esimpl. Qed. - + End POWER. (** Normalization and rewriting *) @@ -1276,86 +1276,86 @@ Section POWER. Fixpoint norm_aux (pe:PExpr) : Pol := match pe with | PEc c => Pc c - | PEX j => mk_X j + | PEX j => mk_X j | PEadd (PEopp pe1) pe2 => Psub (norm_aux pe2) (norm_aux pe1) - | PEadd pe1 (PEopp pe2) => + | 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) + | 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) + | PEX j => subst_l (mk_X j) | PEadd (PEopp pe1) pe2 => Psub (norm_subst pe2) (norm_subst pe1) - | PEadd pe1 (PEopp pe2) => + | 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) + | 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 : + Lemma norm_subst_spec : forall l pe, MPcond lmp l -> - PEeval l pe == (norm_subst pe)@l. + PEeval l pe == (norm_subst pe)@l. Proof. - intros;assert (subst_l_ok:forall P, (subst_l P)@l == P@l). + 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;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; + induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; repeat rewrite Pmul_ok;rrefl. Qed. *) - Lemma norm_aux_spec : + Lemma norm_aux_spec : forall l pe, MPcond lmp l -> - PEeval l pe == (norm_aux pe)@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;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 (intros;rrefl). rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3. - induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; + induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; repeat rewrite Pmul_ok;rrefl. Qed. - Lemma norm_subst_spec : + Lemma norm_subst_spec : forall l pe, MPcond lmp l -> PEeval l pe == (norm_subst pe)@l. Proof. intros;unfold norm_subst. unfold subst_l;rewrite <- PNSubstL_ok;trivial. apply norm_aux_spec. trivial. - Qed. - + Qed. + End NORM_SUBST_REC. - + Fixpoint interp_PElist (l:list R) (lpe:list (PExpr*PExpr)) {struct lpe} : Prop := match lpe with | nil => True - | (me,pe)::lpe => + | (me,pe)::lpe => match lpe with | nil => PEeval l me == PEeval l pe | _ => PEeval l me == PEeval l pe /\ interp_PElist l lpe @@ -1366,9 +1366,9 @@ Section POWER. match P with | Pc c => if (c ?=! cO) then None else Some (c, mon0) | Pinj j P => - match mon_of_pol P with + match mon_of_pol P with | None => None - | Some (c,m) => Some (c, mkZmon j m) + | Some (c,m) => Some (c, mkZmon j m) end | PX P i Q => if Peq Q P0 then @@ -1384,15 +1384,15 @@ Section POWER. | nil => nil | (me,pe)::lpe => match mon_of_pol (norm_subst 0 nil me) with - | None => mk_monpol_list lpe - | Some m => (m,norm_subst 0 nil pe):: mk_monpol_list lpe + | None => mk_monpol_list lpe + | Some m => (m,norm_subst 0 nil pe):: mk_monpol_list lpe end end. Lemma mon_of_pol_ok : forall P m, mon_of_pol P = Some m -> forall l, [fst m] * Mphi l (snd m) == P@l. Proof. - induction P;simpl;intros;Esimpl. + induction P;simpl;intros;Esimpl. assert (H1 := (morph_eq CRmorph) c cO). destruct (c ?=! cO). discriminate. @@ -1418,14 +1418,14 @@ Section POWER. discriminate. intros;discriminate. Qed. - - Lemma interp_PElist_ok : forall l lpe, + + Lemma interp_PElist_ok : forall l lpe, interp_PElist l lpe -> MPcond (mk_monpol_list lpe) l. Proof. induction lpe;simpl. trivial. destruct a;simpl;intros. assert (HH:=mon_of_pol_ok (norm_subst 0 nil p)); - destruct (mon_of_pol (norm_subst 0 nil p)). + destruct (mon_of_pol (norm_subst 0 nil p)). split. rewrite <- norm_subst_spec by exact I. destruct lpe;try destruct H;rewrite <- H; @@ -1440,7 +1440,7 @@ Section POWER. Proof. intros;apply norm_subst_spec. apply interp_PElist_ok;trivial. Qed. - + Lemma ring_correct : forall n l lpe pe1 pe2, interp_PElist l lpe -> (let lmp := mk_monpol_list lpe in @@ -1448,9 +1448,9 @@ Section POWER. PEeval l pe1 == PEeval l pe2. Proof. simpl;intros. - do 2 (rewrite (norm_subst_ok n l lpe);trivial). + do 2 (rewrite (norm_subst_ok n l lpe);trivial). apply Peq_ok;trivial. - Qed. + Qed. @@ -1467,23 +1467,23 @@ Section POWER. Variable mkopp_pow : R -> positive -> R. (* [mkmult_pow r x p] = r * x^p *) Variable mkmult_pow : R -> R -> positive -> R. - + Fixpoint mkmult_rec (r:R) (lm:list (R*positive)) {struct lm}: R := match lm with | nil => r - | cons (x,p) t => mkmult_rec (mkmult_pow r x p) t + | cons (x,p) t => mkmult_rec (mkmult_pow r x p) t end. Definition mkmult1 lm := match lm with | nil => 1 - | cons (x,p) t => mkmult_rec (mkpow x p) t + | cons (x,p) t => mkmult_rec (mkpow x p) t end. Definition mkmultm1 lm := match lm with | nil => ropp rI - | cons (x,p) t => mkmult_rec (mkopp_pow x p) t + | cons (x,p) t => mkmult_rec (mkopp_pow x p) t end. Definition mkmult_c_pos c lm := @@ -1493,11 +1493,11 @@ Section POWER. Definition mkmult_c c lm := match get_sign c with | None => mkmult_c_pos c lm - | Some c' => + | Some c' => if c' ?=! cI then mkmultm1 (rev' lm) else mkmult_rec [c] (rev' lm) end. - + Definition mkadd_mult rP c lm := match get_sign c with | None => rP + mkmult_c_pos c lm @@ -1505,49 +1505,49 @@ Section POWER. end. Definition add_pow_list (r:R) n l := - match n with + match n with | N0 => l | Npos p => (r,p)::l end. - Fixpoint add_mult_dev + Fixpoint add_mult_dev (rP:R) (P:Pol) (fv:list R) (n:N) (lm:list (R*positive)) {struct P} : R := match P with - | Pc c => + | Pc c => let lm := add_pow_list (hd 0 fv) n lm in mkadd_mult rP c lm - | Pinj j Q => + | Pinj j Q => add_mult_dev rP Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm) - | PX P i Q => + | PX P i Q => let rP := add_mult_dev rP P fv (Nplus (Npos i) n) lm in - if Q ?== P0 then rP + if Q ?== P0 then rP else add_mult_dev rP Q (tail fv) N0 (add_pow_list (hd 0 fv) n lm) end. - Fixpoint mult_dev (P:Pol) (fv : list R) (n:N) + Fixpoint mult_dev (P:Pol) (fv : list R) (n:N) (lm:list (R*positive)) {struct P} : R := - (* P@l * (hd 0 l)^n * lm *) + (* P@l * (hd 0 l)^n * lm *) match P with | Pc c => mkmult_c c (add_pow_list (hd 0 fv) n lm) | Pinj j Q => mult_dev Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm) - | PX P i Q => + | PX P i Q => let rP := mult_dev P fv (Nplus (Npos i) n) lm in - if Q ?== P0 then rP - else + if Q ?== P0 then rP + else let lmq := add_pow_list (hd 0 fv) n lm in add_mult_dev rP Q (tail fv) N0 lmq - end. + end. Definition Pphi_avoid fv P := mult_dev P fv N0 nil. - + Fixpoint r_list_pow (l:list (R*positive)) : R := match l with | nil => rI - | cons (r,p) l => pow_pos rmul r p * r_list_pow l + | cons (r,p) l => pow_pos rmul r p * r_list_pow l end. Hypothesis mkpow_spec : forall r p, mkpow r p == pow_pos rmul r p. - Hypothesis mkopp_pow_spec : forall r p, mkopp_pow r p == - (pow_pos rmul r p). + Hypothesis mkopp_pow_spec : forall r p, mkopp_pow r p == - (pow_pos rmul r p). Hypothesis mkmult_pow_spec : forall r x p, mkmult_pow r x p == r * pow_pos rmul x p. Lemma mkmult_rec_ok : forall lm r, mkmult_rec r lm == r * r_list_pow lm. @@ -1571,7 +1571,7 @@ Section POWER. Lemma r_list_pow_rev : forall l, r_list_pow (rev' l) == r_list_pow l. Proof. - assert + assert (forall l lr : list (R * positive), r_list_pow (rev_append l lr) == r_list_pow lr * r_list_pow l). induction l;intros;simpl;Esimpl. destruct a;rewrite IHl;Esimpl. @@ -1583,7 +1583,7 @@ Section POWER. Proof. intros;unfold mkmult_c_pos;simpl. assert (H := (morph_eq CRmorph) c cI). - rewrite <- r_list_pow_rev; destruct (c ?=! cI). + rewrite <- r_list_pow_rev; destruct (c ?=! cI). rewrite H;trivial;Esimpl. apply mkmult1_ok. apply mkmult_rec_ok. Qed. @@ -1610,16 +1610,16 @@ Qed. rewrite mkmult_c_pos_ok;Esimpl. Qed. - Lemma add_pow_list_ok : + Lemma add_pow_list_ok : forall r n l, r_list_pow (add_pow_list r n l) == pow_N rI rmul r n * r_list_pow l. Proof. destruct n;simpl;intros;Esimpl. Qed. - Lemma add_mult_dev_ok : forall P rP fv n lm, + Lemma add_mult_dev_ok : forall P rP fv n lm, add_mult_dev rP P fv n lm == rP + P@fv*pow_N rI rmul (hd 0 fv) n * r_list_pow lm. Proof. - induction P;simpl;intros. + induction P;simpl;intros. rewrite mkadd_mult_ok. rewrite add_pow_list_ok; Esimpl. rewrite IHP. simpl. rewrite add_pow_list_ok; Esimpl. change (match P3 with @@ -1639,7 +1639,7 @@ Qed. rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl. Qed. - Lemma mult_dev_ok : forall P fv n lm, + Lemma mult_dev_ok : forall P fv n lm, mult_dev P fv n lm == P@fv * pow_N rI rmul (hd 0 fv) n * r_list_pow lm. Proof. induction P;simpl;intros;Esimpl. @@ -1669,14 +1669,14 @@ Qed. End EVALUATION. - Definition Pphi_pow := - let mkpow x p := + Definition Pphi_pow := + let mkpow x p := match p with xH => x | _ => rpow x (Cp_phi (Npos p)) end in let mkopp_pow x p := ropp (mkpow x p) in let mkmult_pow r x p := rmul r (mkpow x p) in Pphi_avoid mkpow mkopp_pow mkmult_pow. - Lemma local_mkpow_ok : + Lemma local_mkpow_ok : forall (r : R) (p : positive), match p with | xI _ => rpow r (Cp_phi (Npos p)) @@ -1684,13 +1684,13 @@ Qed. | 1 => r end == pow_pos rmul r p. Proof. intros r p;destruct p;try rewrite pow_th.(rpow_pow_N);reflexivity. Qed. - + Lemma Pphi_pow_ok : forall P fv, Pphi_pow fv P == P@fv. Proof. unfold Pphi_pow;intros;apply Pphi_avoid_ok;intros;try rewrite local_mkpow_ok;rrefl. Qed. - Lemma ring_rw_pow_correct : forall n lH l, + Lemma ring_rw_pow_correct : forall n lH l, interp_PElist l lH -> forall lmp, mk_monpol_list lH = lmp -> forall pe npe, norm_subst n lmp pe = npe -> @@ -1701,22 +1701,22 @@ Qed. apply norm_subst_ok. trivial. Qed. - Fixpoint mkmult_pow (r x:R) (p: positive) {struct p} : R := + Fixpoint mkmult_pow (r x:R) (p: positive) {struct p} : R := match p with - | xH => r*x + | xH => r*x | xO p => mkmult_pow (mkmult_pow r x p) x p | xI p => mkmult_pow (mkmult_pow (r*x) x p) x p end. - + Definition mkpow x p := - match p with + match p with | xH => x | xO p => mkmult_pow x x (Pdouble_minus_one p) | xI p => mkmult_pow x x (xO p) end. - + Definition mkopp_pow x p := - match p with + match p with | xH => -x | xO p => mkmult_pow (-x) x (Pdouble_minus_one p) | xI p => mkmult_pow (-x) x (xO p) @@ -1726,31 +1726,31 @@ Qed. Lemma mkmult_pow_ok : forall p r x, mkmult_pow r x p == r*pow_pos rmul x p. Proof. - induction p;intros;simpl;Esimpl. + induction p;intros;simpl;Esimpl. repeat rewrite IHp;Esimpl. repeat rewrite IHp;Esimpl. Qed. - + Lemma mkpow_ok : forall p x, mkpow x p == pow_pos rmul x p. Proof. destruct p;simpl;intros;Esimpl. repeat rewrite mkmult_pow_ok;Esimpl. rewrite mkmult_pow_ok;Esimpl. - pattern x at 1;replace x with (pow_pos rmul x 1). - rewrite <- pow_pos_Pplus. + pattern x at 1;replace x with (pow_pos rmul x 1). + rewrite <- pow_pos_Pplus. rewrite <- Pplus_one_succ_l. rewrite Psucc_o_double_minus_one_eq_xO. simpl;Esimpl. trivial. Qed. - + Lemma mkopp_pow_ok : forall p x, mkopp_pow x p == - pow_pos rmul x p. Proof. destruct p;simpl;intros;Esimpl. repeat rewrite mkmult_pow_ok;Esimpl. rewrite mkmult_pow_ok;Esimpl. - pattern x at 1;replace x with (pow_pos rmul x 1). - rewrite <- pow_pos_Pplus. + pattern x at 1;replace x with (pow_pos rmul x 1). + rewrite <- pow_pos_Pplus. rewrite <- Pplus_one_succ_l. rewrite Psucc_o_double_minus_one_eq_xO. simpl;Esimpl. @@ -1765,7 +1765,7 @@ Qed. intros;apply mkmult_pow_ok. Qed. - Lemma ring_rw_correct : forall n lH l, + Lemma ring_rw_correct : forall n lH l, interp_PElist l lH -> forall lmp, mk_monpol_list lH = lmp -> forall pe npe, norm_subst n lmp pe = npe -> |