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') 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 +++--- doc/stdlib/hidden-files | 1 + doc/stdlib/index-list.html.template | 1 + 3 files changed, 5 insertions(+), 3 deletions(-) (limited to 'doc') 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 -- 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 (limited to 'doc') 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 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 (limited to 'doc') 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 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 + 2 files changed, 23 insertions(+), 15 deletions(-) (limited to 'doc') 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 -- 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') 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