Library Coq.Classes.SetoidClass
Typeclass-based setoids, tactics and standard instances.
Author: Matthieu Sozeau
Institution: LRI, CNRS UMR 8623 - University Paris Sud
A setoid wraps an equivalence.
Shortcuts to make proof search easier.
Standard setoids.
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 " := (
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 :=
lazymatch 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.
Lemma equiv_nequiv_trans :
forall `{
Setoid A} (
x y z :
A),
x == y ->
y =/= z ->
x =/= z.
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.
Partial setoids don't require reflexivity so we can build a partial setoid on the function space.
Overloaded notation for partial setoid equivalence.
Infix "=~=" :=
pequiv (
at level 70,
no associativity) :
type_scope.
Reset the default Program tactic.
Obligation Tactic := program_simpl.