diff options
Diffstat (limited to 'plugins/setoid_ring/Ring_polynom.v')
| -rw-r--r-- | plugins/setoid_ring/Ring_polynom.v | 166 |
1 files changed, 86 insertions, 80 deletions
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index 21d3099c..2d2756b1 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -1,17 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) + Set Implicit Arguments. -Require Import Setoid Morphisms BinList BinPos BinNat BinInt. +Require Import Setoid Morphisms. +Require Import BinList BinPos BinNat BinInt. Require Export Ring_theory. - Local Open Scope positive_scope. Import RingSyntax. +(* Set Universe Polymorphism. *) Section MakeRingPol. @@ -372,17 +374,6 @@ Section MakeRingPol. Infix "**" := Pmul. - 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 **) (** A monomial is X1^k1...Xi^ki. Its representation @@ -511,6 +502,29 @@ Section MakeRingPol. Reserved Notation "P @ l " (at level 10, no associativity). Notation "P @ l " := (Pphi l P). + Definition Pequiv (P Q : Pol) := forall l, P@l == Q@l. + Infix "===" := Pequiv (at level 70, no associativity). + + Instance Pequiv_eq : Equivalence Pequiv. + Proof. + unfold Pequiv; split; red; intros; [reflexivity|now symmetry|now etransitivity]. + Qed. + + Instance Pphi_ext : Proper (eq ==> Pequiv ==> req) Pphi. + Proof. + now intros l l' <- P Q H. + Qed. + + Instance Pinj_ext : Proper (eq ==> Pequiv ==> Pequiv) Pinj. + Proof. + intros i j <- P P' HP l. simpl. now rewrite HP. + Qed. + + Instance PX_ext : Proper (Pequiv ==> eq ==> Pequiv ==> Pequiv) PX. + Proof. + intros P P' HP p p' <- Q Q' HQ l. simpl. now rewrite HP, HQ. + Qed. + (** Evaluation of a monomial towards R *) Fixpoint Mphi(l:list R) (M: Mon) : R := @@ -532,8 +546,9 @@ Section MakeRingPol. Lemma jump_add' i j (l:list R) : jump (i + j) l = jump j (jump i l). Proof. rewrite Pos.add_comm. apply jump_add. Qed. - Lemma Peq_ok P P' : (P ?== P') = true -> forall l, P@l == P'@ l. + Lemma Peq_ok P P' : (P ?== P') = true -> P === P'. Proof. + unfold Pequiv. 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 ]. @@ -545,8 +560,7 @@ Section MakeRingPol. now rewrite IHP1, IHP2. Qed. - Lemma Peq_spec P P' : - BoolSpec (forall l, P@l == P'@l) True (P ?== P'). + Lemma Peq_spec P P' : BoolSpec (P === P') True (P ?== P'). Proof. generalize (Peq_ok P P'). destruct (P ?== P'); auto. Qed. @@ -567,6 +581,11 @@ Section MakeRingPol. now rewrite jump_add'. Qed. + Instance mkPinj_ext : Proper (eq ==> Pequiv ==> Pequiv) mkPinj. + Proof. + intros i j <- P Q H l. now rewrite !mkPinj_ok. + Qed. + Lemma pow_pos_add x i j : x^(j + i) == x^i * x^j. Proof. rewrite Pos.add_comm. @@ -590,6 +609,11 @@ Section MakeRingPol. rewrite H, Pphi0, Pos.add_comm, pow_pos_add; rsimpl. Qed. + Instance mkPX_ext : Proper (Pequiv ==> eq ==> Pequiv ==> Pequiv) mkPX. + Proof. + intros P P' HP i i' <- Q Q' HQ l. now rewrite !mkPX_ok, HP, HQ. + Qed. + Hint Rewrite Pphi0 Pphi1 @@ -656,7 +680,7 @@ Section MakeRingPol. - add_permut. - destruct p; simpl; rewrite ?jump_pred_double; add_permut. - - destr_pos_sub; intros ->;Esimpl. + - 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. @@ -689,47 +713,23 @@ Section MakeRingPol. rewrite IHP'2, pow_pos_add; rsimpl. add_permut. Qed. - 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. + Lemma Psub_opp P' P : P -- P' === P ++ (--P'). Proof. - intros IHP'. - revert k l. induction P;simpl;intros. - - rewrite Popp_ok;rsimpl; add_permut. - - destruct p; simpl; - rewrite Popp_ok;rsimpl; - rewrite ?jump_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. + revert P; induction P'; simpl; intros. + - intro l; Esimpl. + - revert p; induction P; simpl; intros; try reflexivity. + + destr_pos_sub; intros ->; now apply mkPinj_ext. + + destruct p0; now apply PX_ext. + - destruct P; simpl; try reflexivity. + + destruct p0; now apply PX_ext. + + destr_pos_sub; intros ->; apply mkPX_ext; auto. + revert p1. induction P2; simpl; intros; try reflexivity. + destr_pos_sub; intros ->; now apply mkPX_ext. Qed. Lemma Psub_ok P' P l : (P -- P')@l == P@l - P'@l. Proof. - 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 jump_add'. - * rewrite IHP. now rewrite jump_add'. - + destruct p0;simpl. - * rewrite IHP2;simpl. rsimpl. - * rewrite IHP2;simpl. rewrite jump_pred_double. rsimpl. - * rewrite IHP'. rsimpl. - - destruct P;simpl. - + Esimpl; add_permut. - + destruct p0;simpl;Esimpl; rewrite IHP'2; simpl. - * rsimpl. add_permut. - * rewrite jump_pred_double. rsimpl. add_permut. - * rsimpl. 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. + rewrite Psub_opp, Padd_ok, Popp_ok. rsimpl. Qed. Lemma PmulI_ok P' : @@ -764,15 +764,6 @@ Section MakeRingPol. add_permut; f_equiv; mul_permut. Qed. - Lemma Psquare_ok P l : (Psquare P)@l == P@l * P@l. - Proof. - 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 mkZmon_ok M j l : (mkZmon j M) @@ l == (zmon j M) @@ l. Proof. @@ -807,9 +798,9 @@ Section MakeRingPol. P@l == Q@l + [c] * R@l. Proof. revert l. - induction P as [c0 | j P IH | P1 IH1 i P2 IH2]; intros l; Esimpl. - - assert (H := div_th.(div_eucl_th) c0 c). - destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. + induction P as [c0 | j P IH | P1 IH1 i P2 IH2]; intros l; Esimpl. + - assert (H := div_th.(div_eucl_th) c0 c). + destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. - destr_factor. Esimpl. - destr_factor. Esimpl. add_permut. Qed. @@ -818,11 +809,12 @@ Section MakeRingPol. let (c,M) := cM in let (Q,R) := MFactor P c M in P@l == Q@l + [c] * M@@l * R@l. - Proof. + Proof. destruct cM as (c,M). revert M l. - induction P; destruct M; intros l; simpl; auto; + induction P; destruct M; intros l; simpl; auto; try (case ceqb_spec; intro He); - try (case Pos.compare_spec; intros He); rewrite ?He; + try (case Pos.compare_spec; intros He); + rewrite ?He; destr_factor; simpl; Esimpl. - assert (H := div_th.(div_eucl_th) c0 c). destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. @@ -880,9 +872,9 @@ Section MakeRingPol. Lemma PSubstL1_ok n LM1 P1 l : MPcond LM1 l -> P1@l == (PSubstL1 P1 LM1 n)@l. Proof. - revert P1; induction LM1 as [|(M2,P2) LM2 IH]; simpl; intros. - - reflexivity. - - rewrite <- IH by intuition. now apply PNSubst1_ok. + revert P1; induction LM1 as [|(M2,P2) LM2 IH]; simpl; intros. + - reflexivity. + - rewrite <- IH by intuition; now apply PNSubst1_ok. Qed. Lemma PSubstL_ok n LM1 P1 P2 l : @@ -907,6 +899,8 @@ Section MakeRingPol. (** Definition of polynomial expressions *) Inductive PExpr : Type := + | PEO : PExpr + | PEI : PExpr | PEc : C -> PExpr | PEX : positive -> PExpr | PEadd : PExpr -> PExpr -> PExpr @@ -915,6 +909,7 @@ Section MakeRingPol. | PEopp : PExpr -> PExpr | PEpow : PExpr -> N -> PExpr. + (** evaluation of polynomial expressions towards R *) Definition mk_X j := mkPinj_pred j mkX. @@ -922,6 +917,8 @@ Section MakeRingPol. Fixpoint PEeval (l:list R) (pe:PExpr) {struct pe} : R := match pe with + | PEO => rO + | PEI => rI | PEc c => phi c | PEX j => nth 0 j l | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2) @@ -985,11 +982,13 @@ Section POWER. Variable n : nat. Variable lmp:list (C*Mon*Pol). Let subst_l P := PNSubstL P lmp n n. - Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2). + Let Pmul_subst P1 P2 := subst_l (P1 ** P2). Let Ppow_subst := Ppow_N subst_l. Fixpoint norm_aux (pe:PExpr) : Pol := match pe with + | PEO => Pc cO + | PEI => Pc cI | PEc c => Pc c | PEX j => mk_X j | PEadd (PEopp pe1) pe2 => (norm_aux pe2) -- (norm_aux pe1) @@ -1021,7 +1020,7 @@ Section POWER. end. Proof. simpl (norm_aux (PEadd _ _)). - destruct pe1; [ | | | | | reflexivity | ]; + destruct pe1; [ | | | | | | | reflexivity | ]; destruct pe2; simpl get_PEopp; reflexivity. Qed. @@ -1034,22 +1033,26 @@ Section POWER. now destruct pe. Qed. + Arguments norm_aux !pe : simpl nomatch. + Lemma norm_aux_spec l pe : PEeval l pe == (norm_aux pe)@l. Proof. intros. - induction pe. + induction pe; cbn. + - now rewrite (morph0 CRmorph). + - now rewrite (morph1 CRmorph). - reflexivity. - apply mkX_ok. - - simpl PEeval. rewrite IHpe1, IHpe2. + - 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 IHpe1, IHpe2. Esimpl. + - rewrite IHpe1, IHpe2. now rewrite Pmul_ok. + - rewrite IHpe. Esimpl. + - 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. @@ -1483,3 +1486,6 @@ Qed. Qed. End MakeRingPol. + +Arguments PEO [C]. +Arguments PEI [C]. |