diff options
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 5 | ||||
| -rw-r--r-- | plugins/micromega/zify.ml | 25 | ||||
| -rw-r--r-- | test-suite/micromega/bug_11089.v | 13 | ||||
| -rw-r--r-- | test-suite/micromega/zify.v | 7 | ||||
| -rw-r--r-- | theories/micromega/ZifyClasses.v | 9 |
5 files changed, 52 insertions, 7 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index d718454364..24e35dd85a 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -295,7 +295,7 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands. The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``. -.. cmd:: Add Zify @add_zify @one_term +.. cmd:: Add Zify @add_zify @qualid .. insertprodn add_zify add_zify @@ -304,6 +304,9 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. | {| PropOp | PropBinOp | PropUOp | Saturate } Registers an instance of the specified typeclass. + The typeclass type (e.g. :g:`BinOp Z.mul` or :g:`BinRel (@eq Z)`) has the additional constraint that + the non-implicit argument (here, :g:`Z.mul` or :g:`(@eq Z)`) + is either a :n:`@reference` (here, :g:`Z.mul`) or the application of a :n:`@reference` (here, :g:`@eq`) to a sequence of :n:`@one_term`. .. cmd:: Show Zify @show_zify diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index b780c1833e..3ea7408067 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -46,6 +46,7 @@ let mkrel = lazy (zify "mkrel") let iff_refl = lazy (zify "iff_refl") let eq_iff = lazy (zify "eq_iff") let rew_iff = lazy (zify "rew_iff") +let rew_iff_rev = lazy (zify "rew_iff_rev") (* propositional logic *) @@ -621,14 +622,20 @@ module MakeTable (E : Elt) = struct failwith ("Cannot register term " ^ t) | Some a -> E.mk_elt evd i a + let safe_ref evd c = + try + fst (EConstr.destRef evd c) + with DestKO -> CErrors.user_err Pp.(str "Add Zify "++str E.name ++ str ": the term "++ + gl_pr_constr c ++ str " should be a global reference") + let register_hint evd t elt = match EConstr.kind evd t with | App (c, _) -> - let gr = fst (EConstr.destRef evd c) in - E.table := ConstrMap.add gr (Application t, E.cast elt) !E.table + let gr = safe_ref evd c in + E.table := ConstrMap.add gr (Application t, E.cast elt) !E.table | _ -> - let gr = fst (EConstr.destRef evd t) in - E.table := ConstrMap.add gr (OtherTerm t, E.cast elt) !E.table + let gr = safe_ref evd t in + E.table := ConstrMap.add gr (OtherTerm t, E.cast elt) !E.table let register_constr env evd c = let c = EConstr.of_constr c in @@ -1365,7 +1372,15 @@ let trans_concl prfp = Tactics.change_concl t') | TProof (t, prf) -> Proofview.Goal.enter (fun gl -> - Equality.general_rewrite true Locus.AllOccurrences true false prf) + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + let typ = get_type_of env evd prf in + match EConstr.kind evd typ with + | App (c, a) when Array.length a = 2 -> + Tactics.apply + (EConstr.mkApp (Lazy.force rew_iff_rev, [|a.(0); a.(1); prf|])) + | _ -> + raise (CErrors.anomaly Pp.(str "zify cannot transform conclusion"))) let tclTHENOpt e tac tac' = match e with None -> tac' | Some e' -> Tacticals.New.tclTHEN (tac e') tac' diff --git a/test-suite/micromega/bug_11089.v b/test-suite/micromega/bug_11089.v new file mode 100644 index 0000000000..e62b5b8d9e --- /dev/null +++ b/test-suite/micromega/bug_11089.v @@ -0,0 +1,13 @@ +Require Import Lia. +Unset Lia Cache. +Definition t := nat. +Goal forall (n : t), n = n. +Proof. + intros. + lia. +Qed. +Goal let t' := nat in forall (n : t'), n = n. +Proof. + intros. + lia. +Qed. diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v index a12623c3c0..2ea320047d 100644 --- a/test-suite/micromega/zify.v +++ b/test-suite/micromega/zify.v @@ -167,6 +167,12 @@ Goal @zero znat = 0%nat. reflexivity. Qed. +Require Import ZifyBool. +Instance Op_bool_inj : UnOp (inj : bool -> bool) := + { TUOp := id; TUOpInj := fun _ => eq_refl }. +Add Zify UnOp Op_bool_inj. + + Goal forall (x y : positive) (F : forall (P: Pos.le x y) , positive) (P : Pos.le x y), (F P + 1 = 1 + F P)%positive. Proof. @@ -228,6 +234,7 @@ Proof. intros. lia. Qed. + Ltac Zify.zify_pre_hook ::= unfold is_true in *. Goal forall x y : nat, is_true (Nat.eqb x 1) -> diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v index 019d11d951..25d9fa9104 100644 --- a/theories/micromega/ZifyClasses.v +++ b/theories/micromega/ZifyClasses.v @@ -7,7 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Set Primitive Projections. (** An alternative to [zify] in ML parametrised by user-provided classes instances. @@ -220,6 +219,13 @@ Proof. exact (fun H => proj1 IFF H). Qed. +Lemma rew_iff_rev (P Q : Prop) (IFF : P <-> Q) : Q -> P. +Proof. + exact (fun H => proj2 IFF H). +Qed. + + + (** Registering constants for use by the plugin *) Register eq_iff as ZifyClasses.eq_iff. Register target_prop as ZifyClasses.target_prop. @@ -247,6 +253,7 @@ 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 rew_iff_rev as ZifyClasses.rew_iff_rev. Register source_prop as ZifyClasses.source_prop. Register injprop_ok as ZifyClasses.injprop_ok. Register iff as ZifyClasses.iff. |