summaryrefslogtreecommitdiff
path: root/contrib/setoid_ring/Ring_tac.v
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/setoid_ring/Ring_tac.v')
-rw-r--r--contrib/setoid_ring/Ring_tac.v794
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 19:00:55 +0000