diff options
Diffstat (limited to 'contrib/setoid_ring')
| -rw-r--r-- | contrib/setoid_ring/BinList.v | 101 | ||||
| -rw-r--r-- | contrib/setoid_ring/Pol.v | 1195 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_tac.v | 754 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_th.v | 462 | ||||
| -rw-r--r-- | contrib/setoid_ring/ZRing_th.v | 802 | ||||
| -rw-r--r-- | contrib/setoid_ring/newring.ml4 | 525 |
6 files changed, 3839 insertions, 0 deletions
diff --git a/contrib/setoid_ring/BinList.v b/contrib/setoid_ring/BinList.v new file mode 100644 index 00000000..0def087f --- /dev/null +++ b/contrib/setoid_ring/BinList.v @@ -0,0 +1,101 @@ +Set Implicit Arguments. +Require Import BinPos. +Open Scope positive_scope. + + +Section LIST. + + Variable A:Type. + Variable default:A. + + Inductive list : Type := + | nil : list + | cons : A -> list -> list. + + Infix "::" := cons (at level 60, right associativity). + + Definition hd l := match l with hd :: _ => hd | _ => default end. + + Definition tl l := match l with _ :: tl => tl | _ => nil end. + + Fixpoint jump (p:positive) (l:list) {struct p} : list := + match p with + | xH => tl l + | xO p => jump p (jump p l) + | xI p => jump p (jump p (tl l)) + end. + + Fixpoint nth (p:positive) (l:list) {struct p} : A:= + match p with + | xH => hd l + | xO p => nth p (jump p l) + | xI p => nth p (jump p (tl l)) + end. + + Fixpoint rev_append (rev l : list) {struct l} : list := + match l with + | nil => rev + | (cons h t) => rev_append (cons h rev) t + end. + + Definition rev l : list := rev_append nil l. + + Lemma jump_tl : forall j l, tl (jump j l) = jump j (tl l). + Proof. + induction j;simpl;intros. + repeat rewrite IHj;trivial. + repeat rewrite IHj;trivial. + trivial. + Qed. + + Lemma jump_Psucc : forall j l, + (jump (Psucc j) l) = (jump 1 (jump j l)). + Proof. + induction j;simpl;intros. + repeat rewrite IHj;simpl;repeat rewrite jump_tl;trivial. + repeat rewrite jump_tl;trivial. + trivial. + Qed. + + Lemma jump_Pplus : forall i j l, + (jump (i + j) l) = (jump i (jump j l)). + Proof. + induction i;intros. + rewrite xI_succ_xO;rewrite Pplus_one_succ_r. + rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. + repeat rewrite IHi. + rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite jump_Psucc;trivial. + rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. + repeat rewrite IHi;trivial. + rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite jump_Psucc;trivial. + Qed. + + Lemma jump_Pdouble_minus_one : forall i l, + (jump (Pdouble_minus_one i) (tl l)) = (jump i (jump i l)). + Proof. + induction i;intros;simpl. + repeat rewrite jump_tl;trivial. + rewrite IHi. do 2 rewrite <- jump_tl;rewrite IHi;trivial. + trivial. + Qed. + + + Lemma nth_jump : forall p l, nth p (tl l) = hd (jump p l). + Proof. + induction p;simpl;intros. + rewrite <-jump_tl;rewrite IHp;trivial. + rewrite <-jump_tl;rewrite IHp;trivial. + trivial. + Qed. + + Lemma nth_Pdouble_minus_one : + forall p l, nth (Pdouble_minus_one p) (tl l) = nth p (jump p l). + Proof. + induction p;simpl;intros. + repeat rewrite jump_tl;trivial. + rewrite jump_Pdouble_minus_one. + repeat rewrite <- jump_tl;rewrite IHp;trivial. + trivial. + Qed. + +End LIST. diff --git a/contrib/setoid_ring/Pol.v b/contrib/setoid_ring/Pol.v new file mode 100644 index 00000000..2bf2574f --- /dev/null +++ b/contrib/setoid_ring/Pol.v @@ -0,0 +1,1195 @@ +Set Implicit Arguments. +Require Import Setoid. +Require Export BinList. +Require Import BinPos. +Require Import BinInt. +Require Export Ring_th. + +Section MakeRingPol. + + (* 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 *) + 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. + + + (* 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 0 1 radd rmul rsub ropp req 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 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. + + (** 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. + + 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 => + Padd (mkPX (Pmul_aux P P') i P0) (PmulI Pmul_aux Q xH P') + end. + Notation "P ** P'" := (Pmul P P'). + + (** Evaluation of a polynomial towards R *) + + Fixpoint pow (x:R) (i:positive) {struct i}: R := + match i with + | xH => x + | xO i => let p := pow x i in p * p + | xI i => let p := pow x i in x * p * p + end. + + Fixpoint Pphi(l:list 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 x i in + (Pphi l P) * xi + (Pphi (tl 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 pow_Psucc : forall x j, pow x (Psucc j) == x * pow x j. + Proof. + induction j;simpl;rsimpl. + rewrite IHj;rsimpl;mul_push x;rrefl. + Qed. + + Lemma pow_Pplus : forall x i j, pow x (i + j) == pow x i * pow x j. + Proof. + intro x;induction i;intros. + rewrite xI_succ_xO;rewrite Pplus_one_succ_r. + rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. + repeat rewrite IHi. + rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_Psucc. + simpl;rsimpl. + rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. + repeat rewrite IHi;rsimpl. + rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_Psucc; + simpl;rsimpl. + 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 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 <-jump_Pplus;rewrite Pplus_comm;rrefl. + Qed. + + Lemma mkPX_ok : forall l P i Q, + (mkPX P i Q)@l == P@l*(pow (hd 0 l) i) + Q@(tl 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_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_sym ARth). + assert (H := ZPminus_spec p p0);destruct (ZPminus p p0). + rewrite H;Esimpl. rewrite IHP';rrefl. + rewrite H;Esimpl. rewrite IHP';Esimpl. + rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl. + rewrite H;Esimpl. rewrite IHP. + rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl. + destruct p0;simpl. + rewrite IHP2;simpl;rsimpl. + rewrite IHP2;simpl. + rewrite jump_Pdouble_minus_one;rsimpl. + rewrite IHP';rsimpl. + destruct P;simpl. + Esimpl2;add_push [c];rrefl. + destruct p0;simpl;Esimpl2. + rewrite IHP'2;simpl. + rsimpl;add_push (P'1@l * (pow (hd 0 l) p));rrefl. + rewrite IHP'2;simpl. + rewrite jump_Pdouble_minus_one;rsimpl;add_push (P'1@l * (pow (hd 0 l) p));rrefl. + rewrite IHP'2;rsimpl. add_push (P @ (tl l));rrefl. + assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2. + rewrite IHP'1;rewrite IHP'2;rsimpl. + add_push (P3 @ (tl l));rewrite H;rrefl. + rewrite IHP'1;rewrite IHP'2;simpl;Esimpl. + rewrite H;rewrite Pplus_comm. + rewrite pow_Pplus;rsimpl. + add_push (P3 @ (tl l));rrefl. + assert (forall P k l, + (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow (hd 0 l) k). + induction P;simpl;intros;try apply (ARadd_sym ARth). + destruct p2;simpl;try apply (ARadd_sym ARth). + rewrite jump_Pdouble_minus_one;apply (ARadd_sym ARth). + assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2. + rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tl l0));rrefl. + rewrite IHP'1;simpl;Esimpl. + rewrite H1;rewrite Pplus_comm. + rewrite pow_Pplus;simpl;Esimpl. + add_push (P5 @ (tl l0));rrefl. + rewrite IHP1;rewrite H1;rewrite Pplus_comm. + rewrite pow_Pplus;simpl;rsimpl. + add_push (P5 @ (tl l0));rrefl. + rewrite H0;rsimpl. + add_push (P3 @ (tl l)). + rewrite H;rewrite Pplus_comm. + rewrite IHP'2;rewrite pow_Pplus;rsimpl. + add_push (P3 @ (tl 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_sym ARth). + assert (H := ZPminus_spec p p0);destruct (ZPminus p p0). + rewrite H;Esimpl. rewrite IHP';rsimpl. + rewrite H;Esimpl. rewrite IHP';Esimpl. + rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl. + rewrite H;Esimpl. rewrite IHP. + rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl. + destruct p0;simpl. + rewrite IHP2;simpl;rsimpl. + rewrite IHP2;simpl. + rewrite jump_Pdouble_minus_one;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 (hd 0 l) p));trivial. + add_push (P @ (jump p0 (jump p0 (tl l))));rrefl. + rewrite IHP'2;simpl;rewrite jump_Pdouble_minus_one;rsimpl. + add_push (- (P'1 @ l * pow (hd 0 l) p));rrefl. + rewrite IHP'2;rsimpl;add_push (P @ (tl l));rrefl. + assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2. + rewrite IHP'1; rewrite IHP'2;rsimpl. + add_push (P3 @ (tl l));rewrite H;rrefl. + rewrite IHP'1; rewrite IHP'2;rsimpl;simpl;Esimpl. + rewrite H;rewrite Pplus_comm. + rewrite pow_Pplus;rsimpl. + add_push (P3 @ (tl l));rrefl. + assert (forall P k l, + (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow (hd 0 l) k). + induction P;simpl;intros. + rewrite Popp_ok;rsimpl;apply (ARadd_sym ARth);trivial. + destruct p2;simpl;rewrite Popp_ok;rsimpl. + apply (ARadd_sym ARth);trivial. + rewrite jump_Pdouble_minus_one;apply (ARadd_sym ARth);trivial. + apply (ARadd_sym ARth);trivial. + assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2;rsimpl. + rewrite IHP'1;rsimpl;add_push (P5 @ (tl l0));rewrite H1;rrefl. + rewrite IHP'1;rewrite H1;rewrite Pplus_comm. + rewrite pow_Pplus;simpl;Esimpl. + add_push (P5 @ (tl l0));rrefl. + rewrite IHP1;rewrite H1;rewrite Pplus_comm. + rewrite pow_Pplus;simpl;rsimpl. + add_push (P5 @ (tl l0));rrefl. + rewrite H0;rsimpl. + rewrite IHP'2;rsimpl;add_push (P3 @ (tl l)). + rewrite H;rewrite Pplus_comm. + rewrite pow_Pplus;rsimpl. + 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_sym 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 (hd 0 l) p);rrefl. + rewrite IHP1;rewrite IHP2;simpl;rsimpl. + mul_push (pow (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl. + rewrite IHP1;simpl;rsimpl. + mul_push (pow (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. + + Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. + Proof. + destruct P;simpl;intros. + Esimpl2;apply (ARmul_sym ARth). + rewrite (PmulI_ok P (Pmul_aux_ok P)). + apply (ARmul_sym ARth). + rewrite Padd_ok; Esimpl2. + rewrite (PmulI_ok P3 (Pmul_aux_ok P3));trivial. + rewrite Pmul_aux_ok;mul_push (P' @ l). + rewrite (ARmul_sym ARth (P' @ l));rrefl. + 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. + + (** normalisation towards polynomials *) + + Definition X := (PX P1 xH P0). + + Definition mkX j := + match j with + | xH => X + | xO j => Pinj (Pdouble_minus_one j) X + | xI j => Pinj (xO j) X + end. + + Fixpoint norm (pe:PExpr) : Pol := + match pe with + | PEc c => Pc c + | PEX j => mkX j + | PEadd pe1 (PEopp pe2) => Psub (norm pe1) (norm pe2) + | PEadd (PEopp pe1) pe2 => Psub (norm pe2) (norm pe1) + | PEadd pe1 pe2 => Padd (norm pe1) (norm pe2) + | PEsub pe1 pe2 => Psub (norm pe1) (norm pe2) + | PEmul pe1 pe2 => Pmul (norm pe1) (norm pe2) + | PEopp pe1 => Popp (norm pe1) + end. + + (** evaluation of polynomial expressions towards R *) + + Fixpoint PEeval (l:list R) (pe:PExpr) {struct pe} : R := + match pe with + | PEc c => phi c + | PEX j => nth 0 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) + end. + + (** Correctness proofs *) + + + Lemma mkX_ok : forall p l, nth 0 p l == (mkX p) @ l. + Proof. + destruct p;simpl;intros;Esimpl;trivial. + rewrite <-jump_tl;rewrite nth_jump;rrefl. + rewrite <- nth_jump. + rewrite nth_Pdouble_minus_one;rrefl. + Qed. + + Lemma norm_PEopp : forall l pe, (norm (PEopp pe))@l == -(norm pe)@l. + Proof. + intros;simpl;apply Popp_ok. + 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) + | |- context [(norm (PEopp ?pe))@?l] => rewrite (norm_PEopp l pe) + end;Esimpl2;try rrefl;try apply (ARadd_sym ARth). + + Lemma norm_ok : forall l pe, PEeval l pe == (norm pe)@l. + Proof. + induction pe;simpl;Esimpl3. + apply mkX_ok. + rewrite IHpe1;rewrite IHpe2; destruct pe1;destruct pe2;Esimpl3. + rewrite IHpe1;rewrite IHpe2;rrefl. + rewrite Pmul_ok;rewrite IHpe1;rewrite IHpe2;rrefl. + rewrite IHpe;rrefl. + Qed. + + Lemma ring_correct : forall l pe1 pe2, + ((norm pe1) ?== (norm pe2)) = true -> (PEeval l pe1) == (PEeval l pe2). + Proof. + intros l pe1 pe2 H. + repeat rewrite norm_ok. + apply (Peq_ok (norm pe1) (norm pe2) H l). + Qed. + +(** Evaluation function avoiding parentheses *) + Fixpoint mkmult (r:R) (lm:list R) {struct lm}: R := + match lm with + | nil => r + | cons h t => mkmult (r*h) t + end. + + Definition mkadd_mult rP lm := + match lm with + | nil => rP + 1 + | cons h t => rP + mkmult h t + end. + + Fixpoint powl (i:positive) (x:R) (l:list R) {struct i}: list R := + match i with + | xH => cons x l + | xO i => powl i x (powl i x l) + | xI i => powl i x (powl i x (cons x l)) + end. + + Fixpoint add_mult_dev (rP:R) (P:Pol) (fv lm:list R) {struct P} : R := + (* rP + P@l * lm *) + match P with + | Pc c => if c ?=! cI then mkadd_mult rP (rev lm) + else mkadd_mult rP (cons [c] (rev lm)) + | Pinj j Q => add_mult_dev rP Q (jump j fv) lm + | PX P i Q => + let rP := add_mult_dev rP P fv (powl i (hd 0 fv) lm) in + if Q ?== P0 then rP else add_mult_dev rP Q (tl fv) lm + end. + + Definition mkmult1 lm := + match lm with + | nil => rI + | cons h t => mkmult h t + end. + + Fixpoint mult_dev (P:Pol) (fv lm : list R) {struct P} : R := + (* P@l * lm *) + match P with + | Pc c => if c ?=! cI then mkmult1 (rev lm) else mkmult [c] (rev lm) + | Pinj j Q => mult_dev Q (jump j fv) lm + | PX P i Q => + let rP := mult_dev P fv (powl i (hd 0 fv) lm) in + if Q ?== P0 then rP else add_mult_dev rP Q (tl fv) lm + end. + + Definition Pphi_dev fv P := mult_dev P fv (nil R). + + Add Morphism mkmult : mkmult_ext. + intros r r0 eqr l;generalize l r r0 eqr;clear l r r0 eqr; + induction l;simpl;intros. + trivial. apply IHl; rewrite eqr;rrefl. + Qed. + + Lemma mul_mkmult : forall lm r1 r2, r1 * mkmult r2 lm == mkmult (r1*r2) lm. + Proof. + induction lm;simpl;intros;try rrefl. + rewrite IHlm. + setoid_replace (r1 * (r2 * a)) with (r1 * r2 * a);Esimpl. + Qed. + + Lemma mkmult1_mkmult : forall lm r, r * mkmult1 lm == mkmult r lm. + Proof. + destruct lm;simpl;intros. Esimpl. + apply mul_mkmult. + Qed. + + Lemma mkmult1_mkmult_1 : forall lm, mkmult1 lm == mkmult 1 lm. + Proof. + intros;rewrite <- mkmult1_mkmult;Esimpl. + Qed. + + Lemma mkmult_rev_append : forall lm l r, + mkmult r (rev_append l lm) == mkmult (mkmult r l) lm. + Proof. + induction lm; simpl in |- *; intros. + rrefl. + rewrite IHlm; simpl in |- *. + repeat rewrite <- (ARmul_sym ARth a); rewrite <- mul_mkmult. + rrefl. + Qed. + + Lemma powl_mkmult_rev : forall p r x lm, + mkmult r (rev (powl p x lm)) == mkmult (pow x p * r) (rev lm). + Proof. + induction p;simpl;intros. + repeat rewrite IHp. + unfold rev;simpl. + repeat rewrite mkmult_rev_append. + simpl. + setoid_replace (pow x p * (pow x p * r) * x) + with (x * pow x p * pow x p * r);Esimpl. + mul_push x;rrefl. + repeat rewrite IHp. + setoid_replace (pow x p * (pow x p * r) ) + with (pow x p * pow x p * r);Esimpl. + unfold rev;simpl. repeat rewrite mkmult_rev_append;simpl. + rewrite (ARmul_sym ARth);rrefl. + Qed. + + Lemma Pphi_add_mult_dev : forall P rP fv lm, + rP + P@fv * mkmult1 (rev lm) == add_mult_dev rP P fv lm. + Proof. + induction P;simpl;intros. + assert (H := (morph_eq CRmorph) c cI). + destruct (c ?=! cI). + rewrite (H (refl_equal true));rewrite (morph1 CRmorph);Esimpl. + destruct (rev lm);Esimpl;rrefl. + rewrite mkmult1_mkmult;rrefl. + apply IHP. + replace (match P3 with + | Pc c => c ?=! cO + | Pinj _ _ => false + | PX _ _ _ => false + end) with (Peq P3 P0);trivial. + assert (H := Peq_ok P3 P0). + destruct (P3 ?== P0). + rewrite (H (refl_equal true));simpl;Esimpl. + rewrite <- IHP1. + repeat rewrite mkmult1_mkmult_1. + rewrite powl_mkmult_rev. + rewrite <- mul_mkmult;Esimpl. + rewrite <- IHP2. + rewrite <- IHP1. + repeat rewrite mkmult1_mkmult_1. + rewrite powl_mkmult_rev. + rewrite <- mul_mkmult;Esimpl. + Qed. + + Lemma Pphi_mult_dev : forall P fv lm, + P@fv * mkmult1 (rev lm) == mult_dev P fv lm. + Proof. + induction P;simpl;intros. + assert (H := (morph_eq CRmorph) c cI). + destruct (c ?=! cI). + rewrite (H (refl_equal true));rewrite (morph1 CRmorph);Esimpl. + apply mkmult1_mkmult. + apply IHP. + replace (match P3 with + | Pc c => c ?=! cO + | Pinj _ _ => false + | PX _ _ _ => false + end) with (Peq P3 P0);trivial. + assert (H := Peq_ok P3 P0). + destruct (P3 ?== P0). + rewrite (H (refl_equal true));simpl;Esimpl. + rewrite <- IHP1. + repeat rewrite mkmult1_mkmult_1. + rewrite powl_mkmult_rev. + rewrite <- mul_mkmult;Esimpl. + rewrite <- Pphi_add_mult_dev. + rewrite <- IHP1. + repeat rewrite mkmult1_mkmult_1. + rewrite powl_mkmult_rev. + rewrite <- mul_mkmult;Esimpl. + Qed. + + Lemma Pphi_Pphi_dev : forall P l, P@l == Pphi_dev l P. + Proof. + unfold Pphi_dev;intros. + rewrite <- Pphi_mult_dev;simpl;Esimpl. + Qed. + + Lemma Pphi_dev_ok : forall l pe, PEeval l pe == Pphi_dev l (norm pe). + Proof. + intros l pe;rewrite <- Pphi_Pphi_dev;apply norm_ok. + Qed. + + Lemma Pphi_dev_ok' : + forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe. + Proof. + intros l pe npe npe_eq; subst npe; apply Pphi_dev_ok. + Qed. + +(* The same but building a PExpr *) +(* + Fixpoint Pmkmult (r:PExpr) (lm:list PExpr) {struct lm}: PExpr := + match lm with + | nil => r + | cons h t => Pmkmult (PEmul r h) t + end. + + Definition Pmkadd_mult rP lm := + match lm with + | nil => PEadd rP (PEc cI) + | cons h t => PEadd rP (Pmkmult h t) + end. + + Fixpoint Ppowl (i:positive) (x:PExpr) (l:list PExpr) {struct i}: list PExpr := + match i with + | xH => cons x l + | xO i => Ppowl i x (Ppowl i x l) + | xI i => Ppowl i x (Ppowl i x (cons x l)) + end. + + Fixpoint Padd_mult_dev + (rP:PExpr) (P:Pol) (fv lm:list PExpr) {struct P} : PExpr := + (* rP + P@l * lm *) + match P with + | Pc c => if c ?=! cI then Pmkadd_mult rP (rev lm) + else Pmkadd_mult rP (cons [PEc c] (rev lm)) + | Pinj j Q => Padd_mult_dev rP Q (jump j fv) lm + | PX P i Q => + let rP := Padd_mult_dev rP P fv (Ppowl i (hd P0 fv) lm) in + if Q ?== P0 then rP else Padd_mult_dev rP Q (tl fv) lm + end. + + Definition Pmkmult1 lm := + match lm with + | nil => PEc cI + | cons h t => Pmkmult h t + end. + + Fixpoint Pmult_dev (P:Pol) (fv lm : list PExpr) {struct P} : PExpr := + (* P@l * lm *) + match P with + | Pc c => if c ?=! cI then Pmkmult1 (rev lm) else Pmkmult [PEc c] (rev lm) + | Pinj j Q => Pmult_dev Q (jump j fv) lm + | PX P i Q => + let rP := Pmult_dev P fv (Ppowl i (hd (PEc r0) fv) lm) in + if Q ?== P0 then rP else Padd_mult_dev rP Q (tl fv) lm + end. + + Definition Pphi_dev2 fv P := Pmult_dev P fv (nil PExpr). + +... +*) + (************************************************) + (* avec des parentheses mais un peu plus efficace *) + + + (************************************************** + + Fixpoint pow_mult (i:positive) (x r:R){struct i}:R := + match i with + | xH => r * x + | xO i => pow_mult i x (pow_mult i x r) + | xI i => pow_mult i x (pow_mult i x (r * x)) + end. + + Definition pow_dev i x := + match i with + | xH => x + | xO i => pow_mult (Pdouble_minus_one i) x x + | xI i => pow_mult (xO i) x x + end. + + Lemma pow_mult_pow : forall i x r, pow_mult i x r == pow x i * r. + Proof. + induction i;simpl;intros. + rewrite (IHi x (pow_mult i x (r * x)));rewrite (IHi x (r*x));rsimpl. + mul_push x;rrefl. + rewrite (IHi x (pow_mult i x r));rewrite (IHi x r);rsimpl. + apply ARth.(ARmul_sym). + Qed. + + Lemma pow_dev_pow : forall p x, pow_dev p x == pow x p. + Proof. + destruct p;simpl;intros. + rewrite (pow_mult_pow p x (pow_mult p x x)). + rewrite (pow_mult_pow p x x);rsimpl;mul_push x;rrefl. + rewrite (pow_mult_pow (Pdouble_minus_one p) x x). + rewrite (ARth.(ARmul_sym) (pow x (Pdouble_minus_one p)) x). + rewrite <- (pow_Psucc x (Pdouble_minus_one p)). + rewrite Psucc_o_double_minus_one_eq_xO;simpl; rrefl. + rrefl. + Qed. + + Fixpoint Pphi_dev (fv:list R) (P:Pol) {struct P} : R := + match P with + | Pc c => [c] + | Pinj j Q => Pphi_dev (jump j fv) Q + | PX P i Q => + let rP := mult_dev P fv (pow_dev i (hd 0 fv)) in + add_dev rP Q (tl fv) + end + + with add_dev (ra:R) (P:Pol) (fv:list R) {struct P} : R := + match P with + | Pc c => if c ?=! cO then ra else ra + [c] + | Pinj j Q => add_dev ra Q (jump j fv) + | PX P i Q => + let ra := add_mult_dev ra P fv (pow_dev i (hd 0 fv)) in + add_dev ra Q (tl fv) + end + + with mult_dev (P:Pol) (fv:list R) (rm:R) {struct P} : R := + match P with + | Pc c => if c ?=! cI then rm else [c]*rm + | Pinj j Q => mult_dev Q (jump j fv) rm + | PX P i Q => + let ra := mult_dev P fv (pow_mult i (hd 0 fv) rm) in + add_mult_dev ra Q (tl fv) rm + end + + with add_mult_dev (ra:R) (P:Pol) (fv:list R) (rm:R) {struct P} : R := + match P with + | Pc c => if c ?=! cO then ra else ra + [c]*rm + | Pinj j Q => add_mult_dev ra Q (jump j fv) rm + | PX P i Q => + let rmP := pow_mult i (hd 0 fv) rm in + let raP := add_mult_dev ra P fv rmP in + add_mult_dev raP Q (tl fv) rm + end. + + Lemma Pphi_add_mult_dev : forall P ra fv rm, + add_mult_dev ra P fv rm == ra + P@fv * rm. + Proof. + induction P;simpl;intros. + assert (H := CRmorph.(morph_eq) c cO). + destruct (c ?=! cO). + rewrite (H (refl_equal true));rewrite CRmorph.(morph0);Esimpl. + rrefl. + apply IHP. + rewrite (IHP2 (add_mult_dev ra P2 fv (pow_mult p (hd 0 fv) rm)) (tl fv) rm). + rewrite (IHP1 ra fv (pow_mult p (hd 0 fv) rm)). + rewrite (pow_mult_pow p (hd 0 fv) rm);rsimpl. + Qed. + + Lemma Pphi_add_dev : forall P ra fv, add_dev ra P fv == ra + P@fv. + Proof. + induction P;simpl;intros. + assert (H := CRmorph.(morph_eq) c cO). + destruct (c ?=! cO). + rewrite (H (refl_equal true));rewrite CRmorph.(morph0);Esimpl. + rrefl. + apply IHP. + rewrite (IHP2 (add_mult_dev ra P2 fv (pow_dev p (hd 0 fv))) (tl fv)). + rewrite (Pphi_add_mult_dev P2 ra fv (pow_dev p (hd 0 fv))). + rewrite (pow_dev_pow p (hd 0 fv));rsimpl. + Qed. + + Lemma Pphi_mult_dev : forall P fv rm, mult_dev P fv rm == P@fv * rm. + Proof. + induction P;simpl;intros. + assert (H := CRmorph.(morph_eq) c cI). + destruct (c ?=! cI). + rewrite (H (refl_equal true));rewrite CRmorph.(morph1);Esimpl. + rrefl. + apply IHP. + rewrite (Pphi_add_mult_dev P3 + (mult_dev P2 fv (pow_mult p (hd 0 fv) rm)) (tl fv) rm). + rewrite (IHP1 fv (pow_mult p (hd 0 fv) rm)). + rewrite (pow_mult_pow p (hd 0 fv) rm);rsimpl. + Qed. + + Lemma Pphi_Pphi_dev : forall P fv, P@fv == Pphi_dev fv P. + Proof. + induction P;simpl;intros. + rrefl. trivial. + rewrite (Pphi_add_dev P3 (mult_dev P2 fv (pow_dev p (hd 0 fv))) (tl fv)). + rewrite (Pphi_mult_dev P2 fv (pow_dev p (hd 0 fv))). + rewrite (pow_dev_pow p (hd 0 fv));rsimpl. + Qed. + + Lemma Pphi_dev_ok : forall l pe, PEeval l pe == Pphi_dev l (norm pe). + Proof. + intros l pe;rewrite <- (Pphi_Pphi_dev (norm pe) l);apply norm_ok. + Qed. + + Ltac Trev l := + let rec rev_append rev l := + match l with + | (nil _) => constr:(rev) + | (cons ?h ?t) => let rev := constr:(cons h rev) in rev_append rev t + end in + rev_append (nil R) l. + + Ltac TPphi_dev add mul := + let tl l := match l with (cons ?h ?t) => constr:(t) end in + let rec jump j l := + match j with + | xH => tl l + | (xO ?j) => let l := jump j l in jump j l + | (xI ?j) => let t := tl l in let l := jump j l in jump j l + end in + let rec pow_mult i x r := + match i with + | xH => constr:(mul r x) + | (xO ?i) => let r := pow_mult i x r in pow_mult i x r + | (xI ?i) => + let r := constr:(mul r x) in + let r := pow_mult i x r in + pow_mult i x r + end in + let pow_dev i x := + match i with + | xH => x + | (xO ?i) => + let i := eval compute in (Pdouble_minus_one i) in pow_mult i x x + | (xI ?i) => pow_mult (xO i) x x + end in + let rec add_mult_dev ra P fv rm := + match P with + | (Pc ?c) => + match eval compute in (c ?=! cO) with + | true => constr:ra + | _ => let rc := eval compute in [c] in constr:(add ra (mul rc rm)) + end + | (Pinj ?j ?Q) => + let fv := jump j fv in add_mult_dev ra Q fv rm + | (PX ?P ?i ?Q) => + match fv with + | (cons ?hd ?tl) => + let rmP := pow_mult i hd rm in + let raP := add_mult_dev ra P fv rmP in + add_mult_dev raP Q tl rm + end + end in + let rec mult_dev P fv rm := + match P with + | (Pc ?c) => + match eval compute in (c ?=! cI) with + | true => constr:rm + | false => let rc := eval compute in [c] in constr:(mul rc rm) + end + | (Pinj ?j ?Q) => let fv := jump j fv in mult_dev Q fv rm + | (PX ?P ?i ?Q) => + match fv with + | (cons ?hd ?tl) => + let rmP := pow_mult i hd rm in + let ra := mult_dev P fv rmP in + add_mult_dev ra Q tl rm + end + end in + let rec add_dev ra P fv := + match P with + | (Pc ?c) => + match eval compute in (c ?=! cO) with + | true => ra + | false => let rc := eval compute in [c] in constr:(add ra rc) + end + | (Pinj ?j ?Q) => let fv := jump j fv in add_dev ra Q fv + | (PX ?P ?i ?Q) => + match fv with + | (cons ?hd ?tl) => + let rmP := pow_dev i hd in + let ra := add_mult_dev ra P fv rmP in + add_dev ra Q tl + end + end in + let rec Pphi_dev fv P := + match P with + | (Pc ?c) => eval compute in [c] + | (Pinj ?j ?Q) => let fv := jump j fv in Pphi_dev fv Q + | (PX ?P ?i ?Q) => + match fv with + | (cons ?hd ?tl) => + let rm := pow_dev i hd in + let rP := mult_dev P fv rm in + add_dev rP Q tl + end + end in + Pphi_dev. + + **************************************************************) + +End MakeRingPol. diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v new file mode 100644 index 00000000..6c3f87a5 --- /dev/null +++ b/contrib/setoid_ring/Ring_tac.v @@ -0,0 +1,754 @@ +Set Implicit Arguments. +Require Import Setoid. +Require Import BinList. +Require Import BinPos. +Require Import Pol. +Declare ML Module "newring". + +(* Some Tactics *) + +Ltac compute_assertion id t := + let t' := eval compute in t in + (assert (id : t = t'); [exact_no_check (refl_equal t')|idtac]). + +Ltac compute_assertion' id id' t := + let t' := eval compute in t in + (pose (id' := t'); + assert (id : t = id'); + [exact_no_check (refl_equal id')|idtac]). + +Ltac compute_replace' id t := + let t' := eval compute in t in + (replace t with t' in id; [idtac|exact_no_check (refl_equal t')]). + +Ltac bin_list_fold_right fcons fnil l := + match l with + | (cons ?x ?tl) => fcons x ltac:(bin_list_fold_right fcons fnil tl) + | (nil _) => fnil + end. + +Ltac bin_list_fold_left fcons fnil l := + match l with + | (cons ?x ?tl) => bin_list_fold_left fcons ltac:(fcons x fnil) tl + | (nil _) => fnil + end. + +Ltac bin_list_iter f l := + match l with + | (cons ?x ?tl) => f x; bin_list_iter f tl + | (nil _) => idtac + end. + +(** A tactic that reverses a list *) +Ltac Trev R l := + let rec rev_append rev l := + match l with + | (nil _) => constr:(rev) + | (cons ?h ?t) => let rev := constr:(cons h rev) in rev_append rev t + end in + rev_append (nil R) l. + +(* to avoid conflicts with Coq booleans*) +Definition NotConstant := false. + +Ltac IN a l := + match l with + | (cons a ?l) => true + | (cons _ ?l) => IN a l + | (nil _) => false + end. + +Ltac AddFv a l := + match (IN a l) with + | true => l + | _ => constr:(cons a l) + end. + +Ltac Find_at a l := + match l with + | (nil _) => fail 1 "ring anomaly" + | (cons a _) => constr:1%positive + | (cons _ ?l) => let p := Find_at a l in eval compute in (Psucc p) + end. + +Ltac FV Cst add mul sub opp t fv := + let rec TFV t fv := + match Cst t with + | NotConstant => + match t with + | (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) + | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) + | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) + | (opp ?t1) => TFV t1 fv + | _ => AddFv t fv + end + | _ => fv + end + in TFV t fv. + + (* syntaxification *) + Ltac mkPolexpr C Cst radd rmul rsub ropp t fv := + let rec mkP t := + match Cst t with + | NotConstant => + match t with + | (radd ?t1 ?t2) => + let e1 := mkP t1 in + let e2 := mkP t2 in constr:(PEadd e1 e2) + | (rmul ?t1 ?t2) => + let e1 := mkP t1 in + let e2 := mkP t2 in constr:(PEmul e1 e2) + | (rsub ?t1 ?t2) => + let e1 := mkP t1 in + let e2 := mkP t2 in constr:(PEsub e1 e2) + | (ropp ?t1) => + let e1 := mkP t1 in constr:(PEopp e1) + | _ => + let p := Find_at t fv in constr:(PEX C p) + end + | ?c => constr:(PEc c) + end + in mkP t. + +(* ring tactics *) +Ltac Make_ring_rewrite_step lemma pe:= + let npe := fresh "npe" in + let H := fresh "eq_npe" in + let Heq := fresh "ring_thm" in + let npe_spec := + match type of (lemma pe) with + forall (npe:_), ?npe_spec = npe -> _ => npe_spec + | _ => fail 1 "cannot find norm expression" + end in + (compute_assertion' H npe npe_spec; + assert (Heq:=lemma _ _ H); clear H; + protect_fv in Heq; + (rewrite Heq; clear Heq npe) || clear npe). + + +Ltac Make_ring_rw_list Cst_tac lemma req rl := + match type of lemma with + forall (l:list ?R) (pe:PExpr ?C) (npe:Pol ?C), + _ = npe -> + req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe) _ => + let mkFV := FV Cst_tac add mul sub opp in + let mkPol := mkPolexpr C Cst_tac add mul sub opp in + (* build the atom list *) + let rfv := bin_list_fold_left mkFV (nil R) rl in + let fv := Trev R rfv in + (* rewrite *) + bin_list_iter + ltac:(fun r => + let pe := mkPol r fv in + Make_ring_rewrite_step (lemma fv) pe) + rl + | _ => fail 1 "bad lemma" + end. + +Ltac Make_ring_rw Cst_tac lemma req r := + Make_ring_rw_list Cst_tac lemma req (cons r (nil _)). + + (* Building the generic tactic *) + + Ltac Make_ring_tac Cst_tac lemma1 lemma2 req := + match type of lemma2 with + forall (l:list ?R) (pe:PExpr ?C) (npe:Pol ?C), + _ = npe -> + req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe) _ => + match goal with + | |- req ?r1 ?r2 => + let mkFV := FV Cst_tac add mul sub opp in + let mkPol := mkPolexpr C Cst_tac add mul sub opp in + let rfv := mkFV (add r1 r2) (nil R) in + let fv := Trev R rfv in + let pe1 := mkPol r1 fv in + let pe2 := mkPol r2 fv in + ((apply (lemma1 fv pe1 pe2); + vm_compute; + exact (refl_equal true)) || + (Make_ring_rewrite_step (lemma2 fv) pe1; + Make_ring_rewrite_step (lemma2 fv) pe2)) + | _ => fail 1 "goal is not an equality from a declared ring" + end + end. + + +(* coefs belong to the same type as the target ring (concrete ring) *) +Definition ring_id_correct + R rO rI radd rmul rsub ropp req rSet req_th ARth reqb reqb_ok := + @ring_correct R rO rI radd rmul rsub ropp req rSet req_th ARth + R rO rI radd rmul rsub ropp reqb + (@IDphi R) + (@IDmorph R rO rI radd rmul rsub ropp req rSet reqb reqb_ok). + +Definition ring_rw_id_correct + R rO rI radd rmul rsub ropp req rSet req_th ARth reqb reqb_ok := + @Pphi_dev_ok R rO rI radd rmul rsub ropp req rSet req_th ARth + R rO rI radd rmul rsub ropp reqb + (@IDphi R) + (@IDmorph R rO rI radd rmul rsub ropp req rSet reqb reqb_ok). + +Definition ring_rw_id_correct' + R rO rI radd rmul rsub ropp req rSet req_th ARth reqb reqb_ok := + @Pphi_dev_ok' R rO rI radd rmul rsub ropp req rSet req_th ARth + R rO rI radd rmul rsub ropp reqb + (@IDphi R) + (@IDmorph R rO rI radd rmul rsub ropp req rSet reqb reqb_ok). + +Definition ring_id_eq_correct R rO rI radd rmul rsub ropp ARth reqb reqb_ok := + @ring_id_correct R rO rI radd rmul rsub ropp (@eq R) + (Eqsth R) (Eq_ext _ _ _) ARth reqb reqb_ok. + +Definition ring_rw_id_eq_correct + R rO rI radd rmul rsub ropp ARth reqb reqb_ok := + @ring_rw_id_correct R rO rI radd rmul rsub ropp (@eq R) + (Eqsth R) (Eq_ext _ _ _) ARth reqb reqb_ok. + +Definition ring_rw_id_eq_correct' + R rO rI radd rmul rsub ropp ARth reqb reqb_ok := + @ring_rw_id_correct' R rO rI radd rmul rsub ropp (@eq R) + (Eqsth R) (Eq_ext _ _ _) ARth reqb reqb_ok. + +(* +Require Import ZArith. +Require Import Setoid. +Require Import Ring_tac. +Import BinList. +Import Ring_th. +Open Scope Z_scope. + +Add New Ring Zr : (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) + Computational Zeqb_ok + Constant Zcst. + +Goal forall a b, (a+b*2)*(a+b*2)=1. +intros. + setoid ring ((a + b * 2) * (a + b * 2)). + + Make_ring_rw_list Zcst + (ring_rw_id_correct' (Eqsth Z) (Eq_ext _ _ _) + (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok) + (eq (A:=Z)) + (cons ((a+b)*(a+b)) (nil _)). + + +Goal forall a b, (a+b)*(a+b)=1. +intros. +Ltac zringl := + Make_ring_rw3_list ltac:(inv_gen_phiZ 0 1 Zplus Zmult Zopp) + (ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _) + (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok) + (eq (A:=Z)) +(BinList.cons ((a+b)*(a+b)) (BinList.nil _)). + +Open Scope Z_scope. + +let Cst_tac := inv_gen_phiZ 0 1 Zplus Zmult Zopp in +let lemma := + constr:(ring_rw_id_correct' (Eqsth Z) (Eq_ext _ _ _) + (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok) in +let req := constr:(eq (A:=Z)) in +let rl := constr:(cons ((a+b)*(a+b)) (nil _)) in +Make_ring_rw_list Cst_tac lemma req rl. + +let fv := constr:(cons a (cons b (nil _))) in +let pe := + constr:(PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))) in +Make_ring_rewrite_step (lemma fv) pe. + + + + +OK + +Lemma L0 : + forall (l : list Z) (pe : PExpr Z) pe', + pe' = norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe -> + PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) l pe = + Pphi_dev 0 1 Zplus Zmult 0 1 Zeq_bool (IDphi (R:=Z)) l pe'. +intros; subst pe'. +apply + (ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _) + (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok). +Qed. +Lemma L0' : + forall (l : list Z) (pe : PExpr Z) pe', + norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe = pe' -> + PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) l pe = + Pphi_dev 0 1 Zplus Zmult 0 1 Zeq_bool (IDphi (R:=Z)) l pe'. +intros; subst pe'. +apply + (ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _) + (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok). +Qed. + +pose (pe:=PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))). +compute_assertion ipattern:H (norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe). +let fv := constr:(cons a (cons b (nil _))) in +assert (Heq := L0 fv _ (sym_equal H)); clear H. + protect_fv' in Heq. + rewrite Heq; clear Heq; clear pe. + + +MIEUX (mais taille preuve = taille de pe + taille de nf(pe)... ): + + +Lemma L : + forall (l : list Z) (pe : PExpr Z) pe' (x y :Z), + pe' = norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe -> + x = PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) l pe -> + y = Pphi_dev 0 1 Zplus Zmult 0 1 Zeq_bool (IDphi (R:=Z)) l pe' -> + x=y. +intros; subst x y pe'. +apply + (ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _) + (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok). +Qed. +Lemma L' : + forall (l : list Z) (pe : PExpr Z) pe' (x y :Z), + Peq Zeq_bool pe' (norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe) = true -> + x = PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) l pe -> + y = Pphi_dev 0 1 Zplus Zmult 0 1 Zeq_bool (IDphi (R:=Z)) l pe' -> + forall (P:Z->Type), P y -> P x. +intros. + rewrite L with (2:=H0) (3:=H1); trivial. +apply (Peq_ok (Eqsth Z) (Eq_ext _ _ _) + (IDmorph 0 1 Zplus Zminus Zmult Zopp (Eqsth Z) Zeq_bool Zeqb_ok) ). + + (IDmorph (Eqsth Z) (Eq_ext _ _ _) Zeqb_ok). + + + (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth)). +Qed. + +eapply L' + with (x:=(a+b)*(a+b)) + (pe:=PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))) + (l:=cons a (cons b (nil Z)));[compute;reflexivity|reflexivity|idtac|idtac];norm_evars;[protect_fv';reflexivity|idtac];norm_evars. + + + + + +set (x:=a). +set (x0:=b). +set (fv:=cons x (cons x0 (nil Z))). +let fv:=constr:(cons a (cons b (nil Z))) in +let lemma := constr : (ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _) + (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok) in +let pe := + constr : (PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))) in +assert (Heq := lemma fv pe). +set (npe:=norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool + (PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2)))). +fold npe in Heq. +move npe after fv. +let fv' := eval red in fv in +compute in npe. +subst npe. +let fv' := eval red in fv in +compute_without_globals_of (fv',Zplus,0,1,Zmult,Zopp,Zminus) in Heq. +rewrite Heq. +clear Heq fv; subst x x0. + + +simpl in Heq. +unfold Pphi_dev in Heq. +unfold mult_dev in Heq. +unfold P0, Peq in *. +unfold Zeq_bool at 3, Zcompare, Pcompare in Heq. +unfold fv, hd, tl in Heq. +unfold powl, rev, rev_append in Heq. +unfold mkmult1 in Heq. +unfold mkmult in Heq. +unfold add_mult_dev in |- *. +unfold add_mult_dev at 2 in Heq. +unfold P0, Peq at 1 in Heq. +unfold Zeq_bool at 2 3 4 5 6, Zcompare, Pcompare in Heq. +unfold hd, powl, rev, rev_append in Heq. +unfold mkadd_mult in Heq. +unfold mkmult in Heq. +unfold add_mult_dev in Heq. +unfold P0, Peq in Heq. +unfold Zeq_bool, Zcompare, Pcompare in Heq. +unfold hd,powl, rev,rev_append in Heq. +unfold mkadd_mult in Heq. +unfold mkmult in Heq. +unfold IDphi in Heq. + + fv := cons x (cons x0 (nil Z)) + PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2)) + Heq : PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) fv + (PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))) = + Pphi_dev 0 1 Zplus Zmult 0 1 Zeq_bool (IDphi (R:=Z)) fv + (norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool + (PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2)))) + + + +let Cst_tac := inv_gen_phiZ 0 1 Zplus Zmult Zopp in +let lemma := + constr:(ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _) + (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok) in +let req := constr:(eq (A:=Z)) in +let rl := constr:(BinList.cons ((a+b)*(a+b)) (BinList.nil _)) in + match type of lemma with + forall (l:list ?R) (pe:PExpr ?C), + req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe) _ => + Constant natcst. + + +Require Import Setoid. +Open Scope nat_scope. + +Require Import Ring_th. +Require Import Arith. + +Add New Ring natr : (SRth_ARth (Eqsth nat) natSRth) + Computational nateq_ok + Constant natcst. + + +Require Import Rbase. +Open Scope R_scope. + + Lemma Rth : ring_theory 0 1 Rplus Rmult Rminus Ropp (@eq R). + Proof. + constructor. exact Rplus_0_l. exact Rplus_comm. + intros;symmetry;apply Rplus_assoc. + exact Rmult_1_l. exact Rmult_comm. + intros;symmetry;apply Rmult_assoc. + exact Rmult_plus_distr_r. trivial. exact Rplus_opp_r. + Qed. + +Add New Ring Rr : Rth Abstract. + +Goal forall a b, (a+b*10)*(a+b*10)=1. +intros. + +Module Zring. + Import Zpol. + Import BinPos. + Import BinInt. + +Ltac is_PCst p := + match p with + | xH => true + | (xO ?p') => is_PCst p' + | (xI ?p') => is_PCst p' + | _ => false + end. + +Ltac ZCst t := + match t with + | Z0 => constr:t + | (Zpos ?p) => + match (is_PCst p) with + | false => NotConstant + | _ => constr:t + end + | (Zneg ?p) => + match (is_PCst p) with + | false => NotConstant + | _ => constr:t + end + | _ => NotConstant + end. + +Ltac zring := + Make_ring_tac ZCst + (Zpol.ring_gen_eq_correct Zth) (Zpol.ring_rw_gen_eq_correct Zth) (@eq Z). + +Ltac zrewrite := + Make_ring_rw3 ZCst (Zpol.ring_rw_gen_eq_correct Zth) (@eq Z). + +Ltac zrewrite_list := + Make_ring_rw3_list ZCst (Zpol.ring_rw_gen_eq_correct Zth) (@eq Z). + +End Zring. +*) + + + +(* +(*** Intanciation for Z*) +Require Import ZArith. +Open Scope Z_scope. + +Module Zring. + Let R := Z. + Let rO := 0. + Let rI := 1. + Let radd := Zplus. + Let rmul := Zmult. + Let rsub := Zminus. + Let ropp := Zopp. + Let Rth := Zth. + Let reqb := Zeq_bool. + Let req_morph := Zeqb_ok. + + (* CE_Entries *) + Let C := R. + Let cO := rO. + Let cI := rI. + Let cadd := radd. + Let cmul := rmul. + Let csub := rsub. + Let copp := ropp. + Let req := (@eq R). + Let ceqb := reqb. + Let phi := @IDphi R. + Let Rsth : Setoid_Theory R req := Eqsth R. + Let Reqe : ring_eq_ext radd rmul ropp req := + (@Eq_ext R radd rmul ropp). + Let ARth : almost_ring_theory rO rI radd rmul rsub ropp req := + (@Rth_ARth R rO rI radd rmul rsub ropp req Rsth Reqe Rth). + Let CRmorph : ring_morph rO rI radd rmul rsub ropp req + cO cI cadd cmul csub copp ceqb phi := + (@IDmorph R rO rI radd rmul rsub ropp req Rsth reqb req_morph). + + Definition Peq := Eval red in (Pol.Peq ceqb). + Definition mkPinj := Eval red in (@Pol.mkPinj C). + Definition mkPX := + Eval red; + change (Pol.Peq ceqb) with Peq; + change (@Pol.mkPinj Z) with mkPinj in + (Pol.mkPX cO ceqb). + + Definition P0 := Eval red in (Pol.P0 cO). + Definition P1 := Eval red in (Pol.P1 cI). + + Definition X := + Eval red; change (Pol.P0 cO) with P0; change (Pol.P1 cI) with P1 in + (Pol.X cO cI). + + Definition mkX := + Eval red; change (Pol.X cO cI) with X in + (mkX cO cI). + + Definition PaddC + Definition PaddI + Definition PaddX + + Definition Padd := + Eval red in + + (Pol.Padd cO cadd ceqb) + + Definition PmulC + Definition PmulI + Definition Pmul_aux + Definition Pmul + + Definition PsubC + Definition PsubI + Definition PsubX + Definition Psub + + + + Definition norm := + Eval red; + change (Pol.Padd cO cadd ceqb) with Padd; + change (Pol.Pmul cO cI cadd cmul ceqb) with Pmul; + change (Pol.Psub cO cadd csub copp ceqb) with Psub; + change (Pol.Popp copp) with Psub; + + in + (Pol.norm cO cI cadd cmul csub copp ceqb). + + + +End Zring. + +Ltac is_PCst p := + match p with + | xH => true + | (xO ?p') => is_PCst p' + | (xI ?p') => is_PCst p' + | _ => false + end. + +Ltac ZCst t := + match t with + | Z0 => constr:t + | (Zpos ?p) => + match (is_PCst p) with + | false => NotConstant + | _ => t + end + | (Zneg ?p) => + match (is_PCst p) with + | false => NotConstant + | _ => t + end + | _ => NotConstant + end. + +Ltac zring := + Zring.Make_ring_tac Zplus Zmult Zminus Zopp (@eq Z) ZCst. + +Ltac zrewrite := + Zring.Make_ring_rw3 Zplus Zmult Zminus Zopp ZCst. +*) + +(* +(* Instanciation for Bool *) +Require Import Bool. + +Module BCE. + Definition R := bool. + Definition rO := false. + Definition rI := true. + Definition radd := xorb. + Definition rmul := andb. + Definition rsub := xorb. + Definition ropp b:bool := b. + Lemma Rth : ring_theory rO rI radd rmul rsub ropp (@eq bool). + Proof. + constructor. + exact false_xorb. + exact xorb_comm. + intros; symmetry in |- *; apply xorb_assoc. + exact andb_true_b. + exact andb_comm. + exact andb_assoc. + destruct x; destruct y; destruct z; reflexivity. + intros; reflexivity. + exact xorb_nilpotent. + Qed. + + Definition reqb := eqb. + Definition req_morph := eqb_prop. +End BCE. + +Module BEntries := CE_Entries BCE. + +Module Bring := MakeRingPol BEntries. + +Ltac BCst t := + match t with + | true => true + | false => false + | _ => NotConstant + end. + +Ltac bring := + Bring.Make_ring_tac xorb andb xorb (fun b:bool => b) (@eq bool) BCst. + +Ltac brewrite := + Zring.Make_ring_rw3 Zplus Zmult Zminus Zopp ZCst. +*) + +(*Module Rring. + +(* Instanciation for R *) +Require Import Rbase. +Open Scope R_scope. + + Lemma Rth : ring_theory 0 1 Rplus Rmult Rminus Ropp (@eq R). + Proof. + constructor. exact Rplus_0_l. exact Rplus_comm. + intros;symmetry;apply Rplus_assoc. + exact Rmult_1_l. exact Rmult_comm. + intros;symmetry;apply Rmult_assoc. + exact Rmult_plus_distr_r. trivial. exact Rplus_opp_r. + Qed. + +Ltac RCst := inv_gen_phiZ 0 1 Rplus Rmul Ropp. + +Ltac rring := + Make_ring_tac RCst + (Zpol.ring_gen_eq_correct Rth) (Zpol.ring_rw_gen_eq_correct Rth) (@eq R). + +Ltac rrewrite := + Make_ring_rw3 RCst (Zpol.ring_rw_gen_eq_correct Rth) (@eq R). + +Ltac rrewrite_list := + Make_ring_rw3_list RCst (Zpol.ring_rw_gen_eq_correct Rth) (@eq R). + +End Rring. +*) +(************************) +(* +(* Instanciation for N *) +Require Import NArith. +Open Scope N_scope. + +Module NCSE. + Definition R := N. + Definition rO := 0. + Definition rI := 1. + Definition radd := Nplus. + Definition rmul := Nmult. + Definition SRth := Nth. + Definition reqb := Neq_bool. + Definition req_morph := Neq_bool_ok. +End NCSE. + +Module NEntries := CSE_Entries NCSE. + +Module Nring := MakeRingPol NEntries. + +Ltac NCst := inv_gen_phiN 0 1 Nplus Nmult. + +Ltac nring := + Nring.Make_ring_tac Nplus Nmult (@SRsub N Nplus) (@SRopp N) (@eq N) NCst. + +Ltac nrewrite := + Nring.Make_ring_rw3 Nplus Nmult (@SRsub N Nplus) (@SRopp N) NCst. + +(* Instanciation for nat *) +Open Scope nat_scope. + +Module NatASE. + Definition R := nat. + Definition rO := 0. + Definition rI := 1. + Definition radd := plus. + Definition rmul := mult. + Lemma SRth : semi_ring_theory O (S O) plus mult (@eq nat). + Proof. + constructor. exact plus_0_l. exact plus_comm. exact plus_assoc. + exact mult_1_l. exact mult_0_l. exact mult_comm. exact mult_assoc. + exact mult_plus_distr_r. + Qed. +End NatASE. + +Module NatEntries := ASE_Entries NatASE. + +Module Natring := MakeRingPol NatEntries. + +Ltac natCst t := + match t with + | O => N0 + | (S ?n) => + match (natCst n) with + | NotConstant => NotConstant + | ?p => constr:(Nsucc p) + end + | _ => NotConstant + end. + +Ltac natring := + Natring.Make_ring_tac plus mult (@SRsub nat plus) (@SRopp nat) (@eq nat) natCst. + +Ltac natrewrite := + Natring.Make_ring_rw3 plus mult (@SRsub nat plus) (@SRopp nat) natCst. + +(* Generic tactic, checks the type of the terms and applies the +suitable instanciation*) + +Ltac newring := + match goal with + | |- (?r1 = ?r2) => + match (type of r1) with + | Z => zring + | R => rring + | bool => bring + | N => nring + | nat => natring + end + end. + +*) diff --git a/contrib/setoid_ring/Ring_th.v b/contrib/setoid_ring/Ring_th.v new file mode 100644 index 00000000..9583dd2d --- /dev/null +++ b/contrib/setoid_ring/Ring_th.v @@ -0,0 +1,462 @@ +Require Import Setoid. + Set Implicit Arguments. + + +Reserved Notation "x ?=! y" (at level 70, no associativity). +Reserved Notation "x +! y " (at level 50, left associativity). +Reserved Notation "x -! y" (at level 50, left associativity). +Reserved Notation "x *! y" (at level 40, left associativity). +Reserved Notation "-! x" (at level 35, right associativity). + +Reserved Notation "[ x ]" (at level 1, no associativity). + +Reserved Notation "x ?== y" (at level 70, no associativity). +Reserved Notation "x ++ y " (at level 50, left associativity). +Reserved Notation "x -- y" (at level 50, left associativity). +Reserved Notation "x ** y" (at level 40, left associativity). +Reserved Notation "-- x" (at level 35, right associativity). + +Reserved Notation "x == y" (at level 70, no associativity). + + + +Section DEFINITIONS. + Variable R : Type. + Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). + Variable req : R -> R -> Prop. + 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). + + (** Semi Ring *) + Record semi_ring_theory : Prop := mk_srt { + SRadd_0_l : forall n, 0 + n == n; + SRadd_sym : forall n m, n + m == m + n ; + SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p; + SRmul_1_l : forall n, 1*n == n; + SRmul_0_l : forall n, 0*n == 0; + SRmul_sym : forall n m, n*m == m*n; + SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p; + SRdistr_l : forall n m p, (n + m)*p == n*p + m*p + }. + + (** Almost Ring *) +(*Almost ring are no ring : Ropp_def is missi**) + Record almost_ring_theory : Prop := mk_art { + ARadd_0_l : forall x, 0 + x == x; + ARadd_sym : forall x y, x + y == y + x; + ARadd_assoc : forall x y z, x + (y + z) == (x + y) + z; + ARmul_1_l : forall x, 1 * x == x; + ARmul_0_l : forall x, 0 * x == 0; + ARmul_sym : forall x y, x * y == y * x; + ARmul_assoc : forall x y z, x * (y * z) == (x * y) * z; + ARdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); + ARopp_mul_l : forall x y, -(x * y) == -x * y; + ARopp_add : forall x y, -(x + y) == -x + -y; + ARsub_def : forall x y, x - y == x + -y + }. + + (** Ring *) + Record ring_theory : Prop := mk_rt { + Radd_0_l : forall x, 0 + x == x; + Radd_sym : forall x y, x + y == y + x; + Radd_assoc : forall x y z, x + (y + z) == (x + y) + z; + Rmul_1_l : forall x, 1 * x == x; + Rmul_sym : forall x y, x * y == y * x; + Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z; + Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); + Rsub_def : forall x y, x - y == x + -y; + Ropp_def : forall x, x + (- x) == 0 + }. + + (** Equality is extensional *) + + Record sring_eq_ext : Prop := mk_seqe { + (* SRing operators are compatible with equality *) + SRadd_ext : + forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 + y1 == x2 + y2; + SRmul_ext : + forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2 + }. + + Record ring_eq_ext : Prop := mk_reqe { + (* Ring operators are compatible with equality *) + Radd_ext : + forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 + y1 == x2 + y2; + Rmul_ext : + forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2; + Ropp_ext : forall x1 x2, x1 == x2 -> -x1 == -x2 + }. + + (** Interpretation morphisms definition*) + Section MORPHISM. + Variable C:Type. + Variable (cO cI : C) (cadd cmul csub : C->C->C) (copp : C->C). + Variable ceqb : C->C->bool. + (* [phi] est un morphisme de [C] dans [R] *) + Variable phi : C -> R. + Notation "x +! y" := (cadd x y). Notation "x -! y " := (csub x y). + Notation "x *! y " := (cmul x y). Notation "-! x" := (copp x). + Notation "x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x). + +(*for semi rings*) + Record semi_morph : Prop := mkRmorph { + Smorph0 : [cO] == 0; + Smorph1 : [cI] == 1; + Smorph_add : forall x y, [x +! y] == [x]+[y]; + Smorph_mul : forall x y, [x *! y] == [x]*[y]; + Smorph_eq : forall x y, x?=!y = true -> [x] == [y] + }. + +(* for rings*) + Record ring_morph : Prop := mkmorph { + morph0 : [cO] == 0; + morph1 : [cI] == 1; + morph_add : forall x y, [x +! y] == [x]+[y]; + morph_sub : forall x y, [x -! y] == [x]-[y]; + morph_mul : forall x y, [x *! y] == [x]*[y]; + morph_opp : forall x, [-!x] == -[x]; + morph_eq : forall x y, x?=!y = true -> [x] == [y] + }. + End MORPHISM. + + (** Identity is a morphism *) + Variable Rsth : Setoid_Theory R req. + Add Setoid R req Rsth as R_setoid1. + Variable reqb : R->R->bool. + Hypothesis morph_req : forall x y, (reqb x y) = true -> x == y. + Definition IDphi (x:R) := x. + Lemma IDmorph : ring_morph rO rI radd rmul rsub ropp reqb IDphi. + Proof. + apply (mkmorph rO rI radd rmul rsub ropp reqb IDphi);intros;unfold IDphi; + try apply (Seq_refl _ _ Rsth);auto. + Qed. + +End DEFINITIONS. + + + +Section ALMOST_RING. + Variable R : Type. + Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). + Variable req : R -> R -> Prop. + 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). + + (** Leibniz equality leads to a setoid theory and is extensional*) + Lemma Eqsth : Setoid_Theory R (@eq R). + Proof. constructor;intros;subst;trivial. Qed. + + Lemma Eq_s_ext : sring_eq_ext radd rmul (@eq R). + Proof. constructor;intros;subst;trivial. Qed. + + Lemma Eq_ext : ring_eq_ext radd rmul ropp (@eq R). + Proof. constructor;intros;subst;trivial. Qed. + + Variable Rsth : Setoid_Theory R req. + Add Setoid R req Rsth as R_setoid2. + Ltac sreflexivity := apply (Seq_refl _ _ Rsth). + + Section SEMI_RING. + Variable SReqe : sring_eq_ext radd rmul req. + Add Morphism radd : radd_ext1. exact (SRadd_ext SReqe). Qed. + Add Morphism rmul : rmul_ext1. exact (SRmul_ext SReqe). Qed. + Variable SRth : semi_ring_theory 0 1 radd rmul req. + + (** Every semi ring can be seen as an almost ring, by taking : + -x = x and x - y = x + y *) + Definition SRopp (x:R) := x. Notation "- x" := (SRopp x). + + Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y). + + Lemma SRopp_ext : forall x y, x == y -> -x == -y. + Proof. intros x y H;exact H. Qed. + + Lemma SReqe_Reqe : ring_eq_ext radd rmul SRopp req. + Proof. + constructor. exact (SRadd_ext SReqe). exact (SRmul_ext SReqe). + exact SRopp_ext. + Qed. + + Lemma SRopp_mul_l : forall x y, -(x * y) == -x * y. + Proof. intros;sreflexivity. Qed. + + Lemma SRopp_add : forall x y, -(x + y) == -x + -y. + Proof. intros;sreflexivity. Qed. + + + Lemma SRsub_def : forall x y, x - y == x + -y. + Proof. intros;sreflexivity. Qed. + + Lemma SRth_ARth : almost_ring_theory 0 1 radd rmul SRsub SRopp req. + Proof (mk_art 0 1 radd rmul SRsub SRopp req + (SRadd_0_l SRth) (SRadd_sym SRth) (SRadd_assoc SRth) + (SRmul_1_l SRth) (SRmul_0_l SRth) + (SRmul_sym SRth) (SRmul_assoc SRth) (SRdistr_l SRth) + SRopp_mul_l SRopp_add SRsub_def). + + (** Identity morphism for semi-ring equipped with their almost-ring structure*) + Variable reqb : R->R->bool. + + Hypothesis morph_req : forall x y, (reqb x y) = true -> x == y. + + Definition SRIDmorph : ring_morph 0 1 radd rmul SRsub SRopp req + 0 1 radd rmul SRsub SRopp reqb (@IDphi R). + Proof. + apply mkmorph;intros;try sreflexivity. unfold IDphi;auto. + Qed. + + (* a semi_morph can be extended to a ring_morph for the almost_ring derived + from a semi_ring, provided the ring is a setoid (we only need + reflexivity) *) + Variable C : Type. + Variable (cO cI : C) (cadd cmul: C->C->C). + Variable (ceqb : C -> C -> bool). + Variable phi : C -> R. + Variable Smorph : semi_morph rO rI radd rmul req cO cI cadd cmul ceqb phi. + + Lemma SRmorph_Rmorph : + ring_morph rO rI radd rmul SRsub SRopp req + cO cI cadd cmul cadd (fun x => x) ceqb phi. + Proof. + case Smorph; intros; constructor; auto. + unfold SRopp in |- *; intros. + setoid_reflexivity. + Qed. + + End SEMI_RING. + + Variable Reqe : ring_eq_ext radd rmul ropp req. + Add Morphism radd : radd_ext2. exact (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext2. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext2. exact (Ropp_ext Reqe). Qed. + + Section RING. + Variable Rth : ring_theory 0 1 radd rmul rsub ropp req. + + (** Rings are almost rings*) + Lemma Rmul_0_l : forall x, 0 * x == 0. + Proof. + intro x; setoid_replace (0*x) with ((0+1)*x + -x). + rewrite (Radd_0_l Rth); rewrite (Rmul_1_l Rth). + rewrite (Ropp_def Rth);sreflexivity. + + rewrite (Rdistr_l Rth);rewrite (Rmul_1_l Rth). + rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth). + rewrite (Radd_sym Rth); rewrite (Radd_0_l Rth);sreflexivity. + Qed. + + Lemma Ropp_mul_l : forall x y, -(x * y) == -x * y. + Proof. + intros x y;rewrite <-(Radd_0_l Rth (- x * y)). + rewrite (Radd_sym Rth). + rewrite <-(Ropp_def Rth (x*y)). + rewrite (Radd_assoc Rth). + rewrite <- (Rdistr_l Rth). + rewrite (Rth.(Radd_sym) (-x));rewrite (Ropp_def Rth). + rewrite Rmul_0_l;rewrite (Radd_0_l Rth);sreflexivity. + Qed. + + Lemma Ropp_add : forall x y, -(x + y) == -x + -y. + Proof. + intros x y;rewrite <- ((Radd_0_l Rth) (-(x+y))). + rewrite <- ((Ropp_def Rth) x). + rewrite <- ((Radd_0_l Rth) (x + - x + - (x + y))). + rewrite <- ((Ropp_def Rth) y). + rewrite ((Radd_sym Rth) x). + rewrite ((Radd_sym Rth) y). + rewrite <- ((Radd_assoc Rth) (-y)). + rewrite <- ((Radd_assoc Rth) (- x)). + rewrite ((Radd_assoc Rth) y). + rewrite ((Radd_sym Rth) y). + rewrite <- ((Radd_assoc Rth) (- x)). + rewrite ((Radd_assoc Rth) y). + rewrite ((Radd_sym Rth) y);rewrite (Ropp_def Rth). + rewrite ((Radd_sym Rth) (-x) 0);rewrite (Radd_0_l Rth). + apply (Radd_sym Rth). + Qed. + + Lemma Ropp_opp : forall x, - -x == x. + Proof. + intros x; rewrite <- (Radd_0_l Rth (- -x)). + rewrite <- (Ropp_def Rth x). + rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth). + rewrite ((Radd_sym Rth) x);apply (Radd_0_l Rth). + Qed. + + Lemma Rth_ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. + Proof + (mk_art 0 1 radd rmul rsub ropp req (Radd_0_l Rth) (Radd_sym Rth) (Radd_assoc Rth) + (Rmul_1_l Rth) Rmul_0_l (Rmul_sym Rth) (Rmul_assoc Rth) (Rdistr_l Rth) + Ropp_mul_l Ropp_add (Rsub_def Rth)). + + (** Every semi morphism between two rings is a morphism*) + Variable C : Type. + Variable (cO cI : C) (cadd cmul csub: C->C->C) (copp : C -> C). + Variable (ceq : C -> C -> Prop) (ceqb : C -> C -> bool). + Variable phi : C -> R. + 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). + Variable Csth : Setoid_Theory C ceq. + Variable Ceqe : ring_eq_ext cadd cmul copp ceq. + Add Setoid C ceq Csth as C_setoid. + Add Morphism cadd : cadd_ext. exact (Radd_ext Ceqe). Qed. + Add Morphism cmul : cmul_ext. exact (Rmul_ext Ceqe). Qed. + Add Morphism copp : copp_ext. exact (Ropp_ext Ceqe). Qed. + Variable Cth : ring_theory cO cI cadd cmul csub copp ceq. + Variable Smorph : semi_morph 0 1 radd rmul req cO cI cadd cmul ceqb phi. + Variable phi_ext : forall x y, ceq x y -> [x] == [y]. + Add Morphism phi : phi_ext1. exact phi_ext. Qed. + Lemma Smorph_opp : forall x, [-!x] == -[x]. + Proof. + intros x;rewrite <- (Rth.(Radd_0_l) [-!x]). + rewrite <- ((Ropp_def Rth) [x]). + rewrite ((Radd_sym Rth) [x]). + rewrite <- (Radd_assoc Rth). + rewrite <- (Smorph_add Smorph). + rewrite (Ropp_def Cth). + rewrite (Smorph0 Smorph). + rewrite (Radd_sym Rth (-[x])). + apply (Radd_0_l Rth);sreflexivity. + Qed. + + Lemma Smorph_sub : forall x y, [x -! y] == [x] - [y]. + Proof. + intros x y; rewrite (Rsub_def Cth);rewrite (Rsub_def Rth). + rewrite (Smorph_add Smorph);rewrite Smorph_opp;sreflexivity. + Qed. + + Lemma Smorph_morph : ring_morph 0 1 radd rmul rsub ropp req + cO cI cadd cmul csub copp ceqb phi. + Proof + (mkmorph 0 1 radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi + (Smorph0 Smorph) (Smorph1 Smorph) + (Smorph_add Smorph) Smorph_sub (Smorph_mul Smorph) Smorph_opp + (Smorph_eq Smorph)). + + End RING. + + (** Usefull lemmas on almost ring *) + Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. + + Lemma ARsub_ext : + forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2. + Proof. + intros. + setoid_replace (x1 - y1) with (x1 + -y1). + setoid_replace (x2 - y2) with (x2 + -y2). + rewrite H;rewrite H0;sreflexivity. + apply (ARsub_def ARth). + apply (ARsub_def ARth). + Qed. + Add Morphism rsub : rsub_ext. exact ARsub_ext. Qed. + + Ltac mrewrite := + repeat first + [ rewrite (ARadd_0_l ARth) + | rewrite <- ((ARadd_sym ARth) 0) + | rewrite (ARmul_1_l ARth) + | rewrite <- ((ARmul_sym ARth) 1) + | rewrite (ARmul_0_l ARth) + | rewrite <- ((ARmul_sym ARth) 0) + | rewrite (ARdistr_l ARth) + | sreflexivity + | match goal with + | |- context [?z * (?x + ?y)] => rewrite ((ARmul_sym ARth) z (x+y)) + end]. + + Lemma ARadd_0_r : forall x, (x + 0) == x. + Proof. intros; mrewrite. Qed. + + Lemma ARmul_1_r : forall x, x * 1 == x. + Proof. intros;mrewrite. Qed. + + Lemma ARmul_0_r : forall x, x * 0 == 0. + Proof. intros;mrewrite. Qed. + + Lemma ARdistr_r : forall x y z, z * (x + y) == z*x + z*y. + Proof. + intros;mrewrite. + repeat rewrite (ARth.(ARmul_sym) z);sreflexivity. + Qed. + + Lemma ARadd_assoc1 : forall x y z, (x + y) + z == (y + z) + x. + Proof. + intros;rewrite <-(ARth.(ARadd_assoc) x). + rewrite (ARth.(ARadd_sym) x);sreflexivity. + Qed. + + Lemma ARadd_assoc2 : forall x y z, (y + x) + z == (y + z) + x. + Proof. + intros; repeat rewrite <- (ARadd_assoc ARth); + rewrite ((ARadd_sym ARth) x); sreflexivity. + Qed. + + Lemma ARmul_assoc1 : forall x y z, (x * y) * z == (y * z) * x. + Proof. + intros;rewrite <-((ARmul_assoc ARth) x). + rewrite ((ARmul_sym ARth) x);sreflexivity. + Qed. + + Lemma ARmul_assoc2 : forall x y z, (y * x) * z == (y * z) * x. + Proof. + intros; repeat rewrite <- (ARmul_assoc ARth); + rewrite ((ARmul_sym ARth) x); sreflexivity. + Qed. + + Lemma ARopp_mul_r : forall x y, - (x * y) == x * -y. + Proof. + intros;rewrite ((ARmul_sym ARth) x y); + rewrite (ARopp_mul_l ARth); apply (ARmul_sym ARth). + Qed. + + Lemma ARopp_zero : -0 == 0. + Proof. + rewrite <- (ARmul_0_r 0); rewrite (ARopp_mul_l ARth). + repeat rewrite ARmul_0_r; sreflexivity. + Qed. + +End ALMOST_RING. + +(** Some simplification tactics*) +Ltac gen_reflexivity Rsth := apply (Seq_refl _ _ Rsth). + +Ltac gen_srewrite O I add mul sub opp eq Rsth Reqe ARth := + repeat first + [ gen_reflexivity Rsth + | progress rewrite (ARopp_zero Rsth Reqe ARth) + | rewrite (ARadd_0_l ARth) + | rewrite (ARadd_0_r Rsth ARth) + | rewrite (ARmul_1_l ARth) + | rewrite (ARmul_1_r Rsth ARth) + | rewrite (ARmul_0_l ARth) + | rewrite (ARmul_0_r Rsth ARth) + | rewrite (ARdistr_l ARth) + | rewrite (ARdistr_r Rsth Reqe ARth) + | rewrite (ARadd_assoc ARth) + | rewrite (ARmul_assoc ARth) + | progress rewrite (ARopp_add ARth) + | progress rewrite (ARsub_def ARth) + | progress rewrite <- (ARopp_mul_l ARth) + | progress rewrite <- (ARopp_mul_r Rsth Reqe ARth) ]. + +Ltac gen_add_push add Rsth Reqe ARth x := + repeat (match goal with + | |- context [add (add ?y x) ?z] => + progress rewrite (ARadd_assoc2 Rsth Reqe ARth x y z) + | |- context [add (add x ?y) ?z] => + progress rewrite (ARadd_assoc1 Rsth ARth x y z) + end). + +Ltac gen_mul_push mul Rsth Reqe ARth x := + repeat (match goal with + | |- context [mul (mul ?y x) ?z] => + progress rewrite (ARmul_assoc2 Rsth Reqe ARth x y z) + | |- context [mul (mul x ?y) ?z] => + progress rewrite (ARmul_assoc1 Rsth ARth x y z) + end). + diff --git a/contrib/setoid_ring/ZRing_th.v b/contrib/setoid_ring/ZRing_th.v new file mode 100644 index 00000000..9060428b --- /dev/null +++ b/contrib/setoid_ring/ZRing_th.v @@ -0,0 +1,802 @@ +Require Import Ring_th. +Require Import Pol. +Require Import Ring_tac. +Require Import ZArith_base. +Require Import BinInt. +Require Import BinNat. +Require Import Setoid. + Set Implicit Arguments. + +(** Z is a ring and a setoid*) + +Lemma Zsth : Setoid_Theory Z (@eq Z). +Proof (Eqsth Z). + +Lemma Zeqe : ring_eq_ext Zplus Zmult Zopp (@eq Z). +Proof (Eq_ext Zplus Zmult Zopp). + +Lemma Zth : ring_theory Z0 (Zpos xH) Zplus Zmult Zminus Zopp (@eq Z). +Proof. + constructor. exact Zplus_0_l. exact Zplus_comm. exact Zplus_assoc. + exact Zmult_1_l. exact Zmult_comm. exact Zmult_assoc. + exact Zmult_plus_distr_l. trivial. exact Zminus_diag. +Qed. + + Lemma Zeqb_ok : forall x y, Zeq_bool x y = true -> x = y. + Proof. + intros x y. + assert (H := Zcompare_Eq_eq x y);unfold Zeq_bool; + destruct (Zcompare x y);intros H1;auto;discriminate H1. + Qed. + + +(** Two generic morphisms from Z to (abrbitrary) rings, *) +(**second one is more convenient for proofs but they are ext. equal*) +Section ZMORPHISM. + Variable R : Type. + Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). + Variable req : R -> R -> Prop. + 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). + Variable Rsth : Setoid_Theory R req. + Add Setoid R req Rsth as R_setoid3. + Ltac rrefl := gen_reflexivity Rsth. + Variable Reqe : ring_eq_ext radd rmul ropp req. + Add Morphism radd : radd_ext3. exact (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext3. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext3. exact (Ropp_ext Reqe). Qed. + + Fixpoint gen_phiPOS1 (p:positive) : R := + match p with + | xH => 1 + | xO p => (1 + 1) * (gen_phiPOS1 p) + | xI p => 1 + ((1 + 1) * (gen_phiPOS1 p)) + end. + + Fixpoint gen_phiPOS (p:positive) : R := + match p with + | xH => 1 + | xO xH => (1 + 1) + | xO p => (1 + 1) * (gen_phiPOS p) + | xI xH => 1 + (1 +1) + | xI p => 1 + ((1 + 1) * (gen_phiPOS p)) + end. + + Definition gen_phiZ1 z := + match z with + | Zpos p => gen_phiPOS1 p + | Z0 => 0 + | Zneg p => -(gen_phiPOS1 p) + end. + + Definition gen_phiZ z := + match z with + | Zpos p => gen_phiPOS p + | Z0 => 0 + | Zneg p => -(gen_phiPOS p) + end. + Notation "[ x ]" := (gen_phiZ x). + + Section ALMOST_RING. + Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. + Add Morphism rsub : rsub_ext3. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth. + Ltac add_push := gen_add_push radd Rsth Reqe ARth. + + Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x. + Proof. + induction x;simpl. + rewrite IHx;destruct x;simpl;norm. + rewrite IHx;destruct x;simpl;norm. + rrefl. + Qed. + + Lemma ARgen_phiPOS_Psucc : forall x, + gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x). + Proof. + induction x;simpl;norm. + rewrite IHx;norm. + add_push 1;rrefl. + Qed. + + Lemma ARgen_phiPOS_add : forall x y, + gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y). + Proof. + induction x;destruct y;simpl;norm. + rewrite Pplus_carry_spec. + rewrite ARgen_phiPOS_Psucc. + rewrite IHx;norm. + add_push (gen_phiPOS1 y);add_push 1;rrefl. + rewrite IHx;norm;add_push (gen_phiPOS1 y);rrefl. + rewrite ARgen_phiPOS_Psucc;norm;add_push 1;rrefl. + rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;rrefl. + rewrite IHx;norm;add_push(gen_phiPOS1 y);rrefl. + add_push 1;rrefl. + rewrite ARgen_phiPOS_Psucc;norm;add_push 1;rrefl. + Qed. + + Lemma ARgen_phiPOS_mult : + forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y. + Proof. + induction x;intros;simpl;norm. + rewrite ARgen_phiPOS_add;simpl;rewrite IHx;norm. + rewrite IHx;rrefl. + Qed. + + End ALMOST_RING. + + Variable Rth : ring_theory 0 1 radd rmul rsub ropp req. + Let ARth := Rth_ARth Rsth Reqe Rth. + Add Morphism rsub : rsub_ext4. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth. + Ltac add_push := gen_add_push radd Rsth Reqe ARth. + +(*morphisms are extensionaly equal*) + Lemma same_genZ : forall x, [x] == gen_phiZ1 x. + Proof. + destruct x;simpl; try rewrite (same_gen ARth);rrefl. + Qed. + + Lemma gen_Zeqb_ok : forall x y, + Zeq_bool x y = true -> [x] == [y]. + Proof. + intros x y H; repeat rewrite same_genZ. + assert (H1 := Zeqb_ok x y H);unfold IDphi in H1. + rewrite H1;rrefl. + Qed. + + Lemma gen_phiZ1_add_pos_neg : forall x y, + gen_phiZ1 + match (x ?= y)%positive Eq with + | Eq => Z0 + | Lt => Zneg (y - x) + | Gt => Zpos (x - y) + end + == gen_phiPOS1 x + -gen_phiPOS1 y. + Proof. + intros x y. + assert (H:= (Pcompare_Eq_eq x y)); assert (H0 := Pminus_mask_Gt x y). + generalize (Pminus_mask_Gt y x). + replace Eq with (CompOpp Eq);[intro H1;simpl|trivial]. + rewrite <- Pcompare_antisym in H1. + destruct ((x ?= y)%positive Eq). + rewrite H;trivial. rewrite (Ropp_def Rth);rrefl. + destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial. + unfold Pminus; rewrite Heq1;rewrite <- Heq2. + rewrite (ARgen_phiPOS_add ARth);simpl;norm. + rewrite (Ropp_def Rth);norm. + destruct H0 as [h [Heq1 [Heq2 Hor]]];trivial. + unfold Pminus; rewrite Heq1;rewrite <- Heq2. + rewrite (ARgen_phiPOS_add ARth);simpl;norm. + add_push (gen_phiPOS1 h);rewrite (Ropp_def Rth); norm. + Qed. + + Lemma match_compOpp : forall x (B:Type) (be bl bg:B), + match CompOpp x with Eq => be | Lt => bl | Gt => bg end + = match x with Eq => be | Lt => bg | Gt => bl end. + Proof. destruct x;simpl;intros;trivial. Qed. + + Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y]. + Proof. + intros x y; repeat rewrite same_genZ; generalize x y;clear x y. + induction x;destruct y;simpl;norm. + apply (ARgen_phiPOS_add ARth). + apply gen_phiZ1_add_pos_neg. + replace Eq with (CompOpp Eq);trivial. + rewrite <- Pcompare_antisym;simpl. + rewrite match_compOpp. + rewrite (Radd_sym Rth). + apply gen_phiZ1_add_pos_neg. + rewrite (ARgen_phiPOS_add ARth); norm. + Qed. + + Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y]. + Proof. + intros x y;repeat rewrite same_genZ. + destruct x;destruct y;simpl;norm; + rewrite (ARgen_phiPOS_mult ARth);try (norm;fail). + rewrite (Ropp_opp Rsth Reqe Rth);rrefl. + Qed. + + Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y]. + Proof. intros;subst;rrefl. Qed. + +(*proof that [.] satisfies morphism specifications*) + Lemma gen_phiZ_morph : + ring_morph 0 1 radd rmul rsub ropp req Z0 (Zpos xH) + Zplus Zmult Zminus Zopp Zeq_bool gen_phiZ. + Proof. + assert ( SRmorph : semi_morph 0 1 radd rmul req Z0 (Zpos xH) + Zplus Zmult Zeq_bool gen_phiZ). + apply mkRmorph;simpl;try rrefl. + apply gen_phiZ_add. apply gen_phiZ_mul. apply gen_Zeqb_ok. + apply (Smorph_morph Rsth Reqe Rth Zsth Zth SRmorph gen_phiZ_ext). + Qed. + +End ZMORPHISM. + +(** N is a semi-ring and a setoid*) +Lemma Nsth : Setoid_Theory N (@eq N). +Proof (Eqsth N). + +Lemma Nseqe : sring_eq_ext Nplus Nmult (@eq N). +Proof (Eq_s_ext Nplus Nmult). + +Lemma Nth : semi_ring_theory N0 (Npos xH) Nplus Nmult (@eq N). +Proof. + constructor. exact Nplus_0_l. exact Nplus_comm. exact Nplus_assoc. + exact Nmult_1_l. exact Nmult_0_l. exact Nmult_comm. exact Nmult_assoc. + exact Nmult_plus_distr_r. +Qed. + +Definition Nsub := SRsub Nplus. +Definition Nopp := (@SRopp N). + +Lemma Neqe : ring_eq_ext Nplus Nmult Nopp (@eq N). +Proof (SReqe_Reqe Nseqe). + +Lemma Nath : + almost_ring_theory N0 (Npos xH) Nplus Nmult Nsub Nopp (@eq N). +Proof (SRth_ARth Nsth Nth). + +Definition Neq_bool (x y:N) := + match Ncompare x y with + | Eq => true + | _ => false + end. + +Lemma Neq_bool_ok : forall x y, Neq_bool x y = true -> x = y. + Proof. + intros x y;unfold Neq_bool. + assert (H:=Ncompare_Eq_eq x y); + destruct (Ncompare x y);intros;try discriminate. + rewrite H;trivial. + Qed. + +(**Same as above : definition of two,extensionaly equal, generic morphisms *) +(**from N to any semi-ring*) +Section NMORPHISM. + Variable R : Type. + Variable (rO rI : R) (radd rmul: R->R->R). + Variable req : R -> R -> Prop. + Notation "0" := rO. Notation "1" := rI. + Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y). + Variable Rsth : Setoid_Theory R req. + Add Setoid R req Rsth as R_setoid4. + Ltac rrefl := gen_reflexivity Rsth. + Variable SReqe : sring_eq_ext radd rmul req. + Variable SRth : semi_ring_theory 0 1 radd rmul req. + Let ARth := SRth_ARth Rsth SRth. + Let Reqe := SReqe_Reqe SReqe. + Let ropp := (@SRopp R). + Let rsub := (@SRsub R radd). + Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). + Notation "x == y" := (req x y). + Add Morphism radd : radd_ext4. exact (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext4. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext4. exact (Ropp_ext Reqe). Qed. + Add Morphism rsub : rsub_ext5. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth. + + Definition gen_phiN1 x := + match x with + | N0 => 0 + | Npos x => gen_phiPOS1 1 radd rmul x + end. + + Definition gen_phiN x := + match x with + | N0 => 0 + | Npos x => gen_phiPOS 1 radd rmul x + end. + Notation "[ x ]" := (gen_phiN x). + + Lemma same_genN : forall x, [x] == gen_phiN1 x. + Proof. + destruct x;simpl. rrefl. + rewrite (same_gen Rsth Reqe ARth);rrefl. + Qed. + + Lemma gen_phiN_add : forall x y, [x + y] == [x] + [y]. + Proof. + intros x y;repeat rewrite same_genN. + destruct x;destruct y;simpl;norm. + apply (ARgen_phiPOS_add Rsth Reqe ARth). + Qed. + + Lemma gen_phiN_mult : forall x y, [x * y] == [x] * [y]. + Proof. + intros x y;repeat rewrite same_genN. + destruct x;destruct y;simpl;norm. + apply (ARgen_phiPOS_mult Rsth Reqe ARth). + Qed. + + Lemma gen_phiN_sub : forall x y, [Nsub x y] == [x] - [y]. + Proof. exact gen_phiN_add. Qed. + +(*gen_phiN satisfies morphism specifications*) + Lemma gen_phiN_morph : ring_morph 0 1 radd rmul rsub ropp req + N0 (Npos xH) Nplus Nmult Nsub Nopp Neq_bool gen_phiN. + Proof. + constructor;intros;simpl; try rrefl. + apply gen_phiN_add. apply gen_phiN_sub. apply gen_phiN_mult. + rewrite (Neq_bool_ok x y);trivial. rrefl. + Qed. + +End NMORPHISM. +(* +Section NNMORPHISM. +Variable R : Type. + Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). + Variable req : R -> R -> Prop. + 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). + Variable Rsth : Setoid_Theory R req. + Add Setoid R req Rsth as R_setoid5. + Ltac rrefl := gen_reflexivity Rsth. + Variable Reqe : ring_eq_ext radd rmul ropp req. + Add Morphism radd : radd_ext5. exact Reqe.(Radd_ext). Qed. + Add Morphism rmul : rmul_ext5. exact Reqe.(Rmul_ext). Qed. + Add Morphism ropp : ropp_ext5. exact Reqe.(Ropp_ext). Qed. + + Lemma SReqe : sring_eq_ext radd rmul req. + case Reqe; constructor; trivial. + Qed. + + Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. + Add Morphism rsub : rsub_ext6. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth. + Ltac add_push := gen_add_push radd Rsth Reqe ARth. + + Lemma SRth : semi_ring_theory 0 1 radd rmul req. + case ARth; constructor; trivial. + Qed. + + Definition NN := prod N N. + Definition gen_phiNN (x:NN) := + rsub (gen_phiN rO rI radd rmul (fst x)) (gen_phiN rO rI radd rmul (snd x)). + Notation "[ x ]" := (gen_phiNN x). + + Definition NNadd (x y : NN) : NN := + (fst x + fst y, snd x + snd y)%N. + Definition NNmul (x y : NN) : NN := + (fst x * fst y + snd x * snd y, fst y * snd x + fst x * snd y)%N. + Definition NNopp (x:NN) : NN := (snd x, fst x)%N. + Definition NNsub (x y:NN) : NN := (fst x + snd y, fst y + snd x)%N. + + + Lemma gen_phiNN_add : forall x y, [NNadd x y] == [x] + [y]. + Proof. +intros. +unfold NNadd, gen_phiNN in |- *; simpl in |- *. +repeat rewrite (gen_phiN_add Rsth SReqe SRth). +norm. +add_push (- gen_phiN 0 1 radd rmul (snd x)). +rrefl. +Qed. + + Hypothesis ropp_involutive : forall x, - - x == x. + + + Lemma gen_phiNN_mult : forall x y, [NNmul x y] == [x] * [y]. + Proof. +intros. +unfold NNmul, gen_phiNN in |- *; simpl in |- *. +repeat rewrite (gen_phiN_add Rsth SReqe SRth). +repeat rewrite (gen_phiN_mult Rsth SReqe SRth). +norm. +rewrite ropp_involutive. +add_push (- (gen_phiN 0 1 radd rmul (fst y) * gen_phiN 0 1 radd rmul (snd x))). +add_push ( gen_phiN 0 1 radd rmul (snd x) * gen_phiN 0 1 radd rmul (snd y)). +rewrite (ARmul_sym ARth (gen_phiN 0 1 radd rmul (fst y)) + (gen_phiN 0 1 radd rmul (snd x))). +rrefl. +Qed. + + Lemma gen_phiNN_sub : forall x y, [NNsub x y] == [x] - [y]. +intros. +unfold NNsub, gen_phiNN; simpl. +repeat rewrite (gen_phiN_add Rsth SReqe SRth). +repeat rewrite (ARsub_def ARth). +repeat rewrite (ARopp_add ARth). +repeat rewrite (ARadd_assoc ARth). +rewrite ropp_involutive. +add_push (- gen_phiN 0 1 radd rmul (fst y)). +add_push ( - gen_phiN 0 1 radd rmul (snd x)). +rrefl. +Qed. + + +Definition NNeqbool (x y: NN) := + andb (Neq_bool (fst x) (fst y)) (Neq_bool (snd x) (snd y)). + +Lemma NNeqbool_ok0 : forall x y, + NNeqbool x y = true -> x = y. +unfold NNeqbool in |- *. +intros. +assert (Neq_bool (fst x) (fst y) = true). + generalize H. + case (Neq_bool (fst x) (fst y)); simpl in |- *; trivial. + assert (Neq_bool (snd x) (snd y) = true). + rewrite H0 in H; simpl in |- *; trivial. + generalize H0 H1. + destruct x; destruct y; simpl in |- *. + intros. + replace n with n1. + replace n2 with n0; trivial. + apply Neq_bool_ok; trivial. + symmetry in |- *. + apply Neq_bool_ok; trivial. +Qed. + + +(*gen_phiN satisfies morphism specifications*) + Lemma gen_phiNN_morph : ring_morph 0 1 radd rmul rsub ropp req + (N0,N0) (Npos xH,N0) NNadd NNmul NNsub NNopp NNeqbool gen_phiNN. + Proof. + constructor;intros;simpl; try rrefl. + apply gen_phiN_add. apply gen_phiN_sub. apply gen_phiN_mult. + rewrite (Neq_bool_ok x y);trivial. rrefl. + Qed. + +End NNMORPHISM. + +Section NSTARMORPHISM. +Variable R : Type. + Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). + Variable req : R -> R -> Prop. + 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). + Variable Rsth : Setoid_Theory R req. + Add Setoid R req Rsth as R_setoid3. + Ltac rrefl := gen_reflexivity Rsth. + Variable Reqe : ring_eq_ext radd rmul ropp req. + Add Morphism radd : radd_ext3. exact Reqe.(Radd_ext). Qed. + Add Morphism rmul : rmul_ext3. exact Reqe.(Rmul_ext). Qed. + Add Morphism ropp : ropp_ext3. exact Reqe.(Ropp_ext). Qed. + + Lemma SReqe : sring_eq_ext radd rmul req. + case Reqe; constructor; trivial. + Qed. + + Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. + Add Morphism rsub : rsub_ext7. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth. + Ltac add_push := gen_add_push radd Rsth Reqe ARth. + + Lemma SRth : semi_ring_theory 0 1 radd rmul req. + case ARth; constructor; trivial. + Qed. + + Inductive Nword : Set := + Nlast (p:positive) + | Ndigit (n:N) (w:Nword). + + Fixpoint opp_iter (n:nat) (t:R) {struct n} : R := + match n with + O => t + | S k => ropp (opp_iter k t) + end. + + Fixpoint gen_phiNword (x:Nword) (n:nat) {struct x} : R := + match x with + Nlast p => opp_iter n (gen_phi_pos p) + | Ndigit N0 w => gen_phiNword w (S n) + | Ndigit m w => radd (opp_iter n (gen_phiN m)) (gen_phiNword w (S n)) + end. + Notation "[ x ]" := (gen_phiNword x). + + Fixpoint Nwadd (x y : Nword) {struct x} : Nword := + match x, y with + Nlast p1, Nlast p2 => Nlast (p1+p2)%positive + | Nlast p1, Ndigit n w => Ndigit (Npos p1 + n)%N w + | Ndigit n w, Nlast p1 => Ndigit (n + Npos p1)%N w + | Ndigit n1 w1, Ndigit n2 w2 => Ndigit (n1+n2)%N (Nwadd w1 w2) + end. + Fixpoint Nwmulp (x:positive) (y:Nword) {struct y} : Nword := + match y with + Nlast p => Nlast (x*p)%positive + | Ndigit n w => Ndigit (Npos x * n)%N (Nwmulp x w) + end. + Definition Nwmul (x y : Nword) {struct x} : Nword := + match x with + Nlast k => Nmulp k y + | Ndigit N0 w => Ndigit N0 (Nwmul w y) + | Ndigit (Npos k) w => + Nwadd (Nwmulp k y) (Ndigit N0 (Nwmul w y)) + end. + + Definition Nwopp (x:Nword) : Nword := Ndigit N0 x. + Definition Nwsub (x y:NN) : NN := (Nwadd x (Ndigit N0 y)). + + + Lemma gen_phiNN_add : forall x y, [NNadd x y] == [x] + [y]. + Proof. +intros. +unfold NNadd, gen_phiNN in |- *; simpl in |- *. +repeat rewrite (gen_phiN_add Rsth SReqe SRth). +norm. +add_push (- gen_phiN 0 1 radd rmul (snd x)). +rrefl. +Qed. + + Lemma gen_phiNN_mult : forall x y, [NNmul x y] == [x] * [y]. + Proof. +intros. +unfold NNmul, gen_phiNN in |- *; simpl in |- *. +repeat rewrite (gen_phiN_add Rsth SReqe SRth). +repeat rewrite (gen_phiN_mult Rsth SReqe SRth). +norm. +rewrite ropp_involutive. +add_push (- (gen_phiN 0 1 radd rmul (fst y) * gen_phiN 0 1 radd rmul (snd x))). +add_push ( gen_phiN 0 1 radd rmul (snd x) * gen_phiN 0 1 radd rmul (snd y)). +rewrite (ARmul_sym ARth (gen_phiN 0 1 radd rmul (fst y)) + (gen_phiN 0 1 radd rmul (snd x))). +rrefl. +Qed. + + Lemma gen_phiNN_sub : forall x y, [NNsub x y] == [x] - [y]. +intros. +unfold NNsub, gen_phiNN; simpl. +repeat rewrite (gen_phiN_add Rsth SReqe SRth). +repeat rewrite (ARsub_def ARth). +repeat rewrite (ARopp_add ARth). +repeat rewrite (ARadd_assoc ARth). +rewrite ropp_involutive. +add_push (- gen_phiN 0 1 radd rmul (fst y)). +add_push ( - gen_phiN 0 1 radd rmul (snd x)). +rrefl. +Qed. + + +Definition NNeqbool (x y: NN) := + andb (Neq_bool (fst x) (fst y)) (Neq_bool (snd x) (snd y)). + +Lemma NNeqbool_ok0 : forall x y, + NNeqbool x y = true -> x = y. +unfold NNeqbool in |- *. +intros. +assert (Neq_bool (fst x) (fst y) = true). + generalize H. + case (Neq_bool (fst x) (fst y)); simpl in |- *; trivial. + assert (Neq_bool (snd x) (snd y) = true). + rewrite H0 in H; simpl in |- *; trivial. + generalize H0 H1. + destruct x; destruct y; simpl in |- *. + intros. + replace n with n1. + replace n2 with n0; trivial. + apply Neq_bool_ok; trivial. + symmetry in |- *. + apply Neq_bool_ok; trivial. +Qed. + + +(*gen_phiN satisfies morphism specifications*) + Lemma gen_phiNN_morph : ring_morph 0 1 radd rmul rsub ropp req + (N0,N0) (Npos xH,N0) NNadd NNmul NNsub NNopp NNeqbool gen_phiNN. + Proof. + constructor;intros;simpl; try rrefl. + apply gen_phiN_add. apply gen_phiN_sub. apply gen_phiN_mult. + rewrite (Neq_bool_ok x y);trivial. rrefl. + Qed. + +End NSTARMORPHISM. +*) + + (* syntaxification of constants in an abstract ring *) + Ltac inv_gen_phi_pos rI add mul t := + let rec inv_cst t := + match t with + rI => constr:1%positive + | (add rI rI) => constr:2%positive + | (add rI (add rI rI)) => constr:3%positive + | (mul (add rI rI) ?p) => (* 2p *) + match inv_cst p with + NotConstant => NotConstant + | 1%positive => NotConstant + | ?p => constr:(xO p) + end + | (add rI (mul (add rI rI) ?p)) => (* 1+2p *) + match inv_cst p with + NotConstant => NotConstant + | 1%positive => NotConstant + | ?p => constr:(xI p) + end + | _ => NotConstant + end in + inv_cst t. + + Ltac inv_gen_phiN rO rI add mul t := + match t with + rO => constr:0%N + | _ => + match inv_gen_phi_pos rI add mul t with + NotConstant => NotConstant + | ?p => constr:(Npos p) + end + end. + + Ltac inv_gen_phiZ rO rI add mul opp t := + match t with + rO => constr:0%Z + | (opp ?p) => + match inv_gen_phi_pos rI add mul p with + NotConstant => NotConstant + | ?p => constr:(Zneg p) + end + | _ => + match inv_gen_phi_pos rI add mul t with + NotConstant => NotConstant + | ?p => constr:(Zpos p) + end + end. +(* coefs = Z (abstract ring) *) +Module Zpol. + +Definition ring_gen_correct + R rO rI radd rmul rsub ropp req rSet req_th Rth := + @ring_correct R rO rI radd rmul rsub ropp req rSet req_th + (Rth_ARth rSet req_th Rth) + Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool + (@gen_phiZ R rO rI radd rmul ropp) + (@gen_phiZ_morph R rO rI radd rmul rsub ropp req rSet req_th Rth). + +Definition ring_rw_gen_correct + R rO rI radd rmul rsub ropp req rSet req_th Rth := + @Pphi_dev_ok R rO rI radd rmul rsub ropp req rSet req_th + (Rth_ARth rSet req_th Rth) + Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool + (@gen_phiZ R rO rI radd rmul ropp) + (@gen_phiZ_morph R rO rI radd rmul rsub ropp req rSet req_th Rth). + +Definition ring_rw_gen_correct' + R rO rI radd rmul rsub ropp req rSet req_th Rth := + @Pphi_dev_ok' R rO rI radd rmul rsub ropp req rSet req_th + (Rth_ARth rSet req_th Rth) + Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool + (@gen_phiZ R rO rI radd rmul ropp) + (@gen_phiZ_morph R rO rI radd rmul rsub ropp req rSet req_th Rth). + +Definition ring_gen_eq_correct R rO rI radd rmul rsub ropp Rth := + @ring_gen_correct + R rO rI radd rmul rsub ropp (@eq R) (Eqsth R) (Eq_ext _ _ _) Rth. + +Definition ring_rw_gen_eq_correct R rO rI radd rmul rsub ropp Rth := + @ring_rw_gen_correct + R rO rI radd rmul rsub ropp (@eq R) (Eqsth R) (Eq_ext _ _ _) Rth. + +Definition ring_rw_gen_eq_correct' R rO rI radd rmul rsub ropp Rth := + @ring_rw_gen_correct' + R rO rI radd rmul rsub ropp (@eq R) (Eqsth R) (Eq_ext _ _ _) Rth. + +End Zpol. + +(* coefs = N (abstract semi-ring) *) +Module Npol. + +Definition ring_gen_correct + R rO rI radd rmul req rSet req_th SRth := + @ring_correct R rO rI radd rmul (SRsub radd) (@SRopp R) req rSet + (SReqe_Reqe req_th) + (SRth_ARth rSet SRth) + N 0%N 1%N Nplus Nmult (SRsub Nplus) (@SRopp N) Neq_bool + (@gen_phiN R rO rI radd rmul) + (@gen_phiN_morph R rO rI radd rmul req rSet req_th SRth). + +Definition ring_rw_gen_correct + R rO rI radd rmul req rSet req_th SRth := + @Pphi_dev_ok R rO rI radd rmul (SRsub radd) (@SRopp R) req rSet + (SReqe_Reqe req_th) + (SRth_ARth rSet SRth) + N 0%N 1%N Nplus Nmult (SRsub Nplus) (@SRopp N) Neq_bool + (@gen_phiN R rO rI radd rmul) + (@gen_phiN_morph R rO rI radd rmul req rSet req_th SRth). + +Definition ring_rw_gen_correct' + R rO rI radd rmul req rSet req_th SRth := + @Pphi_dev_ok' R rO rI radd rmul (SRsub radd) (@SRopp R) req rSet + (SReqe_Reqe req_th) + (SRth_ARth rSet SRth) + N 0%N 1%N Nplus Nmult (SRsub Nplus) (@SRopp N) Neq_bool + (@gen_phiN R rO rI radd rmul) + (@gen_phiN_morph R rO rI radd rmul req rSet req_th SRth). + +Definition ring_gen_eq_correct R rO rI radd rmul SRth := + @ring_gen_correct + R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth. + +Definition ring_rw_gen_eq_correct R rO rI radd rmul SRth := + @ring_rw_gen_correct + R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth. + +Definition ring_rw_gen_eq_correct' R rO rI radd rmul SRth := + @ring_rw_gen_correct' + R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth. + +End Npol. + +(* Z *) + +Ltac isZcst t := + match t with + Z0 => constr:true + | Zpos ?p => isZcst p + | Zneg ?p => isZcst p + | xI ?p => isZcst p + | xO ?p => isZcst p + | xH => constr:true + | _ => constr:false + end. +Ltac Zcst t := + match isZcst t with + true => t + | _ => NotConstant + end. + +Add New Ring Zr : Zth Computational Zeqb_ok Constant Zcst. + +(* N *) + +Ltac isNcst t := + match t with + N0 => constr:true + | Npos ?p => isNcst p + | xI ?p => isNcst p + | xO ?p => isNcst p + | xH => constr:true + | _ => constr:false + end. +Ltac Ncst t := + match isNcst t with + true => t + | _ => NotConstant + end. + +Add New Ring Nr : Nth Computational Neq_bool_ok Constant Ncst. + +(* nat *) + +Ltac isnatcst t := + match t with + O => true + | S ?p => isnatcst p + | _ => false + end. +Ltac natcst t := + match isnatcst t with + true => t + | _ => NotConstant + end. + + Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat). + Proof. + constructor. exact plus_0_l. exact plus_comm. exact plus_assoc. + exact mult_1_l. exact mult_0_l. exact mult_comm. exact mult_assoc. + exact mult_plus_distr_r. + Qed. + + +Unboxed Fixpoint nateq (n m:nat) {struct m} : bool := + match n, m with + | O, O => true + | S n', S m' => nateq n' m' + | _, _ => false + end. + +Lemma nateq_ok : forall n m:nat, nateq n m = true -> n = m. +Proof. + simple induction n; simple induction m; simpl; intros; try discriminate. + trivial. + rewrite (H n1 H1). + trivial. +Qed. + +Add New Ring natr : natSRth Computational nateq_ok Constant natcst. + diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 new file mode 100644 index 00000000..7041d7e8 --- /dev/null +++ b/contrib/setoid_ring/newring.ml4 @@ -0,0 +1,525 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(*i $Id: newring.ml4 7974 2006-02-01 19:02:09Z barras $ i*) + +open Pp +open Util +open Names +open Term +open Closure +open Environ +open Tactics +open Rawterm +open Tacticals +open Tacexpr +open Pcoq +open Tactic +open Constr +open Setoid_replace +open Proof_type +open Coqlib +open Tacmach +open Ppconstr +open Mod_subst +open Tacinterp +open Libobject +open Printer + +(****************************************************************************) +(* Library linking *) + +let contrib_name = "setoid_ring" + + +let ring_dir = ["Coq";contrib_name] +let setoids_dir = ["Coq";"Setoids"] +let ring_modules = + [ring_dir@["BinList"];ring_dir@["Ring_th"];ring_dir@["Pol"]; + ring_dir@["Ring_tac"];ring_dir@["ZRing_th"]] +let stdlib_modules = [setoids_dir@["Setoid"]] + +let coq_constant c = + lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c) +let ring_constant c = + lazy (Coqlib.gen_constant_in_modules "Ring" ring_modules c) +let ringtac_constant m c = + lazy (Coqlib.gen_constant_in_modules "Ring" [ring_dir@["ZRing_th";m]] c) + +let new_ring_path = + make_dirpath (List.map id_of_string ["Ring_tac";contrib_name;"Coq"]) +let ltac s = + lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s)) +let znew_ring_path = + make_dirpath (List.map id_of_string ["ZRing_th";contrib_name;"Coq"]) +let zltac s = + lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s)) +let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c) + +let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);; +let pol_cst s = mk_cst [contrib_name;"Pol"] s ;; + +let ic c = + let env = Global.env() and sigma = Evd.empty in + Constrintern.interp_constr sigma env c + + +(* Ring theory *) + +(* almost_ring defs *) +let coq_almost_ring_theory = ring_constant "almost_ring_theory" +let coq_ring_lemma1 = ring_constant "ring_correct" +let coq_ring_lemma2 = ring_constant "Pphi_dev_ok'" +let ring_comp1 = ring_constant "ring_id_correct" +let ring_comp2 = ring_constant "ring_rw_id_correct'" +let ring_abs1 = ringtac_constant "Zpol" "ring_gen_correct" +let ring_abs2 = ringtac_constant "Zpol" "ring_rw_gen_correct'" +let sring_abs1 = ringtac_constant "Npol" "ring_gen_correct" +let sring_abs2 = ringtac_constant "Npol" "ring_rw_gen_correct'" + +(* setoid and morphism utilities *) +let coq_mk_Setoid = coq_constant "Build_Setoid_Theory" +let coq_eq_setoid = ring_constant "Eqsth" +let coq_eq_morph = ring_constant "Eq_ext" + +(* ring -> almost_ring utilities *) +let coq_ring_theory = ring_constant "ring_theory" +let coq_ring_morph = ring_constant "ring_morph" +let coq_Rth_ARth = ring_constant "Rth_ARth" +let coq_mk_reqe = ring_constant "mk_reqe" + +(* semi_ring -> almost_ring utilities *) +let coq_semi_ring_theory = ring_constant "semi_ring_theory" +let coq_SRth_ARth = ring_constant "SRth_ARth" +let coq_sring_morph = ring_constant "semi_morph" +let coq_SRmorph_Rmorph = ring_constant "SRmorph_Rmorph" +let coq_mk_seqe = ring_constant "mk_seqe" +let coq_SRsub = ring_constant "SRsub" +let coq_SRopp = ring_constant "SRopp" +let coq_SReqe_Reqe = ring_constant "SReqe_Reqe" + +let ltac_setoid_ring = ltac"Make_ring_tac" +let ltac_setoid_ring_rewrite = ltac"Make_ring_rw_list" +let ltac_inv_morphZ = zltac"inv_gen_phiZ" +let ltac_inv_morphN = zltac"inv_gen_phiN" + +let coq_cons = ring_constant "cons" +let coq_nil = ring_constant "nil" + +let lapp f args = mkApp(Lazy.force f,args) + +let dest_rel t = + match kind_of_term t with + App(f,args) when Array.length args >= 2 -> + mkApp(f,Array.sub args 0 (Array.length args - 2)) + | _ -> failwith "cannot find relation" + +(****************************************************************************) +(* controlled reduction *) + +let mark_arg i c = mkEvar(i,[|c|]);; +let unmark_arg f c = + match destEvar c with + | (i,[|c|]) -> f i c + | _ -> assert false;; + +type protect_flag = Eval|Prot|Rec ;; + +let tag_arg tag_rec map i c = + match map i with + Eval -> inject c + | Prot -> mk_atom c + | Rec -> if i = -1 then inject c else tag_rec c + +let rec mk_clos_but f_map t = + match f_map t with + | Some map -> tag_arg (mk_clos_but f_map) map (-1) t + | None -> + (match kind_of_term t with + App(f,args) -> mk_clos_app_but f_map f args 0 + (* unspecified constants are evaluated *) + | _ -> inject t) + +and mk_clos_app_but f_map f args n = + if n >= Array.length args then inject(mkApp(f, args)) + else + let fargs, args' = array_chop n args in + let f' = mkApp(f,fargs) in + match f_map f' with + Some map -> + mk_clos_deep + (fun _ -> unmark_arg (tag_arg (mk_clos_but f_map) map)) + (Esubst.ESID 0) + (mkApp (mark_arg (-1) f', Array.mapi mark_arg args')) + | None -> mk_clos_app_but f_map f args (n+1) +;; + +let interp_map l c = + try + let (im,am) = List.assoc c l in + Some(fun i -> + if List.mem i im then Eval + else if List.mem i am then Prot + else if i = -1 then Eval + else Rec) + with Not_found -> None + +let interp_map l t = + try Some(List.assoc t l) with Not_found -> None + +let arg_map = + [mk_cst [contrib_name;"BinList"] "cons",(function -1->Eval|2->Rec|_->Prot); + mk_cst [contrib_name;"BinList"] "nil", (function -1->Eval|_ -> Prot); + (* Pphi_dev: evaluate polynomial and coef operations, protect + ring operations and make recursive call on morphism and var map *) + pol_cst "Pphi_dev", (function -1|6|7|8|11->Eval|9|10->Rec|_->Prot); + (* PEeval: evaluate polynomial, protect ring operations + and make recursive call on morphism and var map *) + pol_cst "PEeval", (function -1|9->Eval|7|8->Rec|_->Prot); + (* Do not evaluate ring operations... *) + ring_constant "gen_phiZ", (function -1|6->Eval|_->Prot); + ring_constant "gen_phiN", (function -1|5->Eval|_->Prot); +];; + +(* Equality: do not evaluate but make recursive call on both sides *) +let is_ring_thm req = + interp_map + ((req,(function -1->Prot|_->Rec)):: + List.map (fun (c,map) -> (Lazy.force c,map)) arg_map) +;; + +let protect_red env sigma c = + let req = dest_rel c in + kl (create_clos_infos betadeltaiota env) + (mk_clos_but (is_ring_thm req) c);; + +let protect_tac = + Tactics.reduct_option (protect_red,DEFAULTcast) None ;; + +let protect_tac_in id = + Tactics.reduct_option (protect_red,DEFAULTcast) (Some(id,[],InHyp));; + + +TACTIC EXTEND protect_fv + [ "protect_fv" "in" ident(id) ] -> + [ protect_tac_in id ] +| [ "protect_fv" ] -> + [ protect_tac ] +END;; + +(****************************************************************************) +(* Ring database *) + +let ty c = Typing.type_of (Global.env()) Evd.empty c + + +type ring_info = + { ring_carrier : types; + ring_req : constr; + ring_cst_tac : glob_tactic_expr; + ring_lemma1 : constr; + ring_lemma2 : constr } + +module Cmap = Map.Make(struct type t = constr let compare = compare end) + +let from_carrier = ref Cmap.empty +let from_relation = ref Cmap.empty + +let _ = + Summary.declare_summary "tactic-new-ring-table" + { Summary.freeze_function = (fun () -> !from_carrier,!from_relation); + Summary.unfreeze_function = + (fun (ct,rt) -> from_carrier := ct; from_relation := rt); + Summary.init_function = + (fun () -> from_carrier := Cmap.empty; from_relation := Cmap.empty); + Summary.survive_module = false; + Summary.survive_section = false } + +let add_entry _ e = + let _ = ty e.ring_lemma1 in + let _ = ty e.ring_lemma2 in + from_carrier := Cmap.add e.ring_carrier e !from_carrier; + from_relation := Cmap.add e.ring_req e !from_relation + + +let subst_th (_,subst,th) = + let c' = subst_mps subst th.ring_carrier in + let eq' = subst_mps subst th.ring_req in + let thm1' = subst_mps subst th.ring_lemma1 in + let thm2' = subst_mps subst th.ring_lemma2 in + let tac'= subst_tactic subst th.ring_cst_tac in + if c' == th.ring_carrier && + eq' == th.ring_req && + thm1' == th.ring_lemma1 && + thm2' == th.ring_lemma2 && + tac' == th.ring_cst_tac then th + else + { ring_carrier = c'; + ring_req = eq'; + ring_cst_tac = tac'; + ring_lemma1 = thm1'; + ring_lemma2 = thm2' } + + +let (theory_to_obj, obj_to_theory) = + let cache_th (name,th) = add_entry name th + and export_th x = Some x in + declare_object + {(default_object "tactic-new-ring-theory") with + open_function = (fun i o -> if i=1 then cache_th o); + cache_function = cache_th; + subst_function = subst_th; + classify_function = (fun (_,x) -> Substitute x); + export_function = export_th } + + +let ring_for_carrier r = Cmap.find r !from_carrier + +let ring_for_relation rel = Cmap.find rel !from_relation + +let setoid_of_relation r = + lapp coq_mk_Setoid + [|r.rel_a; r.rel_aeq; + out_some r.rel_refl; out_some r.rel_sym; out_some r.rel_trans |] + +let op_morph r add mul opp req m1 m2 m3 = + lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |] + +let op_smorph r add mul req m1 m2 = + lapp coq_SReqe_Reqe + [| r;add;mul;req;lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |]|] + +let sr_sub r add = lapp coq_SRsub [|r;add|] +let sr_opp r = lapp coq_SRopp [|r|] + +let dest_morphism kind th sth = + let th_typ = Retyping.get_type_of (Global.env()) Evd.empty th in + match kind_of_term th_typ with + App(f,[|_;_;_;_;_;_;_;_;c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|]) + when f = Lazy.force coq_ring_morph -> + (th,[|c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|]) + | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|]) + when f = Lazy.force coq_sring_morph && kind=Some true-> + let th = + lapp coq_SRmorph_Rmorph + [|r;zero;one;add;mul;req;sth;c;czero;cone;cadd;cmul;ceqb;phi;th|]in + (th,[|c;czero;cone;cadd;cmul;cadd;sr_opp c;ceqb;phi|]) + | _ -> failwith "bad ring_morph lemma" + +let dest_eq_test th = + let th_typ = Retyping.get_type_of (Global.env()) Evd.empty th in + match decompose_prod th_typ with + (_,h)::_,_ -> + (match snd(destApplication h) with + [|_;lhs;_|] -> fst(destApplication lhs) + | _ -> failwith "bad lemma for decidability of equality") + | _ -> failwith "bad lemma for decidability of equality" + +let default_ring_equality is_semi (r,add,mul,opp,req) = + let is_setoid = function + {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _} -> true + | _ -> false in + match default_relation_for_carrier ~filter:is_setoid r with + Leibniz _ -> + let setoid = lapp coq_eq_setoid [|r|] in + let op_morph = lapp coq_eq_morph [|r;add;mul;opp|] in + (setoid,op_morph) + | Relation rel -> + let setoid = setoid_of_relation rel in + let is_endomorphism = function + { args=args } -> List.for_all + (function (var,Relation rel) -> + var=None && eq_constr req rel + | _ -> false) args in + let add_m = + try default_morphism ~filter:is_endomorphism add + with Not_found -> + error "ring addition should be declared as a morphism" in + let mul_m = + try default_morphism ~filter:is_endomorphism mul + with Not_found -> + error "ring multiplication should be declared as a morphism" in + let op_morph = + if is_semi <> Some true then + (let opp_m = default_morphism ~filter:is_endomorphism opp in + let op_morph = + op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in + msgnl + (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++ + str"and morphisms \""++pr_constr add_m.morphism_theory++ + str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ + str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ + str"\""); + op_morph) + else + (msgnl + (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++ + str"and morphisms \""++pr_constr add_m.morphism_theory++ + str"\""++spc()++str"and \""++ + pr_constr mul_m.morphism_theory++str"\""); + op_smorph r add mul req add_m.lem mul_m.lem) in + (setoid,op_morph) + +let build_setoid_params is_semi r add mul opp req eqth = + match eqth with + Some th -> th + | None -> default_ring_equality is_semi (r,add,mul,opp,req) + +let dest_ring th_spec = + let th_typ = Retyping.get_type_of (Global.env()) Evd.empty th_spec in + match kind_of_term th_typ with + App(f,[|r;zero;one;add;mul;sub;opp;req|]) + when f = Lazy.force coq_almost_ring_theory -> + (None,r,zero,one,add,mul,sub,opp,req) + | App(f,[|r;zero;one;add;mul;req|]) + when f = Lazy.force coq_semi_ring_theory -> + (Some true,r,zero,one,add,mul,sr_sub r add,sr_opp r,req) + | App(f,[|r;zero;one;add;mul;sub;opp;req|]) + when f = Lazy.force coq_ring_theory -> + (Some false,r,zero,one,add,mul,sub,opp,req) + | _ -> error "bad ring structure" + + +let build_almost_ring kind r zero one add mul sub opp req sth morph th = + match kind with + None -> th + | Some true -> + lapp coq_SRth_ARth [|r;zero;one;add;mul;req;sth;th|] + | Some false -> + lapp coq_Rth_ARth [|r;zero;one;add;mul;sub;opp;req;sth;morph;th|] + + +type coeff_spec = + Computational of constr (* equality test *) + | Abstract (* coeffs = Z *) + | Morphism of constr (* general morphism *) + +type cst_tac_spec = + CstTac of raw_tactic_expr + | Closed of constr list + + +let add_theory name rth eqth morphth cst_tac = + Coqlib.check_required_library ["Coq";"setoid_ring";"Ring_tac"]; + let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring rth in + let (sth,morph) = build_setoid_params kind r add mul opp req eqth in + let args0 = [|r;zero;one;add;mul;sub;opp;req;sth;morph|] in + let (lemma1,lemma2) = + match morphth with + | Computational c -> + let reqb = dest_eq_test c in + let rth = + build_almost_ring + kind r zero one add mul sub opp req sth morph rth in + let args = Array.append args0 [|rth;reqb;c|] in + (lapp ring_comp1 args, lapp ring_comp2 args) + | Morphism m -> + let (m,args1) = dest_morphism kind m sth in + let rth = + build_almost_ring + kind r zero one add mul sub opp req sth morph rth in + let args = Array.concat [args0;[|rth|]; args1; [|m|]] in + (lapp coq_ring_lemma1 args, lapp coq_ring_lemma2 args) + | Abstract -> + Coqlib.check_required_library ["Coq";"setoid_ring";"ZRing_th"]; + let args1 = Array.append args0 [|rth|] in + (match kind with + None -> error "an almost_ring cannot be abstract" + | Some true -> + (lapp sring_abs1 args1, lapp sring_abs2 args1) + | Some false -> + (lapp ring_abs1 args1, lapp ring_abs2 args1)) in + let cst_tac = match cst_tac with + Some (CstTac t) -> Tacinterp.glob_tactic t + | Some (Closed lc) -> failwith "TODO" + | None -> + (match kind with + Some true -> + let t = Genarg.ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in + TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul])) + | Some false -> + let t = Genarg.ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in + TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) + | _ -> error"a tactic must be specified for an almost_ring") in + let _ = + Lib.add_leaf name + (theory_to_obj + { ring_carrier = r; + ring_req = req; + ring_cst_tac = cst_tac; + ring_lemma1 = lemma1; + ring_lemma2 = lemma2 }) in + () + +VERNAC ARGUMENT EXTEND ring_coefs +| [ "Computational" constr(c)] -> [ Computational (ic c) ] +| [ "Abstract" ] -> [ Abstract ] +| [ "Coefficients" constr(m)] -> [ Morphism (ic m) ] +| [ ] -> [ Abstract ] +END + +VERNAC ARGUMENT EXTEND ring_cst_tac +| [ "Constant" tactic(c)] -> [ Some(CstTac c) ] +| [ "[" ne_constr_list(l) "]" ] -> [ Some(Closed (List.map ic l)) ] +| [ ] -> [ None ] +END + +VERNAC COMMAND EXTEND AddSetoidRing +| [ "Add" "New" "Ring" ident(id) ":" constr(t) ring_coefs(c) + "Setoid" constr(e) constr(m) ring_cst_tac(tac) ] -> + [ add_theory id (ic t) (Some (ic e, ic m)) c tac ] +| [ "Add" "New" "Ring" ident(id) ":" constr(t) ring_coefs(c) + ring_cst_tac(tac) ] -> + [ add_theory id (ic t) None c tac ] +END + + +(*****************************************************************************) +(* The tactics consist then only in a lookup in the ring database and + call the appropriate ltac. *) + +let ring gl = + let req = dest_rel (pf_concl gl) in + let e = + try ring_for_relation req + with Not_found -> + errorlabstrm "ring" + (str"cannot find a declared ring structure for equality"++ + spc()++str"\""++pr_constr req++str"\"") in + Tacinterp.eval_tactic + (TacArg(TacCall(dummy_loc, + Genarg.ArgArg(dummy_loc, Lazy.force ltac_setoid_ring), + Tacexp e.ring_cst_tac:: + List.map carg [e.ring_lemma1;e.ring_lemma2;e.ring_req]))) + gl + +let ring_rewrite rl = + let ty = Retyping.get_type_of (Global.env()) Evd.empty (List.hd rl) in + let e = + try ring_for_carrier ty + with Not_found -> + errorlabstrm "ring" + (str"cannot find a declared ring structure over"++ + spc()++str"\""++pr_constr ty++str"\"") in + let rl = List.fold_right (fun x l -> lapp coq_cons [|ty;x;l|]) rl + (lapp coq_nil [|ty|]) in + Tacinterp.eval_tactic + (TacArg(TacCall(dummy_loc, + Genarg.ArgArg(dummy_loc, Lazy.force ltac_setoid_ring_rewrite), + Tacexp e.ring_cst_tac::List.map carg [e.ring_lemma2;e.ring_req;rl]))) + +let setoid_ring = function + | [] -> ring + | l -> ring_rewrite l + +TACTIC EXTEND setoid_ring + [ "setoid" "ring" constr_list(l) ] -> [ setoid_ring l ] +END + |