aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore1
-rwxr-xr-xdev/ci/ci-basic-overlay.sh2
-rw-r--r--doc/changelog/04-tactics/12552-zify-pre-hook.rst4
-rw-r--r--doc/sphinx/addendum/micromega.rst3
-rw-r--r--engine/evd.ml31
-rw-r--r--pretyping/glob_ops.ml2
-rw-r--r--tactics/autorewrite.ml69
-rw-r--r--tactics/autorewrite.mli19
-rw-r--r--test-suite/bugs/closed/bug_12529.v21
-rw-r--r--test-suite/micromega/zify.v11
-rw-r--r--test-suite/output-coqtop/DependentEvars.out6
-rw-r--r--test-suite/output-coqtop/DependentEvars2.out12
-rw-r--r--test-suite/output/unification.out24
-rw-r--r--test-suite/output/unification.v26
-rw-r--r--theories/Reals/RIneq.v22
-rw-r--r--theories/micromega/Zify.v5
16 files changed, 170 insertions, 88 deletions
diff --git a/.gitignore b/.gitignore
index 0c7a8f70f6..557655317c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -92,6 +92,7 @@ test-suite/coqdoc/coqdoc.css
test-suite/output/MExtraction.out
test-suite/output/*.out.real
test-suite/oUnit-anon.cache
+test-suite/redirect_test.out
test-suite/unit-tests/**/*.test
# documentation
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index cdf00f4767..475f812b5a 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -349,7 +349,7 @@
########################################################################
# perennial
########################################################################
-: "${perennial_CI_REF:=master}"
+: "${perennial_CI_REF:=coq/tested}"
: "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}"
: "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}"
diff --git a/doc/changelog/04-tactics/12552-zify-pre-hook.rst b/doc/changelog/04-tactics/12552-zify-pre-hook.rst
new file mode 100644
index 0000000000..975c917b19
--- /dev/null
+++ b/doc/changelog/04-tactics/12552-zify-pre-hook.rst
@@ -0,0 +1,4 @@
+- **Added:**
+ Thhe :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook`
+ tactic. (`#12552 <https://github.com/coq/coq/pull/12552>`_,
+ by Kazuhiko Sakaguchi).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index c4947e6b3a..c01e6a5aa6 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -278,7 +278,8 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
This tactic is internally called by :tacn:`lia` to support additional types e.g., :g:`nat`, :g:`positive` and :g:`N`.
By requiring the module ``ZifyBool``, the boolean type :g:`bool` and some comparison operators are also supported.
- :tacn:`zify` can also be extended by rebinding the tactic `Zify.zify_post_hook` that is run immediately after :tacn:`zify`.
+ :tacn:`zify` can also be extended by rebinding the tactics `Zify.zify_pre_hook` and `Zify.zify_post_hook` that are
+ respectively run in the first and the last steps of :tacn:`zify`.
+ To support :g:`Z.div` and :g:`Z.modulo`: ``Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations``.
+ To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``.
diff --git a/engine/evd.ml b/engine/evd.ml
index ff13676818..f0ee8ae68f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1174,12 +1174,34 @@ let meta_declare mv v ?(name=Anonymous) evd =
let metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas in
set_metas evd metas
+(* If the meta is defined then forget its name *)
+let meta_name evd mv =
+ try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
+
+let evar_source_of_meta mv evd =
+ match meta_name evd mv with
+ | Anonymous -> Loc.tag Evar_kinds.GoalEvar
+ | Name id -> Loc.tag @@ Evar_kinds.VarInstance id
+
+let use_meta_source evd mv v =
+ match Constr.kind v with
+ | Evar (evk,_) ->
+ let f = function
+ | None -> None
+ | Some evi as x ->
+ match evi.evar_source with
+ | None, Evar_kinds.GoalEvar -> Some { evi with evar_source = evar_source_of_meta mv evd }
+ | _ -> x in
+ { evd with undf_evars = EvMap.update evk f evd.undf_evars }
+ | _ -> evd
+
let meta_assign mv (v, pb) evd =
let modify _ = function
| Cltyp (na, ty) -> Clval (na, (mk_freelisted v, pb), ty)
| _ -> anomaly ~label:"meta_assign" (Pp.str "already defined.")
in
let metas = Metamap.modify mv modify evd.metas in
+ let evd = use_meta_source evd mv v in
set_metas evd metas
let meta_reassign mv (v, pb) evd =
@@ -1190,10 +1212,6 @@ let meta_reassign mv (v, pb) evd =
let metas = Metamap.modify mv modify evd.metas in
set_metas evd metas
-(* If the meta is defined then forget its name *)
-let meta_name evd mv =
- try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
-
let clear_metas evd = {evd with metas = Metamap.empty}
let meta_merge ?(with_univs = true) evd1 evd2 =
@@ -1217,11 +1235,6 @@ let retract_coercible_metas evd =
let metas = Metamap.Smart.mapi map evd.metas in
!mc, set_metas evd metas
-let evar_source_of_meta mv evd =
- match meta_name evd mv with
- | Anonymous -> Loc.tag Evar_kinds.GoalEvar
- | Name id -> Loc.tag @@ Evar_kinds.VarInstance id
-
let dependent_evar_ident ev evd =
let evi = find evd ev in
match evi.evar_source with
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index cb868e0480..342175a512 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -55,7 +55,7 @@ exception ComplexSort
let glob_sort_family = let open Sorts in function
| UAnonymous {rigid=true} -> InType
- | UNamed [GSProp,0] -> InProp
+ | UNamed [GSProp,0] -> InSProp
| UNamed [GProp,0] -> InProp
| UNamed [GSet,0] -> InSet
| _ -> raise ComplexSort
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index eaefa2947a..cc56de066d 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -212,60 +212,37 @@ let inHintRewrite : string * HintDN.t -> Libobject.obj =
~cache:cache_hintrewrite
~subst:(Some subst_hintrewrite)
-open Clenv
-
type hypinfo = {
- hyp_cl : clausenv;
- hyp_prf : constr;
- hyp_ty : types;
- hyp_car : constr;
- hyp_rel : constr;
- hyp_l2r : bool;
- hyp_left : constr;
- hyp_right : constr;
+ hyp_ty : EConstr.types;
+ hyp_pat : EConstr.constr;
}
-let decompose_applied_relation metas env sigma c ctype left2right =
+let decompose_applied_relation env sigma c ctype left2right =
let find_rel ty =
- let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,ty) in
- let eqclause =
- if metas then eqclause
- else fst (clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd))
- in
- let (equiv, args) = EConstr.decompose_app sigma (Clenv.clenv_type eqclause) in
- let rec split_last_two = function
- | [c1;c2] -> [],(c1, c2)
- | x::y::z ->
- let l,res = split_last_two (y::z) in x::l, res
- | _ -> raise Not_found
- in
- try
- let others,(c1,c2) = split_last_two args in
- let ty1, ty2 = Retyping.get_type_of env eqclause.evd c1, Retyping.get_type_of env eqclause.evd c2 in
- (* XXX: It looks like mk_clenv_from_env should be fixed instead? *)
- let open EConstr in
- let hyp_ty = Unsafe.to_constr ty in
- let hyp_car = Unsafe.to_constr ty1 in
- let hyp_prf = Unsafe.to_constr @@ Clenv.clenv_value eqclause in
- let hyp_rel = Unsafe.to_constr @@ mkApp (equiv, Array.of_list others) in
- let hyp_left = Unsafe.to_constr @@ c1 in
- let hyp_right = Unsafe.to_constr @@ c2 in
-(* if not (evd_convertible env eqclause.evd ty1 ty2) then None *)
-(* else *)
- Some { hyp_cl=eqclause; hyp_prf; hyp_ty; hyp_car; hyp_rel; hyp_l2r=left2right; hyp_left; hyp_right; }
- with Not_found -> None
+ (* FIXME: this is nonsense, we generate evars and then we drop the
+ corresponding evarmap. This sometimes works because [Term_dnet] performs
+ evar surgery via [Termops.filtering]. *)
+ let sigma, ty = Clenv.make_evar_clause env sigma ty in
+ let (_, args) = Termops.decompose_app_vect sigma ty.Clenv.cl_concl in
+ let len = Array.length args in
+ if 2 <= len then
+ let c1 = args.(len - 2) in
+ let c2 = args.(len - 1) in
+ Some (if left2right then c1 else c2)
+ else None
in
match find_rel ctype with
- | Some c -> Some c
+ | Some c -> Some { hyp_pat = c; hyp_ty = ctype }
| None ->
let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *)
- match find_rel (it_mkProd_or_LetIn t' ctx) with
- | Some c -> Some c
+ let ctype = it_mkProd_or_LetIn t' ctx in
+ match find_rel ctype with
+ | Some c -> Some { hyp_pat = c; hyp_ty = ctype }
| None -> None
-let find_applied_relation ?loc metas env sigma c left2right =
+let find_applied_relation ?loc env sigma c left2right =
let ctype = Retyping.get_type_of env sigma (EConstr.of_constr c) in
- match decompose_applied_relation metas env sigma c ctype left2right with
+ match decompose_applied_relation env sigma c ctype left2right with
| Some c -> c
| None ->
user_err ?loc ~hdr:"decompose_applied_relation"
@@ -283,9 +260,9 @@ let add_rew_rules base lrul =
List.fold_left
(fun dn {CAst.loc;v=((c,ctx),b,t)} ->
let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
- let info = find_applied_relation ?loc false env sigma c b in
- let pat = if b then info.hyp_left else info.hyp_right in
- let rul = { rew_lemma = c; rew_type = info.hyp_ty;
+ let info = find_applied_relation ?loc env sigma c b in
+ let pat = EConstr.Unsafe.to_constr info.hyp_pat in
+ let rul = { rew_lemma = c; rew_type = EConstr.Unsafe.to_constr info.hyp_ty;
rew_pat = pat; rew_ctx = ctx; rew_l2r = b;
rew_tac = Option.map intern t}
in incr counter;
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 8f7a1c8fcf..974aef8e8f 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -43,22 +43,3 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> uni
val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic
val print_rewrite_hintdb : string -> Pp.t
-
-open Clenv
-
-
-type hypinfo = {
- hyp_cl : clausenv;
- hyp_prf : constr;
- hyp_ty : types;
- hyp_car : constr;
- hyp_rel : constr;
- hyp_l2r : bool;
- hyp_left : constr;
- hyp_right : constr;
-}
-
-val find_applied_relation :
- ?loc:Loc.t -> bool ->
- Environ.env -> Evd.evar_map -> constr -> bool -> hypinfo
-
diff --git a/test-suite/bugs/closed/bug_12529.v b/test-suite/bugs/closed/bug_12529.v
new file mode 100644
index 0000000000..bc3c9a28bd
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12529.v
@@ -0,0 +1,21 @@
+Goal SProp.
+match goal with |- SProp => idtac end.
+Fail match goal with |- Prop => idtac end.
+Abort.
+
+Goal Prop.
+Fail match goal with |- SProp => idtac end.
+match goal with |- Prop => idtac end.
+Abort.
+
+Class F A := f : A.
+
+Inductive pFalse : Prop := .
+Inductive sFalse : SProp := .
+
+Hint Extern 0 (F Prop) => exact pFalse : typeclass_instances.
+Definition pf := f : Prop.
+
+Hint Extern 0 (F SProp) => exact sFalse : typeclass_instances.
+Definition sf := (f : SProp).
+Definition pf' := (f : Prop).
diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v
index 8fd7398638..a12623c3c0 100644
--- a/test-suite/micromega/zify.v
+++ b/test-suite/micromega/zify.v
@@ -159,7 +159,7 @@ Require Import ZifyClasses.
Require Import ZifyInst.
Instance Zero : CstOp (@zero znat : nat) := Op_O.
-Add CstOp Zero.
+Add Zify CstOp Zero.
Goal @zero znat = 0%nat.
@@ -227,3 +227,12 @@ Goal forall (f : Z -> bool), negb (negb (f 0)) = f 0.
Proof.
intros. lia.
Qed.
+
+Ltac Zify.zify_pre_hook ::= unfold is_true in *.
+
+Goal forall x y : nat, is_true (Nat.eqb x 1) ->
+ is_true (Nat.eqb y 0) ->
+ is_true (Nat.eqb (x + y) 1).
+Proof.
+lia.
+Qed.
diff --git a/test-suite/output-coqtop/DependentEvars.out b/test-suite/output-coqtop/DependentEvars.out
index 9ca3fa3357..2e69b94505 100644
--- a/test-suite/output-coqtop/DependentEvars.out
+++ b/test-suite/output-coqtop/DependentEvars.out
@@ -77,14 +77,14 @@ p14 < 3 focused subgoals
p123 : (P1 -> P2) -> P3
p34 : P3 -> P4
============================
- ?P -> (?Goal2 -> P4) /\ ?Goal2
+ ?P -> (?P0 -> P4) /\ ?P0
subgoal 2 is:
- ?P -> (?Goal2 -> P4) /\ ?Goal2
+ ?P -> (?P0 -> P4) /\ ?P0
subgoal 3 is:
?P
-(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal: ?X4 ?X5 ?X10 ?X11)
p14 <
Coq <
diff --git a/test-suite/output-coqtop/DependentEvars2.out b/test-suite/output-coqtop/DependentEvars2.out
index 29ebba7c86..63bfafa88d 100644
--- a/test-suite/output-coqtop/DependentEvars2.out
+++ b/test-suite/output-coqtop/DependentEvars2.out
@@ -90,13 +90,13 @@ Try unfocusing with "}".
(shelved: 2)
subgoal 1 is:
- ?P -> (?Goal2 -> P4) /\ ?Goal2
+ ?P -> (?P0 -> P4) /\ ?P0
subgoal 2 is:
- ?P -> (?Goal2 -> P4) /\ ?Goal2
+ ?P -> (?P0 -> P4) /\ ?P0
subgoal 3 is:
?P
-(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal:)
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal:)
p14 < 3 focused subgoals
(shelved: 2)
@@ -106,14 +106,14 @@ p14 < 3 focused subgoals
p123 : (P1 -> P2) -> P3
p34 : P3 -> P4
============================
- ?P -> (?Goal2 -> P4) /\ ?Goal2
+ ?P -> (?P0 -> P4) /\ ?P0
subgoal 2 is:
- ?P -> (?Goal2 -> P4) /\ ?Goal2
+ ?P -> (?P0 -> P4) /\ ?P0
subgoal 3 is:
?P
-(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal: ?X4 ?X5 ?X10 ?X11)
p14 <
Coq <
diff --git a/test-suite/output/unification.out b/test-suite/output/unification.out
index dfd755da61..cf31871e5a 100644
--- a/test-suite/output/unification.out
+++ b/test-suite/output/unification.out
@@ -9,3 +9,27 @@ Unable to unify "T" with "?X@{x0:=x; x:=C a}" (cannot instantiate
The command has indeed failed with message:
The term "id" has type "ID" while it is expected to have type
"Type -> ?T" (cannot instantiate "?T" because "A" is not in its scope).
+1 focused subgoal
+(shelved: 1)
+
+ H : forall x : nat, S (S (S x)) = x
+ ============================
+ ?x = 0
+1 focused subgoal
+(shelved: 1)
+
+ H : forall x : nat, S (S (S x)) = x
+ ============================
+ ?x = 0
+1 focused subgoal
+(shelved: 1)
+
+ H : forall x : nat, S (S (S x)) = x
+ ============================
+ ?x = 0
+1 focused subgoal
+(shelved: 1)
+
+ H : forall x : nat, S x = x
+ ============================
+ ?y = 0
diff --git a/test-suite/output/unification.v b/test-suite/output/unification.v
index ff99f2e23c..fe7366a97d 100644
--- a/test-suite/output/unification.v
+++ b/test-suite/output/unification.v
@@ -10,3 +10,29 @@ Fail Check fun x => match x return ?[X] with C a => a end.
Fail Check (id:Type -> _).
End A.
+
+(* Choice of evar names *)
+
+Goal (forall x, S (S (S x)) = x) -> exists x, S x = 0.
+eexists.
+rewrite H.
+Show.
+Undo 2.
+eexists ?[x].
+rewrite H.
+Show.
+Undo 2.
+eexists ?[y].
+rewrite H.
+Show.
+reflexivity.
+Qed.
+
+(* Preserve the name if there is one *)
+
+Goal (forall x, S x = x) -> exists x, S x = 0.
+eexists ?[y].
+rewrite H.
+Show.
+reflexivity.
+Qed.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 33e40a115b..4fa8b3216a 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1774,6 +1774,28 @@ Proof.
now rewrite <- INR_IPR, SuccNat2Pos.id_succ.
Qed.
+Lemma IZR_NEG : forall p, IZR (Zneg p) = Ropp (IZR (Zpos p)).
+Proof.
+ reflexivity.
+Qed.
+
+(** The three following lemmas map the default form of numerical
+ constants to their representation in terms of the axioms of
+ [R]. This can be a useful intermediate representation for reifying
+ to another axiomatics of the reals. It is however generally more
+ convenient to keep constants represented under an [IZR z] form when
+ working within [R]. *)
+
+Lemma IZR_POS_xO : forall p, IZR (Zpos (xO p)) = (1+1) * (IZR (Zpos p)).
+Proof.
+ intro. unfold IZR, IPR. destruct p; simpl; trivial. rewrite Rmult_1_r. trivial.
+Qed.
+
+Lemma IZR_POS_xI : forall p, IZR (Zpos (xI p)) = 1 + (1+1) * IZR (Zpos p).
+Proof.
+ intro. unfold IZR, IPR. destruct p; simpl; trivial. rewrite Rmult_1_r. trivial.
+Qed.
+
Lemma plus_IZR_NEG_POS :
forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q).
Proof.
diff --git a/theories/micromega/Zify.v b/theories/micromega/Zify.v
index 2df3c57d32..183fd6a914 100644
--- a/theories/micromega/Zify.v
+++ b/theories/micromega/Zify.v
@@ -11,12 +11,15 @@
Require Import ZifyClasses ZifyInst.
Declare ML Module "zify_plugin".
-(** [zify_post_hook] is there to be redefined. *)
+(** [zify_pre_hook] and [zify_post_hook] are there to be redefined. *)
+Ltac zify_pre_hook := idtac.
+
Ltac zify_post_hook := idtac.
Ltac iter_specs := zify_iter_specs.
Ltac zify := intros;
+ zify_pre_hook ;
zify_elim_let ;
zify_op ;
(zify_iter_specs) ;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 12:07:47 +0000