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
|
(************************************************************************)
(* 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. Definitions on [Equivalence].
Author: Matthieu Sozeau
Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
91405 Orsay, France *)
(* $Id: Equivalence.v 11709 2008-12-20 11:42:15Z msozeau $ *)
Require Export Coq.Program.Basics.
Require Import Coq.Program.Tactics.
Require Import Coq.Classes.Init.
Require Import Relation_Definitions.
Require Import Coq.Classes.RelationClasses.
Require Export Coq.Classes.Morphisms.
Set Implicit Arguments.
Unset Strict Implicit.
Open Local Scope signature_scope.
Definition equiv `{Equivalence A R} : relation A := R.
(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.
Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.
Open Local Scope equiv_scope.
(** Overloading for [PER]. *)
Definition pequiv `{PER A R} : relation A := R.
(** Overloaded notation for partial equivalence. *)
Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
(** Shortcuts to make proof search easier. *)
Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv.
Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv.
Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
Next Obligation.
Proof.
transitivity y ; auto.
Qed.
(** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)
Ltac setoid_subst H :=
match type of H with
?x === ?y => substitute H ; clear H x
end.
Ltac setoid_subst_nofail :=
match goal with
| [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail
| _ => idtac
end.
(** [subst*] will try its best at substituting every equality in the goal. *)
Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail.
(** Simplify the goal w.r.t. equivalence. *)
Ltac equiv_simplify_one :=
match goal with
| [ H : ?x === ?x |- _ ] => clear H
| [ H : ?x === ?y |- _ ] => setoid_subst H
| [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name
| [ |- ~ ?x === ?y ] => let name:=fresh "Hneq" in intro name
end.
Ltac equiv_simplify := repeat equiv_simplify_one.
(** "reify" relations which are equivalences to applications of the overloaded [equiv] method
for easy recognition in tactics. *)
Ltac equivify_tac :=
match goal with
| [ s : Equivalence ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
| [ s : Equivalence ?A ?R |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
end.
Ltac equivify := repeat equivify_tac.
Section Respecting.
(** Here we build an equivalence instance for functions which relates respectful ones only,
we do not export it. *)
Definition respecting `(eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B)) : Type :=
{ morph : A -> B | respectful R R' morph morph }.
Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
Equivalence (fun (f g : respecting eqa eqb) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl.
Next Obligation.
Proof.
unfold respecting in *. program_simpl. transitivity (y y0); auto. apply H0. reflexivity.
Qed.
End Respecting.
(** The default equivalence on function spaces, with higher-priority than [eq]. *)
Program Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) :
Equivalence (pointwise_relation A eqB) | 9.
Next Obligation.
Proof.
transitivity (y a) ; auto.
Qed.
|
