From 4e285a5d21633ecc47543c543043c31cd3be0a18 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 26 Apr 2019 12:24:22 +0200 Subject: [ssr] export Ssrequality.ssr_is_setoid --- plugins/ssr/ssrequality.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'plugins') diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index 43aeeb2dae..baf5288725 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -42,6 +42,9 @@ val mk_rwarg : val norwmult : ssrdir * ssrmult val norwocc : (Ssrast.ssrclear option * Ssrast.ssrocc) * Ssrmatching.rpattern option +val ssr_is_setoid : + Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t array -> bool + val ssrinstancesofrule : Ltac_plugin.Tacinterp.interp_sign -> Ssrast.ssrdir -> -- cgit v1.2.3 From 75f93e90e95f049ae23023f39add16a861ae114b Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 26 Apr 2019 13:00:38 +0200 Subject: [ssr] under: extend ssreflect.v to generalize iff to any setoid eq * Add an extra test with an Equivalence. * Update the doc accordingly. --- plugins/ssr/ssreflect.v | 93 ++++++++++++++++++++++++++++--------------------- plugins/ssr/ssrfwd.ml | 30 ++++++++++------ 2 files changed, 74 insertions(+), 49 deletions(-) (limited to 'plugins') diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 71abafc22f..bd95feacd8 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -531,7 +531,7 @@ Lemma abstract_context T (P : T -> Type) x : Proof. by move=> /(_ P); apply. Qed. (*****************************************************************************) -(* Constants for under, to rewrite under binders using "Leibniz eta lemmas". *) +(* Constants for under/over, to rewrite under binders using "context lemmas" *) Module Type UNDER_EQ. Parameter Under_eq : @@ -576,54 +576,69 @@ Lemma under_eq_done : Proof. by []. Qed. End Under_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_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. -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[' x ]" := (@Under_iff x _) +Register Under_eq.Under_eq as plugins.ssreflect.Under_eq. +Register Under_eq.Under_eq_from_eq as plugins.ssreflect.Under_eq_from_eq. + +Require Import Coq.Relations.Relation_Definitions. +Require Import RelationClasses. + +Module Type UNDER_REL. +Parameter Under_rel : + forall (A : Type) (eqA : relation A), Reflexive eqA -> relation A. +Parameter Under_rel_from_rel : + forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x y : A), + @Under_rel A eqA EeqA x y -> eqA x y. + +(** [Over_rel, over_rel, over_rel_done]: for "by rewrite over_rel" *) +Parameter Over_rel : + forall (A : Type) (eqA : relation A), Reflexive eqA -> relation A. +Parameter over_rel : + forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x y : A), + @Under_rel A eqA EeqA x y = @Over_rel A eqA EeqA x y. +Parameter over_rel_done : + forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x : A), + @Over_rel A eqA EeqA x x. +Hint Extern 0 (@Over_rel _ _ _ _ _) => solve [ apply over_rel_done ] : core. +Hint Resolve over_rel_done : core. + +(** [under_rel_done]: for Ltac-style over *) +Parameter under_rel_done : + forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x : A), + @Under_rel A eqA EeqA x x. +Notation "''Under[' x ]" := (@Under_rel _ _ _ x _) (at level 8, format "''Under[' x ]", only printing). -End UNDER_IFF. - -Module Export Under_iff : UNDER_IFF. -Definition Under_iff := iff. -Lemma Under_iff_from_iff (x y : Prop) : - @Under_iff x y -> x <-> y. +End UNDER_REL. + +Module Export Under_rel : UNDER_REL. +Definition Under_rel (A : Type) (eqA : relation A) (_ : Reflexive eqA) := + eqA. +Lemma Under_rel_from_rel : + forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x y : A), + @Under_rel A eqA EeqA x y -> eqA 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. +Definition Over_rel := Under_rel. +Lemma over_rel : + forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x y : A), + @Under_rel A eqA EeqA x y = @Over_rel A eqA EeqA x y. Proof. by []. Qed. -Lemma over_iff_done : - forall (x : Prop), @Over_iff x x. +Lemma over_rel_done : + forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x : A), + @Over_rel A eqA EeqA x x. Proof. by []. Qed. -Lemma under_iff_done : - forall (x : Prop), @Under_iff x x. +Lemma under_rel_done : + forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x : A), + @Under_rel A eqA EeqA x x. Proof. by []. Qed. -End Under_iff. +End Under_rel. -Register Under_iff as plugins.ssreflect.Under_iff. -Register Under_iff_from_iff as plugins.ssreflect.Under_iff_from_iff. +Register Under_rel.Under_rel as plugins.ssreflect.Under_rel. +Register Under_rel.Under_rel_from_rel as plugins.ssreflect.Under_rel_from_rel. -Definition over := (over_eq, over_iff). +Definition over := (over_eq, over_rel). Ltac over := by [ apply: Under_eq.under_eq_done - | apply: Under_iff.under_iff_done + | apply: Under_rel.under_rel_done | rewrite over ]. diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index cca94c8c9b..f67051eeb7 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -10,6 +10,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open Ltac_plugin open Pp open Names open Constr @@ -349,16 +350,25 @@ let intro_lock ipats = 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_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|])) + Array.length args >= 2 && is_app_evar sigma (Array.last args) && + Ssrequality.ssr_is_setoid env sigma hd args -> + Tactics.New.refine ~typecheck:true (fun sigma -> + let lm2 = Array.length args - 2 in + let sigma, carrier = + Typing.type_of env sigma args.(lm2) in + let rel = EConstr.mkApp (hd, Array.sub args 0 lm2) in + let rel_args = Array.sub args lm2 2 in + let sigma, refl = + (* could raise Not_found in theory *) + Rewrite.get_reflexive_proof env sigma carrier rel in + let sigma, under_rel = + Ssrcommon.mkSsrConst "Under_rel" env sigma in + let sigma, under_from_rel = + Ssrcommon.mkSsrConst "Under_rel_from_rel" env sigma in + let under_rel_args = Array.append [|carrier; rel; refl|] rel_args in + let ty = EConstr.mkApp (under_rel, under_rel_args) in + let sigma, t = Evarutil.new_evar env sigma ty in + sigma, EConstr.mkApp(under_from_rel,Array.append under_rel_args [|t|])) | _ -> let t = Reductionops.whd_all env sigma c in match EConstr.kind_of_type sigma t with -- cgit v1.2.3 From d60b807c868f4d54a273549519ea51c196242370 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 6 Aug 2019 22:52:16 +0200 Subject: [ssr] Refactor under's Setoid generalization to ease stdlib2 porting Changes: * Add ssrclasses.v that redefines [Reflexive] and [iff_Reflexive]; * Add ssrsetoid.v that links [ssrclasses.Reflexive] and [RelationClasses.Reflexive]; * Add [Require Coq.ssr.ssrsetoid] in Setoid.v; * Update ssrfwd.ml accordingly, using a helper file ssrclasses.ml that ports some non-exported material from rewrite.ml; * Some upside in passing: ssrfwd.ml no more depends on Ltac_plugin; * Update doc and tests as well. Summary: * We can now use the under tactic in two flavors: - with the [eq] or [iff] relations: [Require Import ssreflect.] - or a [RewriteRelation]: [Require Import ssreflect. Require Setoid.] (while [ssreflect] does not require [RelationClasses] nor [Setoid], and conversely [Setoid] does not require [ssreflect]). * The file ssrsetoid.v could be skipped when porting under to stdlib2. --- plugins/ssr/ssrclasses.ml | 59 +++++++++++++++++++++++++++++++++++++ plugins/ssr/ssrclasses.mli | 15 ++++++++++ plugins/ssr/ssrclasses.v | 28 ++++++++++++++++++ plugins/ssr/ssreflect.v | 25 ++++++++-------- plugins/ssr/ssreflect_plugin.mlpack | 2 +- plugins/ssr/ssrfwd.ml | 15 +++++++--- plugins/ssr/ssrsetoid.v | 33 +++++++++++++++++++++ 7 files changed, 159 insertions(+), 18 deletions(-) create mode 100644 plugins/ssr/ssrclasses.ml create mode 100644 plugins/ssr/ssrclasses.mli create mode 100644 plugins/ssr/ssrclasses.v create mode 100644 plugins/ssr/ssrsetoid.v (limited to 'plugins') diff --git a/plugins/ssr/ssrclasses.ml b/plugins/ssr/ssrclasses.ml new file mode 100644 index 0000000000..6cf5ffe201 --- /dev/null +++ b/plugins/ssr/ssrclasses.ml @@ -0,0 +1,59 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* + let (evd, c) = Evarutil.new_global evd (Lazy.force gr) in + (evd, cstrs), c + +(* Copy of [Rewrite.app_poly_check] *) +let app_poly_check env evars f args = + let (evars, cstrs), fc = f evars in + let evars, t = Typing.solve_evars env evars (EConstr.mkApp (fc, args)) in + (evars, cstrs), t + +(* Copy of [Rewrite.goalevars], [Rewrite.cstrevars] *) +let goalevars evars = fst evars +let cstrevars evars = snd evars + +(* Copy of [Rewrite.extends_undefined] *) +let extends_undefined evars evars' = + let f ev evi found = found || not (Evd.mem evars ev) + in Evd.fold_undefined f evars' false + +(* Copy of [Rewrite.find_class_proof] *) +let find_class_proof proof_type proof_method env evars carrier relation = + try + let evars, goal = app_poly_check env evars proof_type [| carrier ; relation |] in + let evars', c = Typeclasses.resolve_one_typeclass env (goalevars evars) goal in + if extends_undefined (goalevars evars) evars' then raise Not_found + else app_poly_check env (evars',cstrevars evars) proof_method [| carrier; relation; c |] + with e when Logic.catchable_exception e -> raise Not_found + +(* Copy of [Rewrite.get_lemma_proof *) +let get_lemma_proof f env evm x y = + let (evm, _), c = f env (evm,Evar.Set.empty) x y in + evm, c + +(* Clone of [Rewrite.PropGlobal.get_reflexive_proof] *) +let get_reflexive_proof_aux env = + let reflexive_type = find_global "plugins.ssreflect.reflexive_type" in + let reflexive_proof = find_global "plugins.ssreflect.reflexive_proof" in + find_class_proof reflexive_type reflexive_proof env + +(* Clone of [Rewrite.get_reflexive_proof], + using [Coq.ssr.ssrclasses.Reflexive] + instead of [Coq.Classes.RelationClasses.Reflexive] *) +let get_reflexive_proof_ssr = + get_lemma_proof get_reflexive_proof_aux diff --git a/plugins/ssr/ssrclasses.mli b/plugins/ssr/ssrclasses.mli new file mode 100644 index 0000000000..a0a1f40d9d --- /dev/null +++ b/plugins/ssr/ssrclasses.mli @@ -0,0 +1,15 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map * EConstr.constr diff --git a/plugins/ssr/ssrclasses.v b/plugins/ssr/ssrclasses.v new file mode 100644 index 0000000000..ed9ae0ce17 --- /dev/null +++ b/plugins/ssr/ssrclasses.v @@ -0,0 +1,28 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* .doc { font-family: monospace; white-space: pre; } # **) + +(** Compatibility layer for [under] and [setoid_rewrite]. + + Redefine [Coq.Classes.RelationClasses.Reflexive] here, so that doing + [Require Import ssreflect] does not [Require Import RelationClasses], + and conversely. **) + +Section Defs. + Context {A : Type}. + Class Reflexive (R : A -> A -> Prop) := + reflexivity : forall x : A, R x x. +End Defs. + +Register Reflexive as plugins.ssreflect.reflexive_type. +Register reflexivity as plugins.ssreflect.reflexive_proof. + +Instance iff_Reflexive : Reflexive iff := iff_refl. diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index bd95feacd8..fd73c86fb3 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -579,54 +579,53 @@ End Under_eq. Register Under_eq.Under_eq as plugins.ssreflect.Under_eq. Register Under_eq.Under_eq_from_eq as plugins.ssreflect.Under_eq_from_eq. -Require Import Coq.Relations.Relation_Definitions. -Require Import RelationClasses. +Require Import ssrclasses. Module Type UNDER_REL. Parameter Under_rel : - forall (A : Type) (eqA : relation A), Reflexive eqA -> relation A. + forall (A : Type) (eqA : A -> A -> Prop), Reflexive eqA -> A -> A -> Prop. Parameter Under_rel_from_rel : - forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x y : A), + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A), @Under_rel A eqA EeqA x y -> eqA x y. (** [Over_rel, over_rel, over_rel_done]: for "by rewrite over_rel" *) Parameter Over_rel : - forall (A : Type) (eqA : relation A), Reflexive eqA -> relation A. + forall (A : Type) (eqA : A -> A -> Prop), Reflexive eqA -> A -> A -> Prop. Parameter over_rel : - forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x y : A), + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A), @Under_rel A eqA EeqA x y = @Over_rel A eqA EeqA x y. Parameter over_rel_done : - forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x : A), + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), @Over_rel A eqA EeqA x x. Hint Extern 0 (@Over_rel _ _ _ _ _) => solve [ apply over_rel_done ] : core. Hint Resolve over_rel_done : core. (** [under_rel_done]: for Ltac-style over *) Parameter under_rel_done : - forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x : A), + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), @Under_rel A eqA EeqA x x. Notation "''Under[' x ]" := (@Under_rel _ _ _ x _) (at level 8, format "''Under[' x ]", only printing). End UNDER_REL. Module Export Under_rel : UNDER_REL. -Definition Under_rel (A : Type) (eqA : relation A) (_ : Reflexive eqA) := +Definition Under_rel (A : Type) (eqA : A -> A -> Prop) (_ : Reflexive eqA) := eqA. Lemma Under_rel_from_rel : - forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x y : A), + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A), @Under_rel A eqA EeqA x y -> eqA x y. Proof. by []. Qed. Definition Over_rel := Under_rel. Lemma over_rel : - forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x y : A), + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A), @Under_rel A eqA EeqA x y = @Over_rel A eqA EeqA x y. Proof. by []. Qed. Lemma over_rel_done : - forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x : A), + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), @Over_rel A eqA EeqA x x. Proof. by []. Qed. Lemma under_rel_done : - forall (A : Type) (eqA : relation A) (EeqA : Reflexive eqA) (x : A), + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), @Under_rel A eqA EeqA x x. Proof. by []. Qed. End Under_rel. diff --git a/plugins/ssr/ssreflect_plugin.mlpack b/plugins/ssr/ssreflect_plugin.mlpack index 824348fee7..66aa6b3e67 100644 --- a/plugins/ssr/ssreflect_plugin.mlpack +++ b/plugins/ssr/ssreflect_plugin.mlpack @@ -7,7 +7,7 @@ Ssrview Ssrbwd Ssrequality Ssripats +Ssrclasses Ssrfwd Ssrparser Ssrvernac - diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index f67051eeb7..3401a49bf3 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -10,7 +10,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Ltac_plugin open Pp open Names open Constr @@ -351,7 +350,14 @@ let intro_lock ipats = match EConstr.kind_of_type sigma c with | Term.AtomicType(hd, args) when Array.length args >= 2 && is_app_evar sigma (Array.last args) && - Ssrequality.ssr_is_setoid env sigma hd args -> + Ssrequality.ssr_is_setoid env sigma hd args + (* if the last condition above [ssr_is_setoid ...] holds + then [Coq.Classes.RelationClasses] has been required *) + || + (* if this is not the case, the tactic can still succeed + when the considered relation is [Coq.Init.Logic.iff] *) + 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 lm2 = Array.length args - 2 in let sigma, carrier = @@ -359,8 +365,9 @@ let intro_lock ipats = let rel = EConstr.mkApp (hd, Array.sub args 0 lm2) in let rel_args = Array.sub args lm2 2 in let sigma, refl = - (* could raise Not_found in theory *) - Rewrite.get_reflexive_proof env sigma carrier rel in + (* this could raise Not_found, but this should never occur in + practice given ssrclasses.v, so we put no try/with block *) + Ssrclasses.get_reflexive_proof_ssr env sigma carrier rel in let sigma, under_rel = Ssrcommon.mkSsrConst "Under_rel" env sigma in let sigma, under_from_rel = diff --git a/plugins/ssr/ssrsetoid.v b/plugins/ssr/ssrsetoid.v new file mode 100644 index 0000000000..75653be0c5 --- /dev/null +++ b/plugins/ssr/ssrsetoid.v @@ -0,0 +1,33 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* .doc { font-family: monospace; white-space: pre; } # **) + +(** Compatibility layer for [under] and [setoid_rewrite]. + + This file is intended to be required by [Require Import Setoid] or so + in order to reconcile [Coq.Classes.RelationClasses.Reflexive] with + [Coq.ssr.ssrclasses.Reflexive]. + + We can thus use the [under] tactic with other relations than [eq], + such as [iff] or a [RewriteRelation], by doing: + [Require Import ssreflect. Require Setoid.] + + (Note: this file could be skipped when porting [under] to stdlib2.) + *) + +Require Import ssrclasses. +Require Import RelationClasses. + +Instance compat_Reflexive : + forall {A} {R : A -> A -> Prop}, + RelationClasses.Reflexive R -> + ssrclasses.Reflexive R. +Proof. now trivial. Qed. -- cgit v1.2.3 From e4c185319f3511a8794a12b099400015508d76ee Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 9 Sep 2019 19:03:30 -0700 Subject: feat: Add a rewrite rule (UnderE) to unprotect evars in subgoals E.g., if one wish to instantiate these evars manually, in another way than with reflexivity. --- plugins/ssr/ssreflect.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'plugins') diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index fd73c86fb3..c98d872a9c 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -538,6 +538,8 @@ Parameter Under_eq : forall (R : Type), R -> R -> Prop. Parameter Under_eq_from_eq : forall (T : Type) (x y : T), @Under_eq T x y -> x = y. +Parameter Under_eqE : + forall (T : Type) (x y : T), @Under_eq T x y = (x = y). (** [Over_eq, over_eq, over_eq_done]: for "by rewrite over_eq" *) Parameter Over_eq : @@ -564,6 +566,9 @@ Definition Under_eq := @eq. Lemma Under_eq_from_eq (T : Type) (x y : T) : @Under_eq T x y -> x = y. Proof. by []. Qed. +Lemma Under_eqE (T : Type) (x y : T) : + @Under_eq T x y = (x = y). +Proof. by []. Qed. 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. @@ -587,6 +592,9 @@ Parameter Under_rel : Parameter Under_rel_from_rel : forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A), @Under_rel A eqA EeqA x y -> eqA x y. +Parameter Under_relE : + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A), + @Under_rel A eqA EeqA x y = eqA x y. (** [Over_rel, over_rel, over_rel_done]: for "by rewrite over_rel" *) Parameter Over_rel : @@ -615,6 +623,9 @@ Lemma Under_rel_from_rel : forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A), @Under_rel A eqA EeqA x y -> eqA x y. Proof. by []. Qed. +Lemma Under_relE (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A) : + @Under_rel A eqA EeqA x y = eqA x y. +Proof. by []. Qed. Definition Over_rel := Under_rel. Lemma over_rel : forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A), @@ -633,14 +644,20 @@ End Under_rel. Register Under_rel.Under_rel as plugins.ssreflect.Under_rel. Register Under_rel.Under_rel_from_rel as plugins.ssreflect.Under_rel_from_rel. +(** Closing rewrite rule *) Definition over := (over_eq, over_rel). +(** Closing tactic *) Ltac over := by [ apply: Under_eq.under_eq_done | apply: Under_rel.under_rel_done | rewrite over ]. +(** Convenience rewrite rule to unprotect evars, e.g., to instantiate + them in another way than with reflexivity. *) +Definition UnderE := (Under_eqE, Under_relE). + (** An interface for non-Prop types; used to avoid improper instantiation of polymorphic lemmas with on-demand implicits when they are used as views. For example: Some_inj {T} : forall x y : T, Some x = Some y -> x = y. -- cgit v1.2.3 From 2845bc2712604a3fab3b3a8497bb29b38acf2777 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sun, 20 Oct 2019 22:17:03 +0200 Subject: chore: Enclose the […get_reflexive_proof_ssr…] call in a try/with->assert false as suggested by @gares (the Not_found exc may be catched by coq/ssr otherwise). --- plugins/ssr/ssrfwd.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'plugins') diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 3401a49bf3..485ec667d6 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -365,9 +365,16 @@ let intro_lock ipats = let rel = EConstr.mkApp (hd, Array.sub args 0 lm2) in let rel_args = Array.sub args lm2 2 in let sigma, refl = - (* this could raise Not_found, but this should never occur in - practice given ssrclasses.v, so we put no try/with block *) - Ssrclasses.get_reflexive_proof_ssr env sigma carrier rel in + try + Ssrclasses.get_reflexive_proof_ssr env sigma carrier rel + (* could raise Not_found--this can't occur actually: + at that point, either [Ssrequality.ssr_is_setoid] + holds or the relation is [Coq.Init.Logic.iff], + and [Coq.ssr.ssrclasses] was necessarily required + so we know that in the environment, the relation + has an instance of [Coq.ssr.ssrclasses.Reflexive] + *) + with Not_found -> assert false in let sigma, under_rel = Ssrcommon.mkSsrConst "Under_rel" env sigma in let sigma, under_from_rel = -- cgit v1.2.3 From 1090b272772c70a79fb082713451a935737cb1d3 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 31 Oct 2019 22:08:47 +0100 Subject: [ssr] Refactor/Simplify the implementation of under * Preserve the same behavior/interface but merge the two Module Types (UNDER_EQ and) UNDER_REL. * Remove the "Reflexive" argument in Under_rel.Under_rel * Update plugin code (ssrfwd.ml) & Factor-out the main step * Update the Hint (viz. apply over_rel_done => apply: over_rel_done) * All the tests still pass! Credits to @CohenCyril for suggesting this enhancement --- plugins/ssr/ssrclasses.v | 1 + plugins/ssr/ssreflect.v | 103 ++++++++++++----------------------------------- plugins/ssr/ssrfwd.ml | 50 ++++++++--------------- 3 files changed, 44 insertions(+), 110 deletions(-) (limited to 'plugins') diff --git a/plugins/ssr/ssrclasses.v b/plugins/ssr/ssrclasses.v index ed9ae0ce17..29486ff4cf 100644 --- a/plugins/ssr/ssrclasses.v +++ b/plugins/ssr/ssrclasses.v @@ -25,4 +25,5 @@ End Defs. Register Reflexive as plugins.ssreflect.reflexive_type. Register reflexivity as plugins.ssreflect.reflexive_proof. +Instance eq_Reflexive {A : Type} : Reflexive (@eq A) := @eq_refl A. Instance iff_Reflexive : Reflexive iff := iff_refl. diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index c98d872a9c..a19aade6e9 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -533,111 +533,61 @@ Proof. by move=> /(_ P); apply. Qed. (*****************************************************************************) (* Constants for under/over, to rewrite under binders using "context lemmas" *) -Module Type UNDER_EQ. -Parameter Under_eq : - forall (R : Type), R -> R -> Prop. -Parameter Under_eq_from_eq : - forall (T : Type) (x y : T), @Under_eq T x y -> x = y. -Parameter Under_eqE : - forall (T : Type) (x y : T), @Under_eq T x y = (x = y). - -(** [Over_eq, over_eq, over_eq_done]: for "by rewrite over_eq" *) -Parameter Over_eq : - forall (R : Type), R -> R -> Prop. -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_eq _ _ _) => solve [ apply over_eq_done ] : core. -(* => for [test-suite/ssr/under.v:test_big_patt1] *) -Hint Resolve over_eq_done : core. -(* => for [test-suite/ssr/over.v:test_over_1_1] *) - -(** [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. -Lemma Under_eqE (T : Type) (x y : T) : - @Under_eq T x y = (x = y). -Proof. by []. Qed. -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_eq_done : - forall (T : Type) (x : T), @Over_eq T x x. -Proof. by []. Qed. -Lemma under_eq_done : - forall (T : Type) (x : T), @Under_eq T x x. -Proof. by []. Qed. -End Under_eq. - -Register Under_eq.Under_eq as plugins.ssreflect.Under_eq. -Register Under_eq.Under_eq_from_eq as plugins.ssreflect.Under_eq_from_eq. - Require Import ssrclasses. Module Type UNDER_REL. Parameter Under_rel : - forall (A : Type) (eqA : A -> A -> Prop), Reflexive eqA -> A -> A -> Prop. + forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop. Parameter Under_rel_from_rel : - forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A), - @Under_rel A eqA EeqA x y -> eqA x y. + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y -> eqA x y. Parameter Under_relE : - forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A), - @Under_rel A eqA EeqA x y = eqA x y. + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y = eqA x y. (** [Over_rel, over_rel, over_rel_done]: for "by rewrite over_rel" *) Parameter Over_rel : - forall (A : Type) (eqA : A -> A -> Prop), Reflexive eqA -> A -> A -> Prop. + forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop. Parameter over_rel : - forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A), - @Under_rel A eqA EeqA x y = @Over_rel A eqA EeqA x y. + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y = @Over_rel A eqA x y. Parameter over_rel_done : forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), - @Over_rel A eqA EeqA x x. -Hint Extern 0 (@Over_rel _ _ _ _ _) => solve [ apply over_rel_done ] : core. + @Over_rel A eqA x x. +Hint Extern 0 (@Over_rel _ _ _ _) => + solve [ apply: over_rel_done ] : core. Hint Resolve over_rel_done : core. (** [under_rel_done]: for Ltac-style over *) Parameter under_rel_done : forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), - @Under_rel A eqA EeqA x x. -Notation "''Under[' x ]" := (@Under_rel _ _ _ x _) + @Under_rel A eqA x x. +Notation "''Under[' x ]" := (@Under_rel _ _ x _) (at level 8, format "''Under[' x ]", only printing). End UNDER_REL. Module Export Under_rel : UNDER_REL. -Definition Under_rel (A : Type) (eqA : A -> A -> Prop) (_ : Reflexive eqA) := +Definition Under_rel (A : Type) (eqA : A -> A -> Prop) := eqA. Lemma Under_rel_from_rel : - forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A), - @Under_rel A eqA EeqA x y -> eqA x y. + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y -> eqA x y. Proof. by []. Qed. -Lemma Under_relE (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A) : - @Under_rel A eqA EeqA x y = eqA x y. +Lemma Under_relE (A : Type) (eqA : A -> A -> Prop) (x y : A) : + @Under_rel A eqA x y = eqA x y. Proof. by []. Qed. Definition Over_rel := Under_rel. Lemma over_rel : - forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x y : A), - @Under_rel A eqA EeqA x y = @Over_rel A eqA EeqA x y. + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y = @Over_rel A eqA x y. Proof. by []. Qed. Lemma over_rel_done : forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), - @Over_rel A eqA EeqA x x. -Proof. by []. Qed. + @Over_rel A eqA x x. +Proof. by rewrite /Over_rel. Qed. Lemma under_rel_done : forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), - @Under_rel A eqA EeqA x x. + @Under_rel A eqA x x. Proof. by []. Qed. End Under_rel. @@ -645,18 +595,17 @@ Register Under_rel.Under_rel as plugins.ssreflect.Under_rel. Register Under_rel.Under_rel_from_rel as plugins.ssreflect.Under_rel_from_rel. (** Closing rewrite rule *) -Definition over := (over_eq, over_rel). +Definition over := over_rel. (** Closing tactic *) Ltac over := - by [ apply: Under_eq.under_eq_done - | apply: Under_rel.under_rel_done + by [ apply: Under_rel.under_rel_done | rewrite over ]. (** Convenience rewrite rule to unprotect evars, e.g., to instantiate them in another way than with reflexivity. *) -Definition UnderE := (Under_eqE, Under_relE). +Definition UnderE := Under_relE. (** An interface for non-Prop types; used to avoid improper instantiation of polymorphic lemmas with on-demand implicits when they are used as views. diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 485ec667d6..b0f56c423f 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -340,6 +340,21 @@ let intro_lock ipats = let hnf' = Proofview.numgoals >>= fun ng -> Proofview.tclDISPATCH (ncons (ng - 1) ssrsmovetac @ [Proofview.tclUNIT ()]) in + let protect_subgoal env sigma hd args = + Tactics.New.refine ~typecheck:true (fun sigma -> + let lm2 = Array.length args - 2 in + let sigma, carrier = + Typing.type_of env sigma args.(lm2) in + let rel = EConstr.mkApp (hd, Array.sub args 0 lm2) in + let rel_args = Array.sub args lm2 2 in + let sigma, under_rel = + Ssrcommon.mkSsrConst "Under_rel" env sigma in + let sigma, under_from_rel = + Ssrcommon.mkSsrConst "Under_rel_from_rel" env sigma in + let under_rel_args = Array.append [|carrier; rel|] rel_args in + let ty = EConstr.mkApp (under_rel, under_rel_args) in + let sigma, t = Evarutil.new_evar env sigma ty in + sigma, EConstr.mkApp(under_from_rel,Array.append under_rel_args [|t|])) in let rec lock_eq () : unit Proofview.tactic = Proofview.Goal.enter begin fun _ -> Proofview.tclORELSE (Ssripats.tclIPAT [Ssripats.IOpTemporay; Ssripats.IOpEqGen (lock_eq ())]) @@ -358,45 +373,14 @@ let intro_lock ipats = when the considered relation is [Coq.Init.Logic.iff] *) 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 lm2 = Array.length args - 2 in - let sigma, carrier = - Typing.type_of env sigma args.(lm2) in - let rel = EConstr.mkApp (hd, Array.sub args 0 lm2) in - let rel_args = Array.sub args lm2 2 in - let sigma, refl = - try - Ssrclasses.get_reflexive_proof_ssr env sigma carrier rel - (* could raise Not_found--this can't occur actually: - at that point, either [Ssrequality.ssr_is_setoid] - holds or the relation is [Coq.Init.Logic.iff], - and [Coq.ssr.ssrclasses] was necessarily required - so we know that in the environment, the relation - has an instance of [Coq.ssr.ssrclasses.Reflexive] - *) - with Not_found -> assert false in - let sigma, under_rel = - Ssrcommon.mkSsrConst "Under_rel" env sigma in - let sigma, under_from_rel = - Ssrcommon.mkSsrConst "Under_rel_from_rel" env sigma in - let under_rel_args = Array.append [|carrier; rel; refl|] rel_args in - let ty = EConstr.mkApp (under_rel, under_rel_args) in - let sigma, t = Evarutil.new_evar env sigma ty in - sigma, EConstr.mkApp(under_from_rel,Array.append under_rel_args [|t|])) + protect_subgoal env sigma hd args | _ -> let t = Reductionops.whd_all env sigma c in match EConstr.kind_of_type sigma t with | Term.AtomicType(hd, args) when Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") && Array.length args = 3 && is_app_evar sigma args.(2) -> - Tactics.New.refine ~typecheck:true (fun sigma -> - let sigma, under = - Ssrcommon.mkSsrConst "Under_eq" env sigma in - let sigma, under_from_eq = - 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|])) + protect_subgoal env sigma hd args | _ -> ppdebug(lazy Pp.(str"under: stop:" ++ pr_econstr_env env sigma t)); -- cgit v1.2.3 From a37b6f81a3d3922dc89a179b50494d0bbd7afbf6 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 1 Nov 2019 00:49:55 +0100 Subject: [ssr] Refactor/Extend of under to support more relations (namely, [RewriteRelation]s beyond Equivalence ones) Thanks to @CohenCyril for suggesting this enhancement --- plugins/ssr/ssrclasses.v | 3 ++ plugins/ssr/ssreflect.v | 68 +++++-------------------------- plugins/ssr/ssrsetoid.v | 103 +++++++++++++++++++++++++++++++++++++++++++---- plugins/ssr/ssrunder.v | 75 ++++++++++++++++++++++++++++++++++ 4 files changed, 183 insertions(+), 66 deletions(-) create mode 100644 plugins/ssr/ssrunder.v (limited to 'plugins') diff --git a/plugins/ssr/ssrclasses.v b/plugins/ssr/ssrclasses.v index 29486ff4cf..0ae3f8c6a5 100644 --- a/plugins/ssr/ssrclasses.v +++ b/plugins/ssr/ssrclasses.v @@ -12,6 +12,9 @@ (** Compatibility layer for [under] and [setoid_rewrite]. + Note: this file does not require [ssreflect]; it is both required by + [ssrsetoid] and required by [ssrunder]. + Redefine [Coq.Classes.RelationClasses.Reflexive] here, so that doing [Require Import ssreflect] does not [Require Import RelationClasses], and conversely. **) diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index a19aade6e9..43c091123e 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -531,65 +531,13 @@ Lemma abstract_context T (P : T -> Type) x : Proof. by move=> /(_ P); apply. Qed. (*****************************************************************************) -(* Constants for under/over, to rewrite under binders using "context lemmas" *) - -Require Import ssrclasses. - -Module Type UNDER_REL. -Parameter Under_rel : - forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop. -Parameter Under_rel_from_rel : - forall (A : Type) (eqA : A -> A -> Prop) (x y : A), - @Under_rel A eqA x y -> eqA x y. -Parameter Under_relE : - forall (A : Type) (eqA : A -> A -> Prop) (x y : A), - @Under_rel A eqA x y = eqA x y. - -(** [Over_rel, over_rel, over_rel_done]: for "by rewrite over_rel" *) -Parameter Over_rel : - forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop. -Parameter over_rel : - forall (A : Type) (eqA : A -> A -> Prop) (x y : A), - @Under_rel A eqA x y = @Over_rel A eqA x y. -Parameter over_rel_done : - forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), - @Over_rel A eqA x x. -Hint Extern 0 (@Over_rel _ _ _ _) => - solve [ apply: over_rel_done ] : core. -Hint Resolve over_rel_done : core. - -(** [under_rel_done]: for Ltac-style over *) -Parameter under_rel_done : - forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), - @Under_rel A eqA x x. -Notation "''Under[' x ]" := (@Under_rel _ _ x _) - (at level 8, format "''Under[' x ]", only printing). -End UNDER_REL. - -Module Export Under_rel : UNDER_REL. -Definition Under_rel (A : Type) (eqA : A -> A -> Prop) := - eqA. -Lemma Under_rel_from_rel : - forall (A : Type) (eqA : A -> A -> Prop) (x y : A), - @Under_rel A eqA x y -> eqA x y. -Proof. by []. Qed. -Lemma Under_relE (A : Type) (eqA : A -> A -> Prop) (x y : A) : - @Under_rel A eqA x y = eqA x y. -Proof. by []. Qed. -Definition Over_rel := Under_rel. -Lemma over_rel : - forall (A : Type) (eqA : A -> A -> Prop) (x y : A), - @Under_rel A eqA x y = @Over_rel A eqA x y. -Proof. by []. Qed. -Lemma over_rel_done : - forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), - @Over_rel A eqA x x. -Proof. by rewrite /Over_rel. Qed. -Lemma under_rel_done : - forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), - @Under_rel A eqA x x. -Proof. by []. Qed. -End Under_rel. +(* Material for under/over (to rewrite under binders using "context lemmas") *) + +Require Export ssrunder. + +Hint Extern 0 (@Under_rel.Over_rel _ _ _ _) => + solve [ apply: Under_rel.over_rel_done ] : core. +Hint Resolve Under_rel.over_rel_done : core. Register Under_rel.Under_rel as plugins.ssreflect.Under_rel. Register Under_rel.Under_rel_from_rel as plugins.ssreflect.Under_rel_from_rel. @@ -607,6 +555,8 @@ Ltac over := them in another way than with reflexivity. *) Definition UnderE := Under_relE. +(*****************************************************************************) + (** An interface for non-Prop types; used to avoid improper instantiation of polymorphic lemmas with on-demand implicits when they are used as views. For example: Some_inj {T} : forall x y : T, Some x = Some y -> x = y. diff --git a/plugins/ssr/ssrsetoid.v b/plugins/ssr/ssrsetoid.v index 75653be0c5..609c9d5ab8 100644 --- a/plugins/ssr/ssrsetoid.v +++ b/plugins/ssr/ssrsetoid.v @@ -12,22 +12,111 @@ (** Compatibility layer for [under] and [setoid_rewrite]. - This file is intended to be required by [Require Import Setoid] or so - in order to reconcile [Coq.Classes.RelationClasses.Reflexive] with - [Coq.ssr.ssrclasses.Reflexive]. + This file is intended to be required by [Require Import Setoid]. - We can thus use the [under] tactic with other relations than [eq], - such as [iff] or a [RewriteRelation], by doing: + In particular, we can use the [under] tactic with other relations + than [eq] or [iff], e.g. a [RewriteRelation], by doing: [Require Import ssreflect. Require Setoid.] + This file's instances have priority 12 > other stdlib instances + and each [Under_rel] instance comes with a [Hint Cut] directive + (otherwise Ring_polynom.v won't compile because of unbounded search). + (Note: this file could be skipped when porting [under] to stdlib2.) *) Require Import ssrclasses. +Require Import ssrunder. Require Import RelationClasses. +Require Import Relation_Definitions. + +(** Reconcile [Coq.Classes.RelationClasses.Reflexive] with + [Coq.ssr.ssrclasses.Reflexive] *) Instance compat_Reflexive : - forall {A} {R : A -> A -> Prop}, + forall {A} {R : relation A}, RelationClasses.Reflexive R -> - ssrclasses.Reflexive R. + ssrclasses.Reflexive R | 12. Proof. now trivial. Qed. + +(** Add instances so that ['Under[ F i ]] terms, + that is, [Under_rel T R (F i) (?G i)] terms, + can be manipulated with rewrite/setoid_rewrite with lemmas on [R]. + Note that this requires that [R] is a [Prop] relation, otherwise + a [bool] relation may need to be "lifted": see the [TestPreOrder] + section in test-suite/ssr/under.v *) + +Instance Under_subrelation {A} (R : relation A) : subrelation R (Under_rel _ R) | 12. +Proof. now rewrite Under_relE. Qed. + +(* see also Morphisms.trans_co_eq_inv_impl_morphism *) + +Instance Under_Reflexive {A} (R : relation A) : + RelationClasses.Reflexive R -> + RelationClasses.Reflexive (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Reflexive Under_Reflexive] : typeclass_instances. + +(* These instances are a bit off-topic given that (Under_rel A R) will + typically be reflexive, to be able to trigger the [over] terminator + +Instance under_Irreflexive {A} (R : relation A) : + RelationClasses.Irreflexive R -> + RelationClasses.Irreflexive (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Irreflexive Under_Irreflexive] : typeclass_instances. + +Instance under_Asymmetric {A} (R : relation A) : + RelationClasses.Asymmetric R -> + RelationClasses.Asymmetric (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Asymmetric Under_Asymmetric] : typeclass_instances. + +Instance under_StrictOrder {A} (R : relation A) : + RelationClasses.StrictOrder R -> + RelationClasses.StrictOrder (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Strictorder Under_Strictorder] : typeclass_instances. + *) + +Instance Under_Symmetric {A} (R : relation A) : + RelationClasses.Symmetric R -> + RelationClasses.Symmetric (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Symmetric Under_Symmetric] : typeclass_instances. + +Instance Under_Transitive {A} (R : relation A) : + RelationClasses.Transitive R -> + RelationClasses.Transitive (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Transitive Under_Transitive] : typeclass_instances. + +Instance Under_PreOrder {A} (R : relation A) : + RelationClasses.PreOrder R -> + RelationClasses.PreOrder (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_PreOrder Under_PreOrder] : typeclass_instances. + +Instance Under_PER {A} (R : relation A) : + RelationClasses.PER R -> + RelationClasses.PER (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_PER Under_PER] : typeclass_instances. + +Instance Under_Equivalence {A} (R : relation A) : + RelationClasses.Equivalence R -> + RelationClasses.Equivalence (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Equivalence Under_Equivalence] : typeclass_instances. + +(* Don't handle Antisymmetric and PartialOrder classes for now, + as these classes depend on two relation symbols... *) diff --git a/plugins/ssr/ssrunder.v b/plugins/ssr/ssrunder.v new file mode 100644 index 0000000000..7c529a6133 --- /dev/null +++ b/plugins/ssr/ssrunder.v @@ -0,0 +1,75 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* .doc { font-family: monospace; white-space: pre; } # **) + +(** Constants for under/over, to rewrite under binders using "context lemmas" + + Note: this file does not require [ssreflect]; it is both required by + [ssrsetoid] and *exported* by [ssrunder]. + + This preserves the following feature: we can use [Setoid] without + requiring [ssreflect] and use [ssreflect] without requiring [Setoid]. +*) + +Require Import ssrclasses. + +Module Type UNDER_REL. +Parameter Under_rel : + forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop. +Parameter Under_rel_from_rel : + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y -> eqA x y. +Parameter Under_relE : + forall (A : Type) (eqA : A -> A -> Prop), + @Under_rel A eqA = eqA. + +(** [Over_rel, over_rel, over_rel_done]: for "by rewrite over_rel" *) +Parameter Over_rel : + forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop. +Parameter over_rel : + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y = @Over_rel A eqA x y. +Parameter over_rel_done : + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), + @Over_rel A eqA x x. + +(** [under_rel_done]: for Ltac-style over *) +Parameter under_rel_done : + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), + @Under_rel A eqA x x. +Notation "''Under[' x ]" := (@Under_rel _ _ x _) + (at level 8, format "''Under[' x ]", only printing). +End UNDER_REL. + +Module Export Under_rel : UNDER_REL. +Definition Under_rel (A : Type) (eqA : A -> A -> Prop) := + eqA. +Lemma Under_rel_from_rel : + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y -> eqA x y. +Proof. now trivial. Qed. +Lemma Under_relE (A : Type) (eqA : A -> A -> Prop) : + @Under_rel A eqA = eqA. +Proof. now trivial. Qed. +Definition Over_rel := Under_rel. +Lemma over_rel : + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y = @Over_rel A eqA x y. +Proof. now trivial. Qed. +Lemma over_rel_done : + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), + @Over_rel A eqA x x. +Proof. now unfold Over_rel. Qed. +Lemma under_rel_done : + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), + @Under_rel A eqA x x. +Proof. now trivial. Qed. +End Under_rel. -- cgit v1.2.3 From 1857d474d06b23df32c16be26225ee174ad4d6c1 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 1 Nov 2019 01:45:33 +0100 Subject: [ssr] chore: Remove ssrclasses.{ml,mli} (now unneeded) --- plugins/ssr/ssrclasses.ml | 59 ------------------------------------- plugins/ssr/ssrclasses.mli | 15 ---------- plugins/ssr/ssreflect_plugin.mlpack | 1 - 3 files changed, 75 deletions(-) delete mode 100644 plugins/ssr/ssrclasses.ml delete mode 100644 plugins/ssr/ssrclasses.mli (limited to 'plugins') diff --git a/plugins/ssr/ssrclasses.ml b/plugins/ssr/ssrclasses.ml deleted file mode 100644 index 6cf5ffe201..0000000000 --- a/plugins/ssr/ssrclasses.ml +++ /dev/null @@ -1,59 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* - let (evd, c) = Evarutil.new_global evd (Lazy.force gr) in - (evd, cstrs), c - -(* Copy of [Rewrite.app_poly_check] *) -let app_poly_check env evars f args = - let (evars, cstrs), fc = f evars in - let evars, t = Typing.solve_evars env evars (EConstr.mkApp (fc, args)) in - (evars, cstrs), t - -(* Copy of [Rewrite.goalevars], [Rewrite.cstrevars] *) -let goalevars evars = fst evars -let cstrevars evars = snd evars - -(* Copy of [Rewrite.extends_undefined] *) -let extends_undefined evars evars' = - let f ev evi found = found || not (Evd.mem evars ev) - in Evd.fold_undefined f evars' false - -(* Copy of [Rewrite.find_class_proof] *) -let find_class_proof proof_type proof_method env evars carrier relation = - try - let evars, goal = app_poly_check env evars proof_type [| carrier ; relation |] in - let evars', c = Typeclasses.resolve_one_typeclass env (goalevars evars) goal in - if extends_undefined (goalevars evars) evars' then raise Not_found - else app_poly_check env (evars',cstrevars evars) proof_method [| carrier; relation; c |] - with e when Logic.catchable_exception e -> raise Not_found - -(* Copy of [Rewrite.get_lemma_proof *) -let get_lemma_proof f env evm x y = - let (evm, _), c = f env (evm,Evar.Set.empty) x y in - evm, c - -(* Clone of [Rewrite.PropGlobal.get_reflexive_proof] *) -let get_reflexive_proof_aux env = - let reflexive_type = find_global "plugins.ssreflect.reflexive_type" in - let reflexive_proof = find_global "plugins.ssreflect.reflexive_proof" in - find_class_proof reflexive_type reflexive_proof env - -(* Clone of [Rewrite.get_reflexive_proof], - using [Coq.ssr.ssrclasses.Reflexive] - instead of [Coq.Classes.RelationClasses.Reflexive] *) -let get_reflexive_proof_ssr = - get_lemma_proof get_reflexive_proof_aux diff --git a/plugins/ssr/ssrclasses.mli b/plugins/ssr/ssrclasses.mli deleted file mode 100644 index a0a1f40d9d..0000000000 --- a/plugins/ssr/ssrclasses.mli +++ /dev/null @@ -1,15 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map * EConstr.constr diff --git a/plugins/ssr/ssreflect_plugin.mlpack b/plugins/ssr/ssreflect_plugin.mlpack index 66aa6b3e67..46669998b9 100644 --- a/plugins/ssr/ssreflect_plugin.mlpack +++ b/plugins/ssr/ssreflect_plugin.mlpack @@ -7,7 +7,6 @@ Ssrview Ssrbwd Ssrequality Ssripats -Ssrclasses Ssrfwd Ssrparser Ssrvernac -- cgit v1.2.3