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. --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'doc/sphinx/proof-engine') 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. -- 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. --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc/sphinx/proof-engine') 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. -- 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(-) (limited to 'doc/sphinx/proof-engine') 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