From 4bc91ba5654574d156ebf2934a6fb36d31b40ff9 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 3 Apr 2019 15:03:02 +0200 Subject: [ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations as suggested by @gares, and: * Rename some Under_* terms for better uniformity; * Update & Improve minor details in the documentation. --- plugins/ssr/ssreflect.v | 83 +++++++++++++++++++++++++------------------------ plugins/ssr/ssrfwd.ml | 6 ++-- 2 files changed, 45 insertions(+), 44 deletions(-) (limited to 'plugins') diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 94e0b2a724..6c74ac1960 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -504,55 +504,55 @@ Proof. by move=> /(_ P); apply. Qed. (*****************************************************************************) (* Constants for under, to rewrite under binders using "Leibniz eta lemmas". *) -Module Type UNDER. -Parameter Under : +Module Type UNDER_EQ. +Parameter Under_eq : forall (R : Type), R -> R -> Prop. -Parameter Under_from_eq : - forall (T : Type) (x y : T), @Under T x y -> x = y. +Parameter Under_eq_from_eq : + forall (T : Type) (x y : T), @Under_eq T x y -> x = y. -(** [Over, over, over_done]: for "by rewrite over" *) -Parameter Over : +(** [Over_eq, over_eq, over_eq_done]: for "by rewrite over_eq" *) +Parameter Over_eq : forall (R : Type), R -> R -> Prop. -Parameter over : - forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y. -Parameter over_done : - forall (T : Type) (x : T), @Over T x x. +Parameter over_eq : + forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y. +Parameter over_eq_done : + forall (T : Type) (x : T), @Over_eq T x x. (* We need both hints below, otherwise the test-suite does not pass *) -Hint Extern 0 (@Over _ _ _) => solve [ apply over_done ] : core. +Hint Extern 0 (@Over_eq _ _ _) => solve [ apply over_eq_done ] : core. (* => for [test-suite/ssr/under.v:test_big_patt1] *) -Hint Resolve over_done : core. +Hint Resolve over_eq_done : core. (* => for [test-suite/ssr/over.v:test_over_1_1] *) -(** [under_done]: for Ltac-style over *) -Parameter under_done : - forall (T : Type) (x : T), @Under T x x. -Notation "''Under[' x ]" := (@Under _ x _) - (at level 8, format "''Under[' x ]"). -End UNDER. - -Module Export Under : UNDER. -Definition Under := @eq. -Lemma Under_from_eq (T : Type) (x y : T) : - @Under T x y -> x = y. +(** [under_eq_done]: for Ltac-style over *) +Parameter under_eq_done : + forall (T : Type) (x : T), @Under_eq T x x. +Notation "''Under[' x ]" := (@Under_eq _ x _) + (at level 8, format "''Under[' x ]", only printing). +End UNDER_EQ. + +Module Export Under_eq : UNDER_EQ. +Definition Under_eq := @eq. +Lemma Under_eq_from_eq (T : Type) (x y : T) : + @Under_eq T x y -> x = y. Proof. by []. Qed. -Definition Over := Under. -Lemma over : - forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y. +Definition Over_eq := Under_eq. +Lemma over_eq : + forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y. Proof. by []. Qed. -Lemma over_done : - forall (T : Type) (x : T), @Over T x x. +Lemma over_eq_done : + forall (T : Type) (x : T), @Over_eq T x x. Proof. by []. Qed. -Lemma under_done : - forall (T : Type) (x : T), @Under T x x. +Lemma under_eq_done : + forall (T : Type) (x : T), @Under_eq T x x. Proof. by []. Qed. -End Under. +End Under_eq. -Register Under as plugins.ssreflect.Under. -Register Under_from_eq as plugins.ssreflect.Under_from_eq. +Register Under_eq as plugins.ssreflect.Under_eq. +Register Under_eq_from_eq as plugins.ssreflect.Under_eq_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. +Parameter Under_iff_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. @@ -566,13 +566,13 @@ 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 ]"). +Notation "''Under[' x ]" := (@Under_iff x _) + (at level 8, format "''Under[' x ]", only printing). End UNDER_IFF. Module Export Under_iff : UNDER_IFF. Definition Under_iff := iff. -Lemma Under_from_iff (x y : Prop) : +Lemma Under_iff_from_iff (x y : Prop) : @Under_iff x y -> x <-> y. Proof. by []. Qed. Definition Over_iff := Under_iff. @@ -588,11 +588,12 @@ Proof. by []. Qed. End Under_iff. Register Under_iff as plugins.ssreflect.Under_iff. -Register Under_from_iff as plugins.ssreflect.Under_from_iff. +Register Under_iff_from_iff as plugins.ssreflect.Under_iff_from_iff. + +Definition over := (over_eq, over_iff). Ltac over := - by [ apply: Under.under_done - | rewrite over + by [ apply: Under_eq.under_eq_done | apply: Under_iff.under_iff_done - | rewrite over_iff + | rewrite over ]. diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index d60e3857b1..313b46ddc3 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -347,7 +347,7 @@ let intro_lock ipats = let sigma, under_iff = Ssrcommon.mkSsrConst "Under_iff" env sigma in let sigma, under_from_iff = - Ssrcommon.mkSsrConst "Under_from_iff" env sigma in + Ssrcommon.mkSsrConst "Under_iff_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|])) @@ -359,9 +359,9 @@ let intro_lock ipats = Array.length args = 3 && is_app_evar sigma args.(2) -> Tactics.New.refine ~typecheck:true (fun sigma -> let sigma, under = - Ssrcommon.mkSsrConst "Under" env sigma in + Ssrcommon.mkSsrConst "Under_eq" env sigma in let sigma, under_from_eq = - Ssrcommon.mkSsrConst "Under_from_eq" env sigma in + Ssrcommon.mkSsrConst "Under_eq_from_eq" env sigma in let ty = EConstr.mkApp (under,args) in let sigma, t = Evarutil.new_evar env sigma ty in sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|])) -- cgit v1.2.3