diff options
Diffstat (limited to 'contrib/setoid_ring/Ring_tac.v')
| -rw-r--r-- | contrib/setoid_ring/Ring_tac.v | 754 |
1 files changed, 754 insertions, 0 deletions
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. + +*) |