diff options
author | 2006-11-21 21:38:49 +0000 | |
---|---|---|
committer | 2006-11-21 21:38:49 +0000 | |
commit | 70b9be8acc1d1ada178a95c1cd4013506e9d0d1b (patch) | |
tree | f672a286d962cc67c95874b3b60402fc957870b6 /contrib/setoid_ring/Ring_tac.v | |
parent | a5bd4e097a94cc4f863bf4d4bcc5ce592c30ba47 (diff) | |
parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) |
Merge commit 'upstream/8.1.gamma' into 8.1
Diffstat (limited to 'contrib/setoid_ring/Ring_tac.v')
-rw-r--r-- | contrib/setoid_ring/Ring_tac.v | 794 |
1 files changed, 100 insertions, 694 deletions
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v index 6c3f87a5..95efde7f 100644 --- a/contrib/setoid_ring/Ring_tac.v +++ b/contrib/setoid_ring/Ring_tac.v @@ -1,76 +1,73 @@ Set Implicit Arguments. Require Import Setoid. -Require Import BinList. Require Import BinPos. -Require Import Pol. +Require Import Ring_polynom. +Require Import BinList. 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 +(* adds a definition id' on the normal form of t and an hypothesis id + stating that t = id' (tries to produces a proof as small as possible) *) +Ltac compute_assertion id id' t := + let t' := eval vm_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')]). +(********************************************************************) +(* Tacticals to build reflexive tactics *) -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 +Ltac OnEquation req := + match goal with + | |- req ?lhs ?rhs => (fun f => f lhs rhs) + | _ => fail 1 "Goal is not an equation (of expected equality)" 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 +Ltac OnMainSubgoal H ty := + match ty with + | _ -> ?ty' => + let subtac := OnMainSubgoal H ty' in + fun tac => lapply H; [clear H; intro H; subtac tac | idtac] + | _ => (fun tac => tac) 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*) +Ltac ApplyLemmaAndSimpl tac lemma pe:= + let npe := fresh "ast_nf" in + let H := fresh "eq_nf" in + let Heq := fresh "thm" in + let npe_spec := + match type of (lemma pe) with + forall npe, ?npe_spec = npe -> _ => npe_spec + | _ => fail 1 "ApplyLemmaAndSimpl: cannot find norm expression" + end in + (compute_assertion H npe npe_spec; + (assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma"); + clear H; + OnMainSubgoal Heq ltac:(type of Heq) + ltac:(tac Heq; rewrite Heq; clear Heq npe)). + +(* General scheme of reflexive tactics using of correctness lemma + that involves normalisation of one expression *) +Ltac ReflexiveRewriteTactic FV_tac SYN_tac SIMPL_tac lemma2 req rl := + let R := match type of req with ?R -> _ => R end in + (* build the atom list *) + let fv := list_fold_left FV_tac (@List.nil R) rl in + (* some type-checking to avoid late errors *) + (check_fv fv; + (* rewrite steps *) + list_iter + ltac:(fun r => + let ast := SYN_tac r fv in + try ApplyLemmaAndSimpl SIMPL_tac (lemma2 fv) ast) + rl). + +(********************************************************) + +(* An object to return when an expression is not recognized as a constant *) 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. +(* Building the atom list of a ring expression *) Ltac FV Cst add mul sub opp t fv := let rec TFV t fv := match Cst t with @@ -80,13 +77,13 @@ Ltac FV Cst add mul sub opp t 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 + | _ => AddFvTail t fv end | _ => fv - end + end in TFV t fv. - (* syntaxification *) + (* syntaxification of ring expressions *) Ltac mkPolexpr C Cst radd rmul rsub ropp t fv := let rec mkP t := match Cst t with @@ -111,644 +108,53 @@ Ltac FV Cst add mul sub opp t fv := 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. + Ltac Ring Cst_tac lemma1 req := + let Make_tac := + match type of lemma1 with + | forall (l:list ?R) (pe1 pe2:PExpr ?C), + _ = true -> + req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe1) _ => + let mkFV := FV Cst_tac add mul sub opp in + let mkPol := mkPolexpr C Cst_tac add mul sub opp in + fun f => f R mkFV mkPol + | _ => fail 1 "ring anomaly: bad correctness lemma" + end in + let Main r1 r2 R mkFV mkPol := + let fv := mkFV r1 (@List.nil R) in + let fv := mkFV r2 fv in + check_fv fv; + (let pe1 := mkPol r1 fv in + let pe2 := mkPol r2 fv in + apply (lemma1 fv pe1 pe2) || fail "typing error while applying ring"; + vm_compute; + exact (refl_equal true) || fail "not a valid ring equation") in + Make_tac ltac:(OnEquation req Main). + +Ltac Ring_simplify Cst_tac lemma2 req rl := + let Make_tac := + 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) _ => + let mkFV := FV Cst_tac add mul sub opp in + let mkPol := mkPolexpr C Cst_tac add mul sub opp in + let simpl_ring H := protect_fv "ring" in H in + (fun tac => tac mkFV mkPol simpl_ring lemma2 req rl) + | _ => fail 1 "ring anomaly: bad correctness lemma" + end in + Make_tac ReflexiveRewriteTactic. -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. +Tactic Notation (at level 0) "ring" := + ring_lookup + (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl => + pre(); Ring cst_tac lemma1 req). -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. +Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := + ring_lookup + (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl => + pre(); Ring_simplify cst_tac lemma2 req rl; post()) rl. -*) +(* A simple macro tactic to be prefered to ring_simplify *) +Ltac ring_replace t1 t2 := replace t1 with t2 by ring. |