aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ssr/ssrcommon.ml9
-rw-r--r--plugins/ssr/ssrcommon.mli3
-rw-r--r--plugins/ssr/ssreflect.v42
-rw-r--r--plugins/ssr/ssrequality.ml4
-rw-r--r--plugins/ssr/ssrfwd.ml13
5 files changed, 65 insertions, 6 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 0b3bfab366..a05b1e3d81 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -828,10 +828,12 @@ let view_error s gv =
open Locus
(****************************** tactics ***********************************)
-let rewritetac dir c =
+let rewritetac ?(under=false) dir c =
(* Due to the new optional arg ?tac, application shouldn't be too partial *)
+ let open Proofview.Notations in
Proofview.V82.of_tactic begin
- Equality.general_rewrite (dir = L2R) AllOccurrences true false c
+ Equality.general_rewrite (dir = L2R) AllOccurrences true false c <*>
+ if under then Proofview.cycle 1 else Proofview.tclUNIT ()
end
(**********************`:********* hooks ************************************)
@@ -1542,6 +1544,7 @@ end
let is_construct_ref sigma c r =
EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r
let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r
-
+let is_const_ref sigma c r =
+ EConstr.isConst sigma c && GlobRef.equal (ConstRef (fst(EConstr.destConst sigma c))) r
(* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 3049f67f87..58ce84ecb3 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -349,7 +349,7 @@ val resolve_typeclasses :
(*********************** Wrapped Coq tactics *****************************)
-val rewritetac : ssrdir -> EConstr.t -> tactic
+val rewritetac : ?under:bool -> ssrdir -> EConstr.t -> tactic
type name_hint = (int * EConstr.types array) option ref
@@ -486,3 +486,4 @@ end
val is_ind_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
val is_construct_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
+val is_const_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 37390e1af7..94e0b2a724 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -550,7 +550,49 @@ End Under.
Register Under as plugins.ssreflect.Under.
Register Under_from_eq as plugins.ssreflect.Under_from_eq.
+Module Type UNDER_IFF.
+Parameter Under_iff : Prop -> Prop -> Prop.
+Parameter Under_from_iff : forall x y : Prop, @Under_iff x y -> x <-> y.
+
+(** [Over_iff, over_iff, over_iff_done]: for "by rewrite over_iff" *)
+Parameter Over_iff : Prop -> Prop -> Prop.
+Parameter over_iff :
+ forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y.
+Parameter over_iff_done :
+ forall (x : Prop), @Over_iff x x.
+Hint Extern 0 (@Over_iff _ _) => solve [ apply over_iff_done ] : core.
+Hint Resolve over_iff_done : core.
+
+(** [under_iff_done]: for Ltac-style over *)
+Parameter under_iff_done :
+ forall (x : Prop), @Under_iff x x.
+Notation "''Under_iff[' x ]" := (@Under_iff x _)
+ (at level 8, format "''Under_iff[' x ]").
+End UNDER_IFF.
+
+Module Export Under_iff : UNDER_IFF.
+Definition Under_iff := iff.
+Lemma Under_from_iff (x y : Prop) :
+ @Under_iff x y -> x <-> y.
+Proof. by []. Qed.
+Definition Over_iff := Under_iff.
+Lemma over_iff :
+ forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y.
+Proof. by []. Qed.
+Lemma over_iff_done :
+ forall (x : Prop), @Over_iff x x.
+Proof. by []. Qed.
+Lemma under_iff_done :
+ forall (x : Prop), @Under_iff x x.
+Proof. by []. Qed.
+End Under_iff.
+
+Register Under_iff as plugins.ssreflect.Under_iff.
+Register Under_from_iff as plugins.ssreflect.Under_from_iff.
+
Ltac over :=
by [ apply: Under.under_done
| rewrite over
+ | apply: Under_iff.under_iff_done
+ | rewrite over_iff
].
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index ff6dd8f75a..842e4feecf 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -406,7 +406,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in
let sigma, _ = Typing.type_of env sigma cl' in
let gl = pf_merge_uc_of sigma gl in
- Proofview.V82.of_tactic (convert_concl cl'), rewritetac dir r', gl
+ Proofview.V82.of_tactic (convert_concl cl'), rewritetac ?under dir r', gl
else
let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in
let r3, _, r3t =
@@ -417,7 +417,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in
let itacs = [introid pattern_id; introid rule_id] in
let cltac = Proofview.V82.of_tactic (Tactics.clear [pattern_id; rule_id]) in
- let rwtacs = [rewritetac dir (EConstr.mkVar rule_id); cltac] in
+ let rwtacs = [rewritetac ?under dir (EConstr.mkVar rule_id); cltac] in
apply_type cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], tclTHENLIST (itacs @ rwtacs), gl
in
let cvtac' _ =
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index b5082582c9..2bac69b5b7 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -339,6 +339,19 @@ let intro_lock ipats =
let c = Proofview.Goal.concl gl in
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
+ match EConstr.kind_of_type sigma c with
+ | Term.AtomicType(hd, args) when
+ Ssrcommon.is_const_ref sigma hd (Coqlib.lib_ref "core.iff.type") &&
+ Array.length args = 2 && is_app_evar sigma args.(1) ->
+ Tactics.New.refine ~typecheck:true (fun sigma ->
+ let sigma, under_iff =
+ Ssrcommon.mkSsrConst "Under_iff" env sigma in
+ let sigma, under_from_iff =
+ Ssrcommon.mkSsrConst "Under_from_iff" env sigma in
+ let ty = EConstr.mkApp (under_iff,args) in
+ let sigma, t = Evarutil.new_evar env sigma ty in
+ sigma, EConstr.mkApp(under_from_iff,Array.append args [|t|]))
+ | _ ->
let t = Reductionops.whd_all env sigma c in
match EConstr.kind_of_type sigma t with
| Term.AtomicType(hd, args) when
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:22:47 +0000