diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/micromega/Lia.v | 11 | ||||
| -rw-r--r-- | theories/micromega/ZMicromega.v | 2 | ||||
| -rw-r--r-- | theories/micromega/Zify.v | 85 | ||||
| -rw-r--r-- | theories/micromega/ZifyClasses.v | 143 | ||||
| -rw-r--r-- | theories/micromega/ZifyInst.v | 114 | ||||
| -rw-r--r-- | theories/omega/PreOmega.v | 14 |
6 files changed, 157 insertions, 212 deletions
diff --git a/theories/micromega/Lia.v b/theories/micromega/Lia.v index e53800d07d..5d97fc46ef 100644 --- a/theories/micromega/Lia.v +++ b/theories/micromega/Lia.v @@ -14,11 +14,8 @@ (* *) (************************************************************************) -Require Import ZMicromega. -Require Import ZArith_base. -Require Import RingMicromega. -Require Import VarMap. -Require Import DeclConstant. +Require Import ZMicromega RingMicromega VarMap DeclConstant. +Require Import BinNums. Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". @@ -29,9 +26,9 @@ Ltac zchecker := (@eq_refl bool true <: @eq bool (ZTautoChecker __ff __wit) true) (@find Z Z0 __varmap)). -Ltac lia := PreOmega.zify; xlia zchecker. +Ltac lia := Zify.zify; xlia zchecker. -Ltac nia := PreOmega.zify; xnlia zchecker. +Ltac nia := Zify.zify; xnlia zchecker. (* Local Variables: *) diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v index 9bedb47371..38f3d3e0c0 100644 --- a/theories/micromega/ZMicromega.v +++ b/theories/micromega/ZMicromega.v @@ -1549,7 +1549,7 @@ Proof. apply H ; auto. unfold ltof in *. simpl in *. - PreOmega.zify. + Zify.zify. intuition subst. assumption. eapply Z.lt_le_trans. eassumption. apply Z.add_le_mono_r. assumption. diff --git a/theories/micromega/Zify.v b/theories/micromega/Zify.v index 18cd196148..494d5e5623 100644 --- a/theories/micromega/Zify.v +++ b/theories/micromega/Zify.v @@ -8,83 +8,16 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import ZifyClasses. -Require Export ZifyInst. -Require Import InitialRing. - -(** From PreOmega *) - -(** I) translation of Z.max, Z.min, Z.abs, Z.sgn into recognized equations *) - -Ltac zify_unop_core t thm a := - (* Let's introduce the specification theorem for t *) - pose proof (thm a); - (* Then we replace (t a) everywhere with a fresh variable *) - let z := fresh "z" in set (z:=t a) in *; clearbody z. - -Ltac zify_unop_var_or_term t thm a := - (* If a is a variable, no need for aliasing *) - let za := fresh "z" in - (rename a into za; rename za into a; zify_unop_core t thm a) || - (* Otherwise, a is a complex term: we alias it. *) - (remember a as za; zify_unop_core t thm za). - -Ltac zify_unop t thm a := - (* If a is a scalar, we can simply reduce the unop. *) - (* Note that simpl wasn't enough to reduce [Z.max 0 0] (#5439) *) - let isz := isZcst a in - match isz with - | true => - let u := eval compute in (t a) in - change (t a) with u in * - | _ => zify_unop_var_or_term t thm a - end. - -Ltac zify_unop_nored t thm a := - (* in this version, we don't try to reduce the unop (that can be (Z.add x)) *) - let isz := isZcst a in - match isz with - | true => zify_unop_core t thm a - | _ => zify_unop_var_or_term t thm a - end. - -Ltac zify_binop t thm a b:= - (* works as zify_unop, except that we should be careful when - dealing with b, since it can be equal to a *) - let isza := isZcst a in - match isza with - | true => zify_unop (t a) (thm a) b - | _ => - let za := fresh "z" in - (rename a into za; rename za into a; zify_unop_nored (t a) (thm a) b) || - (remember a as za; match goal with - | H : za = b |- _ => zify_unop_nored (t za) (thm za) za - | _ => zify_unop_nored (t za) (thm za) b - end) - end. - -(* end from PreOmega *) - -Ltac applySpec S := - let t := type of S in - match t with - | @BinOpSpec _ _ ?Op _ => - let Spec := (eval unfold S, BSpec in (@BSpec _ _ Op _ S)) in - repeat - match goal with - | H : context[Op ?X ?Y] |- _ => zify_binop Op Spec X Y - | |- context[Op ?X ?Y] => zify_binop Op Spec X Y - end - | @UnOpSpec _ _ ?Op _ => - let Spec := (eval unfold S, USpec in (@USpec _ _ Op _ S)) in - repeat - match goal with - | H : context[Op ?X] |- _ => zify_unop Op Spec X - | |- context[Op ?X ] => zify_unop Op Spec X - end - end. +Require Import ZifyClasses ZifyInst. +Declare ML Module "zify_plugin". (** [zify_post_hook] is there to be redefined. *) Ltac zify_post_hook := idtac. -Ltac zify := zify_op ; (zify_iter_specs applySpec) ; zify_post_hook. +Ltac iter_specs := zify_iter_specs. + +Ltac zify := intros; + zify_elim_let ; + zify_op ; + (zify_iter_specs) ; + zify_saturate ; zify_post_hook. diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v index d3f7f91074..988205a891 100644 --- a/theories/micromega/ZifyClasses.v +++ b/theories/micromega/ZifyClasses.v @@ -73,6 +73,7 @@ Class BinRel {S:Type} {T:Type} (R : S -> S -> Prop) {I : InjTyp S T} := (** [PropOp Op] declares morphisms for [<->]. This will be used to deal with e.g. [and], [or],... *) + Class PropOp (Op : Prop -> Prop -> Prop) := mkprop { op_iff : forall (p1 p2 q1 q2:Prop), (p1 <-> q1) -> (p2 <-> q2) -> (Op p1 p2 <-> Op q1 q2) @@ -80,7 +81,7 @@ Class PropOp (Op : Prop -> Prop -> Prop) := Class PropUOp (Op : Prop -> Prop) := mkuprop { - uop_iff : forall (p1 q1 :Prop), (p1 <-> q1) -> (Op p1 <-> Op q1) + uop_iff : forall (p1 q1 :Prop), (p1 <-> q1) -> (Op p1 <-> Op q1) }. @@ -131,7 +132,7 @@ Class Saturate {T: Type} (Op : T -> T -> T) := are used to store source and target expressions together with a correctness proof. *) -Record injterm {S T: Type} {I : S -> T} := +Record injterm {S T: Type} (I : S -> T) := mkinjterm { source : S ; target : T ; inj_ok : I source = target}. Record injprop := @@ -139,82 +140,104 @@ Record injprop := source_prop : Prop ; target_prop : Prop ; injprop_ok : source_prop <-> target_prop}. -(** Lemmas for building [injterm] and [injprop]. *) -Definition mkprop_op (Op : Prop -> Prop -> Prop) (POp : PropOp Op) - (p1 :injprop) (p2: injprop) : injprop := - {| source_prop := (Op (source_prop p1) (source_prop p2)) ; - target_prop := (Op (target_prop p1) (target_prop p2)) ; - injprop_ok := (op_iff (source_prop p1) (source_prop p2) (target_prop p1) (target_prop p2) - (injprop_ok p1) (injprop_ok p2)) - |}. -Definition mkuprop_op (Op : Prop -> Prop) (POp : PropUOp Op) - (p1 :injprop) : injprop := - {| source_prop := (Op (source_prop p1)) ; - target_prop := (Op (target_prop p1)) ; - injprop_ok := (uop_iff (source_prop p1) (target_prop p1) (injprop_ok p1)) - |}. +(** Lemmas for building rewrite rules. *) + +Definition PropOp_iff (Op : Prop -> Prop -> Prop) := + forall (p1 p2 q1 q2:Prop), (p1 <-> q1) -> (p2 <-> q2) -> (Op p1 p2 <-> Op q1 q2). + +Definition PropUOp_iff (Op : Prop -> Prop) := + forall (p1 q1 :Prop), (p1 <-> q1) -> (Op p1 <-> Op q1). Lemma mkapp2 (S1 S2 S3 T : Type) (Op : S1 -> S2 -> S3) - {I1 : InjTyp S1 T} {I2 : InjTyp S2 T} {I3 : InjTyp S3 T} - (B : @BinOp S1 S2 S3 T Op I1 I2 I3) - (t1 : @injterm S1 T inj) (t2 : @injterm S2 T inj) - : @injterm S3 T inj. + (I1 : S1 -> T) (I2 : S2 -> T) (I3 : S3 -> T) + (TBOP : T -> T -> T) + (TBOPINJ : forall n m, I3 (Op n m) = TBOP (I1 n) (I2 m)) + (s1 : S1) (t1 : T) (P1: I1 s1 = t1) + (s2 : S2) (t2 : T) (P2: I2 s2 = t2): I3 (Op s1 s2) = TBOP t1 t2. Proof. - apply (mkinjterm _ _ inj (Op (source t1) (source t2)) (TBOp (target t1) (target t2))). - (rewrite <- inj_ok; - rewrite <- inj_ok; - apply TBOpInj). -Defined. + subst. apply TBOPINJ. +Qed. -Lemma mkapp (S1 S2 T : Type) (Op : S1 -> S2) - {I1 : InjTyp S1 T} - {I2 : InjTyp S2 T} - (B : @UnOp S1 S2 T Op I1 I2 ) - (t1 : @injterm S1 T inj) - : @injterm S2 T inj. +Lemma mkapp (S1 S2 T : Type) (OP : S1 -> S2) + (I1 : S1 -> T) + (I2 : S2 -> T) + (TUOP : T -> T) + (TUOPINJ : forall n, I2 (OP n) = TUOP (I1 n)) + (s1: S1) (t1: T) (P1: I1 s1 = t1): I2 (OP s1) = TUOP t1. Proof. - apply (mkinjterm _ _ inj (Op (source t1)) (TUOp (target t1))). - (rewrite <- inj_ok; apply TUOpInj). -Defined. + subst. apply TUOPINJ. +Qed. + +Lemma mkrel (S T : Type) (R : S -> S -> Prop) + (I : S -> T) + (TR : T -> T -> Prop) + (TRINJ : forall n m : S, R n m <-> TR (I n) (I m)) + (s1 : S) (t1 : T) (P1 : I s1 = t1) + (s2 : S) (t2 : T) (P2 : I s2 = t2): + R s1 s2 <-> TR t1 t2. +Proof. + subst. + apply TRINJ. +Qed. + +(** Hardcoded support and lemma for propositional logic *) -Lemma mkapp0 (S T : Type) (Op : S) - {I : InjTyp S T} - (B : @CstOp S T Op I) - : @injterm S T inj. +Lemma and_morph : forall (s1 s2 t1 t2:Prop), s1 <-> t1 -> s2 <-> t2 -> ((s1 /\ s2) <-> (t1 /\ t2)). Proof. - apply (mkinjterm _ _ inj Op TCst). - (apply TCstInj). -Defined. + intros. tauto. +Qed. -Lemma mkrel (S T : Type) (R : S -> S -> Prop) - {Inj : InjTyp S T} - (B : @BinRel S T R Inj) - (t1 : @injterm S T inj) (t2 : @injterm S T inj) - : @injprop. +Lemma or_morph : forall (s1 s2 t1 t2:Prop), s1 <-> t1 -> s2 <-> t2 -> ((s1 \/ s2) <-> (t1 \/ t2)). +Proof. + intros. tauto. +Qed. + +Lemma impl_morph : forall (s1 s2 t1 t2:Prop), s1 <-> t1 -> s2 <-> t2 -> ((s1 -> s2) <-> (t1 -> t2)). +Proof. + intros. tauto. +Qed. + +Lemma iff_morph : forall (s1 s2 t1 t2:Prop), s1 <-> t1 -> s2 <-> t2 -> ((s1 <-> s2) <-> (t1 <-> t2)). +Proof. + intros. tauto. +Qed. + +Lemma not_morph : forall (s1 t1:Prop), s1 <-> t1 -> (not s1) <-> (not t1). +Proof. + intros. tauto. +Qed. + +Lemma eq_iff : forall (P Q : Prop), P = Q -> (P <-> Q). Proof. - apply (mkinjprop (R (source t1) (source t2)) (TR (target t1) (target t2))). - (rewrite <- inj_ok; rewrite <- inj_ok;apply TRInj). + intros. + rewrite H. + apply iff_refl. Defined. +Lemma rew_iff (P Q : Prop) (IFF : P <-> Q) : P -> Q. +Proof. + exact (fun H => proj1 IFF H). +Qed. + +Definition identity (A : Type) : A -> A := fun x => x. + (** Registering constants for use by the plugin *) +Register eq_iff as ZifyClasses.eq_iff. Register target_prop as ZifyClasses.target_prop. Register mkrel as ZifyClasses.mkrel. Register target as ZifyClasses.target. Register mkapp2 as ZifyClasses.mkapp2. Register mkapp as ZifyClasses.mkapp. -Register mkapp0 as ZifyClasses.mkapp0. Register op_iff as ZifyClasses.op_iff. Register uop_iff as ZifyClasses.uop_iff. Register TR as ZifyClasses.TR. Register TBOp as ZifyClasses.TBOp. Register TUOp as ZifyClasses.TUOp. Register TCst as ZifyClasses.TCst. -Register mkprop_op as ZifyClasses.mkprop_op. -Register mkuprop_op as ZifyClasses.mkuprop_op. Register injprop_ok as ZifyClasses.injprop_ok. Register inj_ok as ZifyClasses.inj_ok. Register source as ZifyClasses.source. @@ -225,8 +248,26 @@ Register TUOpInj as ZifyClasses.TUOpInj. Register not as ZifyClasses.not. Register mkinjterm as ZifyClasses.mkinjterm. Register eq_refl as ZifyClasses.eq_refl. +Register eq as ZifyClasses.eq. Register mkinjprop as ZifyClasses.mkinjprop. Register iff_refl as ZifyClasses.iff_refl. +Register rew_iff as ZifyClasses.rew_iff. Register source_prop as ZifyClasses.source_prop. Register injprop_ok as ZifyClasses.injprop_ok. Register iff as ZifyClasses.iff. +Register BinOpSpec as ZifyClasses.BinOpSpec. +Register UnOpSpec as ZifyClasses.UnOpSpec. + +(** Propositional logic *) +Register and as ZifyClasses.and. +Register and_morph as ZifyClasses.and_morph. +Register or as ZifyClasses.or. +Register or_morph as ZifyClasses.or_morph. +Register iff as ZifyClasses.iff. +Register iff_morph as ZifyClasses.iff_morph. +Register impl_morph as ZifyClasses.impl_morph. +Register not as ZifyClasses.not. +Register not_morph as ZifyClasses.not_morph. + +(** Identify function *) +Register identity as ZifyClasses.identity. diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v index edfb5a2a94..fa486f3abc 100644 --- a/theories/micromega/ZifyInst.v +++ b/theories/micromega/ZifyInst.v @@ -17,44 +17,10 @@ Require Import ZifyClasses. Declare ML Module "zify_plugin". Local Open Scope Z_scope. -(** Propositional logic *) -Instance PropAnd : PropOp and. -Proof. - constructor. - tauto. -Defined. -Add PropOp PropAnd. - -Instance PropOr : PropOp or. -Proof. - constructor. - tauto. -Defined. -Add PropOp PropOr. - -Instance PropArrow : PropOp (fun x y => x -> y). -Proof. - constructor. - intros. - tauto. -Defined. -Add PropOp PropArrow. - -Instance PropIff : PropOp iff. -Proof. - constructor. - intros. - tauto. -Defined. -Add PropOp PropIff. - -Instance PropNot : PropUOp not. -Proof. - constructor. - intros. - tauto. -Defined. -Add PropUOp PropNot. +Ltac refl := + abstract (intros ; match goal with + | |- context[@inj _ _ ?X] => unfold X, inj + end ; reflexivity). Instance Inj_Z_Z : InjTyp Z Z := @@ -162,13 +128,18 @@ Instance Op_pos_le : BinRel Pos.le := {| TR := Z.le; TRInj := fun x y => iff_refl (Z.pos x <= Z.pos y) |}. Add BinRel Op_pos_le. +Lemma eq_pos_inj : forall (x y:positive), x = y <-> Z.pos x = Z.pos y. +Proof. + intros. + apply (iff_sym (Pos2Z.inj_iff x y)). +Qed. + Instance Op_eq_pos : BinRel (@eq positive) := - {| TR := @eq Z ; TRInj := fun x y => iff_sym (Pos2Z.inj_iff x y) |}. + { TR := @eq Z ; TRInj := eq_pos_inj }. Add BinRel Op_eq_pos. (* zify_positive_op *) - Instance Op_Z_of_N : UnOp Z.of_N := { TUOp := (fun x => x) ; TUOpInj := fun x => eq_refl (Z.of_N x) }. Add UnOp Op_Z_of_N. @@ -189,8 +160,11 @@ Instance Op_pos_succ : UnOp Pos.succ := { TUOp := fun x => x + 1; TUOpInj := Pos2Z.inj_succ }. Add UnOp Op_pos_succ. + + + Instance Op_pos_pred_double : UnOp Pos.pred_double := - { TUOp := fun x => 2 * x - 1; TUOpInj := ltac:(reflexivity) }. +{ TUOp := fun x => 2 * x - 1; TUOpInj := ltac:(refl) }. Add UnOp Op_pos_pred_double. Instance Op_pos_pred : UnOp Pos.pred := @@ -217,7 +191,7 @@ Instance Op_pos_of_nat : UnOp Pos.of_nat := Add UnOp Op_pos_of_nat. Instance Op_pos_add : BinOp Pos.add := - { TBOp := Z.add ; TBOpInj := ltac: (reflexivity) }. + { TBOp := Z.add ; TBOpInj := ltac: (refl) }. Add BinOp Op_pos_add. Instance Op_pos_add_carry : BinOp Pos.add_carry := @@ -230,7 +204,7 @@ Instance Op_pos_sub : BinOp Pos.sub := Add BinOp Op_pos_sub. Instance Op_pos_mul : BinOp Pos.mul := - { TBOp := Z.mul ; TBOpInj := ltac: (reflexivity) }. + { TBOp := Z.mul ; TBOpInj := ltac: (refl) }. Add BinOp Op_pos_mul. Instance Op_pos_min : BinOp Pos.min := @@ -250,19 +224,19 @@ Instance Op_pos_square : UnOp Pos.square := Add UnOp Op_pos_square. Instance Op_xO : UnOp xO := - { TUOp := fun x => 2 * x ; TUOpInj := ltac: (reflexivity) }. + { TUOp := fun x => 2 * x ; TUOpInj := ltac: (refl) }. Add UnOp Op_xO. Instance Op_xI : UnOp xI := - { TUOp := fun x => 2 * x + 1 ; TUOpInj := ltac: (reflexivity) }. + { TUOp := fun x => 2 * x + 1 ; TUOpInj := ltac: (refl) }. Add UnOp Op_xI. Instance Op_xH : CstOp xH := - { TCst := 1%Z ; TCstInj := ltac:(reflexivity)}. + { TCst := 1%Z ; TCstInj := ltac:(refl)}. Add CstOp Op_xH. Instance Op_Z_of_nat : UnOp Z.of_nat:= - { TUOp := fun x => x ; TUOpInj := ltac:(reflexivity) }. + { TUOp := fun x => x ; TUOpInj := (fun x : nat => @eq_refl Z (Z.of_nat x)) }. Add UnOp Op_Z_of_nat. (* zify_N_rel *) @@ -287,6 +261,14 @@ Instance Op_eq_N : BinRel (@eq N) := Add BinRel Op_eq_N. (* zify_N_op *) +Instance Op_N_N0 : CstOp N0 := + { TCst := Z0 ; TCstInj := eq_refl }. +Add CstOp Op_N_N0. + +Instance Op_N_Npos : UnOp Npos := + { TUOp := (fun x => x) ; TUOpInj := ltac:(refl) }. +Add UnOp Op_N_Npos. + Instance Op_N_of_nat : UnOp N.of_nat := { TUOp := fun x => x ; TUOpInj := nat_N_Z }. Add UnOp Op_N_of_nat. @@ -296,7 +278,7 @@ Instance Op_Z_abs_N : UnOp Z.abs_N := Add UnOp Op_Z_abs_N. Instance Op_N_pos : UnOp N.pos := - { TUOp := fun x => x ; TUOpInj := ltac:(reflexivity)}. + { TUOp := fun x => x ; TUOpInj := ltac:(refl)}. Add UnOp Op_N_pos. Instance Op_N_add : BinOp N.add := @@ -360,68 +342,72 @@ Instance Op_eqZ : BinRel (@eq Z) := { TR := @eq Z ; TRInj := fun x y => iff_refl (x = y) }. Add BinRel Op_eqZ. +Instance Op_Z_Z0 : CstOp Z0 := + { TCst := Z0 ; TCstInj := eq_refl }. +Add CstOp Op_Z_Z0. + Instance Op_Z_add : BinOp Z.add := - { TBOp := Z.add ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.add ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_add. Instance Op_Z_min : BinOp Z.min := - { TBOp := Z.min ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.min ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_min. Instance Op_Z_max : BinOp Z.max := - { TBOp := Z.max ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.max ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_max. Instance Op_Z_mul : BinOp Z.mul := - { TBOp := Z.mul ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.mul ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_mul. Instance Op_Z_sub : BinOp Z.sub := - { TBOp := Z.sub ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.sub ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_sub. Instance Op_Z_div : BinOp Z.div := - { TBOp := Z.div ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.div ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_div. Instance Op_Z_mod : BinOp Z.modulo := - { TBOp := Z.modulo ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.modulo ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_mod. Instance Op_Z_rem : BinOp Z.rem := - { TBOp := Z.rem ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.rem ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_rem. Instance Op_Z_quot : BinOp Z.quot := - { TBOp := Z.quot ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.quot ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_quot. Instance Op_Z_succ : UnOp Z.succ := - { TUOp := fun x => x + 1 ; TUOpInj := ltac:(reflexivity) }. + { TUOp := fun x => x + 1 ; TUOpInj := ltac:(refl) }. Add UnOp Op_Z_succ. Instance Op_Z_pred : UnOp Z.pred := - { TUOp := fun x => x - 1 ; TUOpInj := ltac:(reflexivity) }. + { TUOp := fun x => x - 1 ; TUOpInj := ltac:(refl) }. Add UnOp Op_Z_pred. Instance Op_Z_opp : UnOp Z.opp := - { TUOp := Z.opp ; TUOpInj := ltac:(reflexivity) }. + { TUOp := Z.opp ; TUOpInj := ltac:(refl) }. Add UnOp Op_Z_opp. Instance Op_Z_abs : UnOp Z.abs := - { TUOp := Z.abs ; TUOpInj := ltac:(reflexivity) }. + { TUOp := Z.abs ; TUOpInj := ltac:(refl) }. Add UnOp Op_Z_abs. Instance Op_Z_sgn : UnOp Z.sgn := - { TUOp := Z.sgn ; TUOpInj := ltac:(reflexivity) }. + { TUOp := Z.sgn ; TUOpInj := ltac:(refl) }. Add UnOp Op_Z_sgn. Instance Op_Z_pow : BinOp Z.pow := - { TBOp := Z.pow ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.pow ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_pow. Instance Op_Z_pow_pos : BinOp Z.pow_pos := - { TBOp := Z.pow ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.pow ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_pow_pos. Instance Op_Z_double : UnOp Z.double := diff --git a/theories/omega/PreOmega.v b/theories/omega/PreOmega.v index 34533670f8..bd9caa801c 100644 --- a/theories/omega/PreOmega.v +++ b/theories/omega/PreOmega.v @@ -573,16 +573,4 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. Require Import ZifyClasses ZifyInst. Require Zify. -(* [elim_let] replaces a let binding (x := e : t) - by an equation (x = e) if t is an injected type *) - -Ltac elim_binding x t ty := - let h := fresh "heq_" x in - pose proof (@eq_refl ty x : @eq ty x t) as h; - try clearbody x. - -Ltac elim_let := zify_iter_let elim_binding. - -Ltac zify := - intros ; elim_let ; - Zify.zify ; ZifyInst.zify_saturate. +Ltac zify := Zify.zify. |