From fe93c1b7cb7484ec4fa3fbaf57f84958164067d2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Dec 2015 23:28:43 +0100
Subject: [PATCH] Simplify definition of type class for Leibniz <-> setoid
 equality.

---
 theories/base.v     | 15 +++++++++------
 theories/co_pset.v  |  2 +-
 theories/fin_maps.v |  5 ++---
 theories/list.v     |  5 +----
 theories/option.v   |  5 +----
 theories/orders.v   |  2 +-
 6 files changed, 15 insertions(+), 19 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 30ec9466..8e7817bc 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -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 := (=).
diff --git a/theories/co_pset.v b/theories/co_pset.v
index d00c218d..b0c65632 100644
--- a/theories/co_pset.v
+++ b/theories/co_pset.v
@@ -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.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index daaa5c69..46646c7d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -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.
diff --git a/theories/list.v b/theories/list.v
index 539388af..84c0b177 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -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).
diff --git a/theories/option.v b/theories/option.v
index ed262cfb..08bc2bc6 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -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 :
diff --git a/theories/orders.v b/theories/orders.v
index 2a8b1424..a8b7f2d2 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -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 *)
-- 
GitLab