Library Coq.Classes.Equivalence
Typeclass-based setoids. Definitions on Equivalence.
Author: Matthieu Sozeau
Institution: LRI, CNRS UMR 8623 - University Paris Sud
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.
Local Open Scope equiv_scope.
Overloading for PER.
Overloaded notation for partial equivalence.
Infix "=~=" :=
pequiv (
at level 70,
no associativity) :
equiv_scope.
Shortcuts to make proof search easier.
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.
The default equivalence on function spaces, with higher priority than eq.