1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
|
(************************************************************************)
(* * 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># **)
(** Compatibility layer for [under] and [setoid_rewrite].
This file is intended to be required by [Require Import Setoid].
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 : relation A},
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... *)
|
