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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
|
(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Typeclass-based setoids, tactics and standard instances.
Author: Matthieu Sozeau
Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
91405 Orsay, France *)
(* $Id: SetoidClass.v 11282 2008-07-28 11:51:53Z msozeau $ *)
Set Implicit Arguments.
Unset Strict Implicit.
Require Import Coq.Program.Program.
Require Import Coq.Classes.Init.
Require Export Coq.Classes.RelationClasses.
Require Export Coq.Classes.Morphisms.
Require Import Coq.Classes.Functions.
(** A setoid wraps an equivalence. *)
Class Setoid A :=
equiv : relation A ;
setoid_equiv :> Equivalence A equiv.
Typeclasses unfold equiv.
(* Too dangerous instance *)
(* Program Instance [ eqa : Equivalence A eqA ] => *)
(* equivalence_setoid : Setoid A := *)
(* equiv := eqA ; setoid_equiv := eqa. *)
(** Shortcuts to make proof search easier. *)
Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
Proof. typeclasses eauto. Qed.
Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv.
Proof. typeclasses eauto. Qed.
Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
Proof. typeclasses eauto. Qed.
Existing Instance setoid_refl.
Existing Instance setoid_sym.
Existing Instance setoid_trans.
(** Standard setoids. *)
(* Program Instance eq_setoid : Setoid A := *)
(* equiv := eq ; setoid_equiv := eq_equivalence. *)
Program Instance iff_setoid : Setoid Prop :=
equiv := iff ; setoid_equiv := iff_equivalence.
(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
(** Subset objects should be first coerced to their underlying type, but that notation doesn't work in the standard case then. *)
(* Notation " x == y " := (equiv (x :>) (y :>)) (at level 70, no associativity) : type_scope. *)
Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope.
Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : type_scope.
(** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
Ltac clsubst H :=
match type of H with
?x == ?y => substitute H ; clear H x
end.
Ltac clsubst_nofail :=
match goal with
| [ H : ?x == ?y |- _ ] => clsubst H ; clsubst_nofail
| _ => idtac
end.
(** [subst*] will try its best at substituting every equality in the goal. *)
Tactic Notation "clsubst" "*" := clsubst_nofail.
Lemma nequiv_equiv_trans : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z.
Proof with auto.
intros; intro.
assert(z == y) by (symmetry ; auto).
assert(x == y) by (transitivity z ; eauto).
contradiction.
Qed.
Lemma equiv_nequiv_trans : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z.
Proof.
intros; intro.
assert(y == x) by (symmetry ; auto).
assert(y == z) by (transitivity x ; eauto).
contradiction.
Qed.
Ltac setoid_simplify_one :=
match goal with
| [ H : (?x == ?x)%type |- _ ] => clear H
| [ H : (?x == ?y)%type |- _ ] => clsubst H
| [ |- (?x =/= ?y)%type ] => let name:=fresh "Hneq" in intro name
end.
Ltac setoid_simplify := repeat setoid_simplify_one.
Ltac setoidify_tac :=
match goal with
| [ s : Setoid ?A, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
| [ s : Setoid ?A |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
end.
Ltac setoidify := repeat setoidify_tac.
(** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv ++> iff) equiv :=
PER_morphism.
(** Add this very useful instance in the database. *)
Implicit Arguments setoid_morphism [[!sa]].
Existing Instance setoid_morphism.
Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) :=
Reflexive_partial_app_morphism.
Existing Instance setoid_partial_app_morphism.
Definition type_eq : relation Type :=
fun x y => x = y.
Program Instance type_equivalence : Equivalence Type type_eq.
Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
Ltac obligation_tactic ::= morphism_tac.
(** These are morphisms used to rewrite at the top level of a proof,
using [iff_impl_id_morphism] if the proof is in [Prop] and
[eq_arrow_id_morphism] if it is in Type. *)
Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) Basics.id.
(* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *)
(* Definition compose_respect (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
(* (x y : A -> C) : Prop := forall (f : A -> B) (g : B -> C), R f f -> R' g g. *)
(* Program Instance (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
(* [ mg : ? Morphism R' g ] [ mf : ? Morphism R f ] => *)
(* compose_morphism : ? Morphism (compose_respect R R') (g o f). *)
(* Next Obligation. *)
(* Proof. *)
(* apply (respect (m0:=mg)). *)
(* apply (respect (m0:=mf)). *)
(* assumption. *)
(* Qed. *)
(** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *)
Class PartialSetoid (carrier : Type) :=
pequiv : relation carrier ;
pequiv_prf :> PER carrier pequiv.
(** Overloaded notation for partial setoid equivalence. *)
Infix "=~=" := pequiv (at level 70, no associativity) : type_scope.
(** Reset the default Program tactic. *)
Ltac obligation_tactic ::= program_simpl.
|
