diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrclasses.v | 3 | ||||
| -rw-r--r-- | plugins/ssr/ssreflect.v | 68 | ||||
| -rw-r--r-- | plugins/ssr/ssrsetoid.v | 103 | ||||
| -rw-r--r-- | plugins/ssr/ssrunder.v | 75 |
4 files changed, 183 insertions, 66 deletions
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 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **) + +(** 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. |