diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrsetoid.v | 86 |
1 files changed, 1 insertions, 85 deletions
diff --git a/plugins/ssr/ssrsetoid.v b/plugins/ssr/ssrsetoid.v index 609c9d5ab8..7c5cd135fe 100644 --- a/plugins/ssr/ssrsetoid.v +++ b/plugins/ssr/ssrsetoid.v @@ -18,9 +18,7 @@ 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). + This file's instances have priority 12 > other stdlib instances. (Note: this file could be skipped when porting [under] to stdlib2.) *) @@ -38,85 +36,3 @@ Instance compat_Reflexive : RelationClasses.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... *) |