Commit fe93c1b7 authored by Robbert Krebbers's avatar Robbert Krebbers

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

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