Commit 287afa0d authored by Robbert Krebbers's avatar Robbert Krebbers

Simplify definition of type class for Leibniz <-> setoid equality.

parent e20e49c6
......@@ -177,21 +177,24 @@ Notation "(≡{ Γ1 , Γ2 , .. , Γ3 } )" := (equivE (pair .. (Γ1, Γ2) .. Γ3)
with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
setoid equalities into Leibniz equalities, and [unfold_leibniz] for the
reverse. *)
Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x y x = y.
Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x y x = y.
Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@equiv A _)} (x y : A) :
x y x = y.
Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed.
Ltac fold_leibniz := repeat
match goal with
| H : context [ @equiv ?A _ _ _ ] |- _ =>
setoid_rewrite (leibniz_equiv (A:=A)) in H
setoid_rewrite (leibniz_equiv_iff (A:=A)) in H
| |- context [ @equiv ?A _ _ _ ] =>
setoid_rewrite (leibniz_equiv (A:=A))
setoid_rewrite (leibniz_equiv_iff (A:=A))
end.
Ltac unfold_leibniz := repeat
match goal with
| H : context [ @eq ?A _ _ ] |- _ =>
setoid_rewrite <-(leibniz_equiv (A:=A)) in H
setoid_rewrite <-(leibniz_equiv_iff (A:=A)) in H
| |- context [ @eq ?A _ _ ] =>
setoid_rewrite <-(leibniz_equiv (A:=A))
setoid_rewrite <-(leibniz_equiv_iff (A:=A))
end.
Definition equivL {A} : Equiv A := (=).
......
......@@ -175,7 +175,7 @@ Proof.
Qed.
Instance coPset_leibniz : LeibnizEquiv coPset.
Proof.
intros X Y; split; [rewrite elem_of_equiv; intros HXY|by intros ->].
intros X Y; rewrite elem_of_equiv; intros HXY.
apply (sig_eq_pi _), coPset_eq; try apply proj2_sig.
intros p; apply eq_bool_prop_intro, (HXY p).
Qed.
......
......@@ -162,9 +162,8 @@ Section setoid.
Qed.
Global Instance map_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (M A).
Proof.
intros m1 m2; split.
* by intros Hm; apply map_eq; intros i; unfold_leibniz; apply lookup_proper.
* by intros <-; intros i; fold_leibniz.
intros m1 m2 Hm; apply map_eq; intros i.
by unfold_leibniz; apply lookup_proper.
Qed.
Lemma map_equiv_empty (m : M A) : m m = .
Proof.
......
......@@ -380,10 +380,7 @@ Section setoid.
by apply cons_equiv, IH.
Qed.
Global Instance list_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (list A).
Proof.
intros l1 l2; split; [|by intros <-].
induction 1; f_equal; fold_leibniz; auto.
Qed.
Proof. induction 1; f_equal; fold_leibniz; auto. Qed.
End setoid.
Global Instance: Injective2 (=) (=) (=) (@cons A).
......
......@@ -101,10 +101,7 @@ Section setoids.
Global Instance Some_proper : Proper (() ==> ()) (@Some A).
Proof. by constructor. Qed.
Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
Proof.
intros x y; split; [destruct 1; fold_leibniz; congruence|].
by intros <-; destruct x; constructor; fold_leibniz.
Qed.
Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed.
Lemma equiv_None (mx : option A) : mx None mx = None.
Proof. split; [by inversion_clear 1|by intros ->]. Qed.
Lemma equiv_Some (mx my : option A) x :
......
......@@ -364,7 +364,7 @@ Hint Extern 0 (@Equivalence _ (≡)) =>
Section partial_order.
Context `{SubsetEq A, !PartialOrder (@subseteq A _)}.
Global Instance: LeibnizEquiv A.
Proof. split. intros [??]. by apply (anti_symmetric ()). by intros ->. Qed.
Proof. intros ?? [??]; by apply (anti_symmetric ()). Qed.
End partial_order.
(** * Join semi lattices *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment