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(+)
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.
---
.../proof-engine/ssreflect-proof-language.rst | 5 +-
plugins/ssr/ssreflect.v | 93 +++++++++++++---------
plugins/ssr/ssrfwd.ml | 30 ++++---
test-suite/ssr/under.v | 22 ++++-
4 files changed, 98 insertions(+), 52 deletions(-)
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index ed980bd4de..0af23354cc 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3756,8 +3756,9 @@ involves the following steps:
the corresponding intro pattern :n:`@i_pattern__i` in each goal.
4. Then :tacn:`under` checks that the first n subgoals
- are (quantified) equalities or double implications between a
- term and an evar (e.g. ``m - m = ?F2 m`` in the running example).
+ are (quantified) Leibniz equalities or registered Setoid equalities
+ between a term and an evar (e.g. ``m - m = ?F2 m`` in the running
+ example).
5. If so :tacn:`under` protects these n goals against an
accidental instantiation of the evar.
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
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index f285ad138b..b1349f287a 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -228,7 +228,27 @@ Qed.
Arguments ex_iff [R P1] P2 iffP12.
Require Import Setoid.
+
Lemma test_ex_iff (P : nat -> Prop) : (exists x, P x) -> True.
under ex_iff => n.
by rewrite over.
-Abort.
+by move=> _.
+Qed.
+
+
+Section TestGeneric.
+Context {A B : Type} {R : nat -> relation B} `{!forall n : nat, Equivalence (R n)}.
+Variables (F : (A -> A -> B) -> B).
+Hypothesis ex_gen : forall (n : nat) (P1 P2 : A -> A -> B),
+ (forall x y : A, R n (P1 x y) (P2 x y)) -> (R n (F P1) (F P2)).
+Arguments ex_gen [n P1] P2 relP12.
+Lemma test_ex_gen (P1 P2 : A -> A -> B) (n : nat) :
+ (forall x y : A, P2 x y = P2 y x) ->
+ R n (F P1) (F P2) /\ True -> True.
+Proof.
+move=> P2C.
+under [X in R _ _ X]ex_gen => a b.
+ by rewrite P2C over.
+by move => _.
+Qed.
+End TestGeneric.
--
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.
---
.../proof-engine/ssreflect-proof-language.rst | 6 +--
doc/stdlib/hidden-files | 1 +
doc/stdlib/index-list.html.template | 1 +
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 ++++++++++++
test-suite/ssr/under.v | 18 +++++--
theories/Setoids/Setoid.v | 2 +
12 files changed, 179 insertions(+), 26 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
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 0af23354cc..3db771b0ba 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3756,9 +3756,9 @@ involves the following steps:
the corresponding intro pattern :n:`@i_pattern__i` in each goal.
4. Then :tacn:`under` checks that the first n subgoals
- are (quantified) Leibniz equalities or registered Setoid equalities
- between a term and an evar (e.g. ``m - m = ?F2 m`` in the running
- example).
+ are (quantified) Leibniz equalities, double implications or
+ registered Setoid equalities between a term and an evar
+ (e.g. ``m - m = ?F2 m`` in the running example).
5. If so :tacn:`under` protects these n goals against an
accidental instantiation of the evar.
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index 46175e37ed..4f8986984f 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -77,3 +77,4 @@ plugins/setoid_ring/Rings_Q.v
plugins/setoid_ring/Rings_R.v
plugins/setoid_ring/Rings_Z.v
plugins/setoid_ring/ZArithRing.v
+plugins/ssr/ssrsetoid.v
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index dcfe4a08f3..2673d8db82 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -602,6 +602,7 @@ through the Require Import command.
plugins/ssrmatching/ssrmatching.v
+ plugins/ssr/ssrclasses.v
plugins/ssr/ssreflect.v
plugins/ssr/ssrbool.v
plugins/ssr/ssrfun.v
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.
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index b1349f287a..7a723b2c5e 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -218,7 +218,6 @@ under Lub_Rbar_eqset => r.
by rewrite over.
Abort.
-
Lemma ex_iff R (P1 P2 : R -> Prop) :
(forall x : R, P1 x <-> P2 x) -> ((exists x, P1 x) <-> (exists x, P2 x)).
Proof.
@@ -227,17 +226,26 @@ Qed.
Arguments ex_iff [R P1] P2 iffP12.
-Require Import Setoid.
+(** Load the [setoid_rewrite] machinery *)
+Require Setoid.
+
+(** Replay the tactics from [test_Lub_Rbar] in this new environment *)
+Lemma test_Lub_Rbar_again (E : R -> Prop) :
+ Rbar_le Rbar0 (Lub_Rbar (fun x => x = R0 \/ E x)).
+Proof.
+under Lub_Rbar_eqset => r.
+by rewrite over.
+Abort.
Lemma test_ex_iff (P : nat -> Prop) : (exists x, P x) -> True.
-under ex_iff => n.
+under ex_iff => n. (* this requires [Setoid] *)
by rewrite over.
by move=> _.
Qed.
-
Section TestGeneric.
-Context {A B : Type} {R : nat -> relation B} `{!forall n : nat, Equivalence (R n)}.
+Context {A B : Type} {R : nat -> B -> B -> Prop}
+ `{!forall n : nat, RelationClasses.Equivalence (R n)}.
Variables (F : (A -> A -> B) -> B).
Hypothesis ex_gen : forall (n : nat) (P1 P2 : A -> A -> B),
(forall x y : A, R n (P1 x y) (P2 x y)) -> (R n (F P1) (F P2)).
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 2f8be5de12..ddc9967bfa 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -12,6 +12,8 @@ Require Export Coq.Classes.SetoidTactics.
Export Morphisms.ProperNotations.
+Require Coq.ssr.ssrsetoid.
+
(** For backward compatibility *)
Definition Setoid_Theory := @Equivalence.
--
cgit v1.2.3
From 05ae4be1258ed198949f886e83151fb41f7dedb1 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 7 Aug 2019 00:47:03 +0200
Subject: [ssr] under: Add a contrived example to test under/over with Setoids
* Borrow ideas from the Setoid refman documentation:
https://coq.inria.fr/refman/addendum/generalized-rewriting.html#first-class-setoids-and-morphisms
* Introduce a relation with the following signature:
[Rel : forall (m n : nat) (s : Setoid m n), car s -> car s -> Prop]
---
test-suite/ssr/under.v | 43 +++++++++++++++++++++++++++++++++++++++++++
1 file changed, 43 insertions(+)
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index 7a723b2c5e..2ef2690252 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -260,3 +260,46 @@ under [X in R _ _ X]ex_gen => a b.
by move => _.
Qed.
End TestGeneric.
+
+Import Setoid.
+(* to expose [Coq.Relations.Relation_Definitions.reflexive],
+ [Coq.Classes.RelationClasses.RewriteRelation], and so on. *)
+
+Section TestGeneric2.
+(* Some toy abstract example with a parameterized setoid type *)
+Record Setoid (m n : nat) : Type :=
+ { car : Type
+ ; Rel : car -> car -> Prop
+ ; refl : reflexive _ Rel
+ ; sym : symmetric _ Rel
+ ; trans : transitive _ Rel
+ }.
+
+Context {m n : nat}.
+Add Parametric Relation (s : Setoid m n) : (car s) (@Rel _ _ s)
+ reflexivity proved by (@refl _ _ s)
+ symmetry proved by (@sym _ _ s)
+ transitivity proved by (@trans _ _ s)
+ as eq_rel.
+
+Context {A : Type} {s1 s2 : Setoid m n}.
+
+Let B := @car m n s1.
+Let C := @car m n s2.
+Variable (F : C -> (A -> A -> B) -> C).
+Hypothesis rel2_gen :
+ forall (c1 c2 : C) (P1 P2 : A -> A -> B),
+ Rel c1 c2 ->
+ (forall a b : A, Rel (P1 a b) (P2 a b)) ->
+ Rel (F c1 P1) (F c2 P2).
+Arguments rel2_gen [c1] c2 [P1] P2 relc12 relP12.
+Lemma test_rel2_gen (c : C) (P : A -> A -> B)
+ (toy_hyp : forall a b, P a b = P b a) :
+ Rel (F c P) (F c (fun a b => P b a)).
+Proof.
+under [here in Rel _ here]rel2_gen.
+- over.
+- by move=> a b; rewrite toy_hyp over.
+- reflexivity.
+Qed.
+End TestGeneric2.
--
cgit v1.2.3
From d4e07328f7aed9d19e9b9a0f442e8fe85643073a Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 6 Aug 2019 23:34:07 +0200
Subject: [doc][ssr][under][setoid] Add changelog entry
---
doc/changelog/05-tactic-language/10022-ssr-under-setoid.rst | 6 ++++++
1 file changed, 6 insertions(+)
create mode 100644 doc/changelog/05-tactic-language/10022-ssr-under-setoid.rst
diff --git a/doc/changelog/05-tactic-language/10022-ssr-under-setoid.rst b/doc/changelog/05-tactic-language/10022-ssr-under-setoid.rst
new file mode 100644
index 0000000000..00b988ed4c
--- /dev/null
+++ b/doc/changelog/05-tactic-language/10022-ssr-under-setoid.rst
@@ -0,0 +1,6 @@
+- The :tacn:`under` and :tacn:`over` tactics can handle any registered
+ setoid equality (beyond mere double implications). See also Section
+ :ref:`under_ssr`. This generalized support for setoid equalities is
+ enabled as soon as we do both ``Require Import ssreflect.`` and
+ ``Require Setoid.`` (`#10022 `_,
+ by Erik Martin-Dorel, with suggestions and review by Enrico Tassi).
--
cgit v1.2.3
From 638dacdba06fb09898d57106f65afa1c88f5805d Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 10 Sep 2019 09:57:32 -0700
Subject: [ssr] Add test "do [under ... do ...] in H"
---
test-suite/ssr/under.v | 10 +++++++++-
1 file changed, 9 insertions(+), 1 deletion(-)
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index 2ef2690252..821683ca6d 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -160,7 +160,15 @@ Lemma test_big_occs (F G : nat -> nat) (n : nat) :
\sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0).
Proof.
under {2}[in RHS]eq_bigr => i Hi do rewrite muln0.
-by rewrite big_const_nat iter_addn_0.
+by rewrite big_const_nat iter_addn_0 mul0n addn0.
+Qed.
+
+Lemma test_big_occs_inH (F G : nat -> nat) (n : nat) :
+ \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0) -> True.
+Proof.
+move=> H.
+do [under {2}[in RHS]eq_bigr => i Hi do rewrite muln0] in H.
+by rewrite big_const_nat iter_addn_0 mul0n addn0 in H.
Qed.
(* Solely used, one such renaming is useless in practice, but it works anyway *)
--
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(+)
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 79df4c762ce0c04111957ef2b050aa087bf0a3b2 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sun, 20 Oct 2019 17:28:22 +0200
Subject: docs(changelog): Address @gares' comment
& Put the changelog entry in the proper folder
---
.../05-tactic-language/10022-ssr-under-setoid.rst | 6 ------
.../06-ssreflect/10022-ssr-under-setoid.rst | 21 +++++++++++++++++++++
2 files changed, 21 insertions(+), 6 deletions(-)
delete mode 100644 doc/changelog/05-tactic-language/10022-ssr-under-setoid.rst
create mode 100644 doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst
diff --git a/doc/changelog/05-tactic-language/10022-ssr-under-setoid.rst b/doc/changelog/05-tactic-language/10022-ssr-under-setoid.rst
deleted file mode 100644
index 00b988ed4c..0000000000
--- a/doc/changelog/05-tactic-language/10022-ssr-under-setoid.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- The :tacn:`under` and :tacn:`over` tactics can handle any registered
- setoid equality (beyond mere double implications). See also Section
- :ref:`under_ssr`. This generalized support for setoid equalities is
- enabled as soon as we do both ``Require Import ssreflect.`` and
- ``Require Setoid.`` (`#10022 `_,
- by Erik Martin-Dorel, with suggestions and review by Enrico Tassi).
diff --git a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst
new file mode 100644
index 0000000000..e9eab0924c
--- /dev/null
+++ b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst
@@ -0,0 +1,21 @@
+- Generalize tactics :tacn:`under` and :tacn:`over` for any registered
+ setoid equality. More precisely, assume the given context lemma has
+ type `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`.
+ The first step performed by :tacn:`under` (since Coq 8.10) amounts
+ to calling the tactic :tacn:`rewrite `, which
+ itself relies on :tacn:`setoid_rewrite` if need be. So this step was
+ already compatible with a double implication or setoid equality for
+ the conclusion head symbol `R2`. But a further step consists in
+ tagging the generated subgoal `R1 (f1 i) (?f2 i)` to protect it from
+ unwanted evar instantiation, and obtain a subgoal displayed as
+ ``'Under[ f1 i ]``. In Coq 8.10, this second (convenience) step was
+ only performed when `R1` was Leibniz' `eq` or `iff`. Now, it is also
+ performed for any relation `R1` which has a ``RewriteRelation``
+ instance as well as a ``RelationClasses.Reflexive`` instance. This
+ generalized support for setoid relations is enabled as soon as we do
+ both ``Require Import ssreflect.`` and ``Require Setoid.`` Finally,
+ a rewrite rule ``UnderE`` has been added if one wants to "unprotect"
+ the evar, and instantiate it manually with another rule than
+ reflexivity (i.e., without using :tacn:`over`). See also Section
+ :ref:`under_ssr` (`#10022 `_,
+ by Erik Martin-Dorel, with suggestions and review by Enrico Tassi).
--
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(-)
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 ++++++++---------------
test-suite/ssr/over.v | 8 ++--
4 files changed, 48 insertions(+), 114 deletions(-)
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));
diff --git a/test-suite/ssr/over.v b/test-suite/ssr/over.v
index 8232741b0d..267d981d05 100644
--- a/test-suite/ssr/over.v
+++ b/test-suite/ssr/over.v
@@ -12,7 +12,7 @@ assert (H : forall i : nat, i + 2 * i - i = x2 i).
unfold x2 in *; clear x2;
unfold R in *; clear R;
unfold I in *; clear I.
- apply Under_eq_from_eq.
+ apply Under_rel_from_rel.
Fail done.
over.
@@ -27,7 +27,7 @@ assert (H : forall i : nat, i + 2 * i - i = x2 i).
unfold x2 in *; clear x2;
unfold R in *; clear R;
unfold I in *; clear I.
- apply Under_eq_from_eq.
+ apply Under_rel_from_rel.
Fail done.
by rewrite over.
@@ -45,7 +45,7 @@ assert (H : forall i j, i + 2 * j - i = x2 i j).
unfold R in *; clear R;
unfold J in *; clear J;
unfold I in *; clear I.
- apply Under_eq_from_eq.
+ apply Under_rel_from_rel.
Fail done.
over.
@@ -61,7 +61,7 @@ assert (H : forall i j : nat, i + 2 * j - i = x2 i j).
unfold R in *; clear R;
unfold J in *; clear J;
unfold I in *; clear I.
- apply Under_eq_from_eq.
+ apply Under_rel_from_rel.
Fail done.
rewrite over.
--
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
---
.../06-ssreflect/10022-ssr-under-setoid.rst | 37 +++++---
doc/stdlib/hidden-files | 1 +
plugins/ssr/ssrclasses.v | 3 +
plugins/ssr/ssreflect.v | 68 ++------------
plugins/ssr/ssrsetoid.v | 103 +++++++++++++++++++--
plugins/ssr/ssrunder.v | 75 +++++++++++++++
test-suite/ssr/under.v | 69 ++++++++++++++
7 files changed, 275 insertions(+), 81 deletions(-)
create mode 100644 plugins/ssr/ssrunder.v
diff --git a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst
index e9eab0924c..5e005742fd 100644
--- a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst
+++ b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst
@@ -1,21 +1,28 @@
- Generalize tactics :tacn:`under` and :tacn:`over` for any registered
- setoid equality. More precisely, assume the given context lemma has
- type `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`.
- The first step performed by :tacn:`under` (since Coq 8.10) amounts
- to calling the tactic :tacn:`rewrite `, which
+ relation. More precisely, assume the given context lemma has type
+ `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`. The
+ first step performed by :tacn:`under` (since Coq 8.10) amounts to
+ calling the tactic :tacn:`rewrite `, which
itself relies on :tacn:`setoid_rewrite` if need be. So this step was
already compatible with a double implication or setoid equality for
the conclusion head symbol `R2`. But a further step consists in
tagging the generated subgoal `R1 (f1 i) (?f2 i)` to protect it from
- unwanted evar instantiation, and obtain a subgoal displayed as
- ``'Under[ f1 i ]``. In Coq 8.10, this second (convenience) step was
- only performed when `R1` was Leibniz' `eq` or `iff`. Now, it is also
- performed for any relation `R1` which has a ``RewriteRelation``
- instance as well as a ``RelationClasses.Reflexive`` instance. This
- generalized support for setoid relations is enabled as soon as we do
- both ``Require Import ssreflect.`` and ``Require Setoid.`` Finally,
- a rewrite rule ``UnderE`` has been added if one wants to "unprotect"
- the evar, and instantiate it manually with another rule than
- reflexivity (i.e., without using :tacn:`over`). See also Section
+ unwanted evar instantiation, and get `Under_rel _ R1 (f1 i) (?f2 i)`
+ that is displayed as ``'Under[ f1 i ]``. In Coq 8.10, this second
+ (convenience) step was only performed when `R1` was Leibniz' `eq` or
+ `iff`. Now, it is also performed for any relation `R1` which has a
+ ``RewriteRelation`` instance (a `RelationClasses.Reflexive` instance
+ being also needed so :tacn:`over` can discharge the ``'Under[ _ ]``
+ goal by instantiating the hidden evar.) Also, it is now possible to
+ manipulate `Under_rel _ R1 (f1 i) (?f2 i)` subgoals directly if `R1`
+ is a `PreOrder` relation or so, thanks to extra instances proving
+ that `Under_rel` preserves the properties of the `R1` relation.
+ These two features generalizing support for setoid-like relations is
+ enabled as soon as we do both ``Require Import ssreflect.`` and
+ ``Require Setoid.`` Finally, a rewrite rule ``UnderE`` has been
+ added if one wants to "unprotect" the evar, and instantiate it
+ manually with another rule than reflexivity (i.e., without using the
+ :tacn:`over` tactic nor the ``over`` rewrite rule). See also Section
:ref:`under_ssr` (`#10022 `_,
- by Erik Martin-Dorel, with suggestions and review by Enrico Tassi).
+ by Erik Martin-Dorel, with suggestions and review by Enrico Tassi
+ and Cyril Cohen).
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index 4f8986984f..6699252cee 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -77,4 +77,5 @@ plugins/setoid_ring/Rings_Q.v
plugins/setoid_ring/Rings_R.v
plugins/setoid_ring/Rings_Z.v
plugins/setoid_ring/ZArithRing.v
+plugins/ssr/ssrunder.v
plugins/ssr/ssrsetoid.v
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.
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index 821683ca6d..c12491138a 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -311,3 +311,72 @@ under [here in Rel _ here]rel2_gen.
- reflexivity.
Qed.
End TestGeneric2.
+
+Section TestPreOrder.
+(* inspired by https://github.com/coq/coq/pull/10022#issuecomment-530101950
+ but without needing to do [rewrite UnderE] manually. *)
+
+Require Import Morphisms.
+
+(** Tip to tell rewrite that the LHS of [leq' x y (:= leq x y = true)]
+ is x, not [leq x y] *)
+Definition rel_true {T} (R : rel T) x y := is_true (R x y).
+Definition leq' : nat -> nat -> Prop := rel_true leq.
+
+Parameter leq_add :
+ forall m1 m2 n1 n2 : nat, m1 <= n1 -> m2 <= n2 -> m1 + m2 <= n1 + n2.
+Parameter leq_mul :
+ forall m1 m2 n1 n2 : nat, m1 <= n1 -> m2 <= n2 -> m1 * m2 <= n1 * n2.
+
+Local Notation "+%N" := addn (at level 0, only parsing).
+
+(** Context lemma (could *)
+Lemma leq'_big : forall I (F G : I -> nat) (r : seq I),
+ (forall i : I, leq' (F i) (G i)) ->
+ (leq' (\big[+%N/0%N]_(i <- r) F i) (\big[+%N/0%N]_(i <- r) G i)).
+Proof.
+red=> F G m n HFG.
+apply: (big_ind2 leq _ _ (P := xpredT) (op1 := addn) (op2 := addn)) =>//.
+move=> *; exact: leq_add.
+move=> *; exact: HFG.
+Qed.
+
+(** Instances for [setoid_rewrite] *)
+Instance leq'_rr : RewriteRelation leq' := {}.
+
+Instance leq'_proper_addn : Proper (leq' ==> leq' ==> leq') addn.
+Proof. move=> a1 b1 le1 a2 b2 le2; exact/leq_add. Qed.
+
+Instance leq'_proper_muln : Proper (leq' ==> leq' ==> leq') muln.
+Proof. move=> a1 b1 le1 a2 b2 le2; exact/leq_mul. Qed.
+
+
+Instance leq'_preorder : PreOrder leq'.
+(** encompasses [Reflexive] *)
+Proof. rewrite /leq' /rel_true; split =>// ??? A B; exact: leq_trans A B. Qed.
+
+Instance leq'_reflexive : Reflexive leq'.
+Proof. by rewrite /leq' /rel_true. Qed.
+
+Parameter leq_add2l :
+ forall p m n : nat, (p + m <= p + n) = (m <= n).
+
+Lemma test : forall n : nat,
+ (1 + 2 * (\big[+%N/0]_(i < n) (3 + i)) * 4 + 5 <= 6 + 24 * n + 8 * n * n)%N.
+Proof.
+move=> n; rewrite -[is_true _]/(rel_true _ _ _) -/leq'.
+have lem : forall (i : nat), i < n -> leq' (3 + i) (3 + n).
+{ by move=> i Hi; rewrite /leq' /rel_true leq_add2l; apply/ltnW. }
+
+under leq'_big => i.
+{
+ (* The "magic" is here: instantiate the evar with the bound "3 + n" *)
+ rewrite lem ?ltn_ord //. over.
+}
+cbv beta.
+
+now_show (leq' (1 + 2 * \big[+%N/0]_(i < n) (3 + n) * 4 + 5) (6 + 24 * n + 8 * n * n)).
+(* uninteresting end of proof, omitted *)
+Abort.
+
+End TestPreOrder.
--
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
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
From f7c078d1a16a9554fb320a85b4c7d33499037484 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 1 Nov 2019 01:59:07 +0100
Subject: [ssr] Update doc for under w.r.t. setoid-like relations
---
doc/sphinx/proof-engine/ssreflect-proof-language.rst | 15 ++++++++++++---
1 file changed, 12 insertions(+), 3 deletions(-)
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 3db771b0ba..e70f9d7716 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3757,8 +3757,10 @@ involves the following steps:
4. Then :tacn:`under` checks that the first n subgoals
are (quantified) Leibniz equalities, double implications or
- registered Setoid equalities between a term and an evar
- (e.g. ``m - m = ?F2 m`` in the running example).
+ registered relations (w.r.t. Class ``RewriteRelation``) between a
+ term and an evar, e.g. ``m - m = ?F2 m`` in the running example.
+ (This support for setoid-like relations is enabled as soon as we do
+ both ``Require Import ssreflect.`` and ``Require Setoid.``)
5. If so :tacn:`under` protects these n goals against an
accidental instantiation of the evar.
@@ -3770,7 +3772,10 @@ involves the following steps:
by using a regular :tacn:`rewrite` tactic.
7. Interactive editing of the first n goals has to be signalled by
- using the :tacn:`over` tactic or rewrite rule (see below).
+ using the :tacn:`over` tactic or rewrite rule (see below), which
+ requires that the underlying relation is reflexive. (The running
+ example deals with Leibniz equality, but ``PreOrder`` relations are
+ also supported, for example.)
8. Finally, a post-processing step is performed in the main goal
to keep the name(s) for the bound variables chosen by the user in
@@ -3796,6 +3801,10 @@ displayed as ``'Under[ … ]``):
This is a variant of :tacn:`over` in order to close ``'Under[ … ]``
goals, relying on the ``over`` rewrite rule.
+Note that a rewrite rule ``UnderE`` is available as well, if one wants
+to "unprotect" the evar, without closing the goal automatically (e.g.,
+to instantiate it manually with another rule than reflexivity).
+
.. _under_one_liner:
One-liner mode
--
cgit v1.2.3