From 5912f8b1487d1e9547a34e11afbfdd5f465c5ffc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 30 Sep 2014 16:17:41 -0400
Subject: [PATCH] Let simplify_equality perform injection less eagerly.

Now it only performs injection on hypotheses of the shape f .. = f ..
---
 theories/base.v            |  1 +
 theories/error.v           |  6 ++++--
 theories/fin_collections.v |  2 +-
 theories/fin_maps.v        |  2 +-
 theories/finite.v          |  6 +++---
 theories/list.v            | 11 +++++------
 theories/natmap.v          |  8 ++++----
 theories/nmap.v            |  5 ++---
 theories/option.v          |  3 +++
 theories/stringmap.v       |  2 +-
 theories/tactics.v         |  7 ++++++-
 theories/zmap.v            |  2 +-
 12 files changed, 32 insertions(+), 23 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index a3aaf528..2ff07170 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -940,3 +940,4 @@ Section sig_map.
     apply (injective f) in Hxy; subst. rewrite (proof_irrel _ Hy). auto.
   Qed.
 End sig_map.
+Arguments sig_map _ _ _ _ _ _ !_ /.
diff --git a/theories/error.v b/theories/error.v
index 26c15ec1..d89d3eeb 100644
--- a/theories/error.v
+++ b/theories/error.v
@@ -41,6 +41,9 @@ Tactic Notation "case_error_guard" :=
 Tactic Notation "simplify_error_equality" :=
   repeat match goal with
   | _ => progress simplify_equality'
+  | H : appcontext [@mret (sum ?E) _ ?A] |- _ =>
+     change (@mret (sum E) _ A) with (@inr E A) in H
+  | |- appcontext [@mret (sum ?E) _ ?A] => change (@mret _ _ A) with (@inr E A)
   | H : error_of_option ?o ?e = ?x |- _ => apply error_of_option_inr in H
   | H : mbind (M:=sum _) ?f ?o = ?x |- _ =>
     apply bind_inr in H; destruct H as (?&?&?)
@@ -71,8 +74,7 @@ Section mapM.
   Proof.
     revert k. induction l as [|x l]; intros [|y k]; simpl; try done.
     * destruct (f x); simpl; [discriminate|]. by destruct (mapM f l).
-    * destruct (f x) eqn:?; simpl; [discriminate|].
-      destruct (mapM f l); intros; simplify_equality. constructor; auto.
+    * destruct (f x) eqn:?; intros; simplify_error_equality; auto.
   Qed.
   Lemma mapM_inr_2 l k : Forall2 (λ x y, f x = inr y) l k → mapM f l = inr k.
   Proof.
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 26ed4ae4..33ad27ec 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -49,7 +49,7 @@ Qed.
 Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
 Proof.
   unfold size, collection_size. simpl. rewrite <-!elem_of_elements.
-  generalize (elements X). intros [|? l]; intro; simplify_equality.
+  generalize (elements X). intros [|? l]; intro; simplify_equality'.
   rewrite (nil_length_inv l), !elem_of_list_singleton by done. congruence.
 Qed.
 Lemma collection_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index e0966cc0..a91b201f 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -734,7 +734,7 @@ Proof.
   split.
   * intros Hm i P'; rewrite lookup_merge by done; intros.
     specialize (Hm i). destruct (m1 !! i), (m2 !! i);
-      simplify_equality; auto using bool_decide_pack.
+      simplify_equality'; auto using bool_decide_pack.
   * intros Hm i. specialize (Hm i). rewrite lookup_merge in Hm by done.
     destruct (m1 !! i), (m2 !! i); simplify_equality'; auto;
       by eapply bool_decide_unpack, Hm.
diff --git a/theories/finite.v b/theories/finite.v
index 48056ab8..2315bdc0 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -164,7 +164,7 @@ Section enc_finite.
   Next Obligation.
     apply NoDup_alt. intros i j x. rewrite !list_lookup_fmap. intros Hi Hj.
     destruct (seq _ _ !! i) as [i'|] eqn:Hi',
-      (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_equality.
+      (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_equality'.
     destruct (lookup_seq_inv _ _ _ _ Hi'), (lookup_seq_inv _ _ _ _ Hj'); subst.
     rewrite <-(to_of_nat i), <-(to_of_nat j) by done. by f_equal.
   Qed.
@@ -272,10 +272,10 @@ Next Obligation.
   apply NoDup_app; split_ands.
   * by apply (NoDup_fmap_2 _).
   * intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
-    intros ([k2 Hk2]&?&?) Hxk2; simplify_equality. destruct Hx. revert Hxk2.
+    intros ([k2 Hk2]&?&?) Hxk2; simplify_equality'. destruct Hx. revert Hxk2.
     induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
     rewrite elem_of_app, elem_of_list_fmap, elem_of_cons.
-    intros [([??]&?&?)|?]; simplify_equality; auto.
+    intros [([??]&?&?)|?]; simplify_equality'; auto.
   * apply IH.
 Qed.
 Next Obligation.
diff --git a/theories/list.v b/theories/list.v
index d7ead777..f1cc4701 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1253,7 +1253,7 @@ Lemma prefix_of_cons_inv_1 x y l1 l2 : x :: l1 `prefix_of` y :: l2 → x = y.
 Proof. by intros [k ?]; simplify_equality'. Qed.
 Lemma prefix_of_cons_inv_2 x y l1 l2 :
   x :: l1 `prefix_of` y :: l2 → l1 `prefix_of` l2.
-Proof. intros [k ?]; simplify_equality. by exists k. Qed.
+Proof. intros [k ?]; simplify_equality'. by exists k. Qed.
 Lemma prefix_of_app k l1 l2 : l1 `prefix_of` l2 → k ++ l1 `prefix_of` k ++ l2.
 Proof. intros [k' ->]. exists k'. by rewrite (associative_L (++)). Qed.
 Lemma prefix_of_app_alt k1 k2 l1 l2 :
@@ -1407,7 +1407,7 @@ Lemma suffix_of_cons_inv l1 l2 x y :
   x :: l1 `suffix_of` y :: l2 → x :: l1 = y :: l2 ∨ x :: l1 `suffix_of` l2.
 Proof.
   intros [[|? k] E]; [by left|].
-  right. simplify_equality. by apply suffix_of_app_r.
+  right. simplify_equality'. by apply suffix_of_app_r.
 Qed.
 Lemma suffix_of_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2.
 Proof. intros [? ->]. rewrite app_length. lia. Qed.
@@ -2463,7 +2463,7 @@ Section fmap.
     (f <$> l) !! i = Some x → ∃ y, x = f y ∧ l !! i = Some y.
   Proof.
     intros Hi. rewrite list_lookup_fmap in Hi.
-    destruct (l !! i) eqn:?; simplify_equality; eauto.
+    destruct (l !! i) eqn:?; simplify_equality'; eauto.
   Qed.
   Lemma list_alter_fmap (g : A → A) (h : B → B) l i :
     Forall (λ x, f (g x) = h (f x)) l → f <$> alter g i l = alter h i (f <$> l).
@@ -2652,8 +2652,7 @@ Section mapM.
   Proof.
     revert k. induction l as [|x l]; intros [|y k]; simpl; try done.
     * destruct (f x); simpl; [|discriminate]. by destruct (mapM f l).
-    * destruct (f x) eqn:?; simpl; [|discriminate].
-      destruct (mapM f l); intros; simplify_equality. constructor; auto.
+    * destruct (f x) eqn:?; intros; simplify_option_equality; auto.
   Qed.
   Lemma mapM_Some_2 l k : Forall2 (λ x y, f x = Some y) l k → mapM f l = Some k.
   Proof.
@@ -3229,7 +3228,7 @@ Ltac simplify_suffix_of := repeat
   | H : suffix_of ?x ?x |- _ => clear H
   | H : suffix_of ?x (_ :: ?x) |- _ => clear H
   | H : suffix_of ?x (_ ++ ?x) |- _ => clear H
-  | _ => progress simplify_equality
+  | _ => progress simplify_equality'
   end.
 
 (** The [solve_suffix_of] tactic tries to solve goals involving [suffix_of]. It
diff --git a/theories/natmap.v b/theories/natmap.v
index f609b05b..b498d2cb 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -171,10 +171,10 @@ Proof.
   * intros (i'&?&Hi'). subst. revert i' j Hi'.
     induction l as [|[y|] l IH]; intros i j ?; simpl.
     + done.
-    + destruct i as [|i]; simplify_equality; [left|].
-      right. rewrite Nat.add_succ_comm. by apply (IH i (S j)).
-    + destruct i as [|i]; simplify_equality.
-      rewrite Nat.add_succ_comm. by apply (IH i (S j)).
+    + destruct i as [|i]; simplify_equality'; [left|].
+      right. rewrite <-Nat.add_succ_r. by apply (IH i (S j)).
+    + destruct i as [|i]; simplify_equality'.
+      rewrite <-Nat.add_succ_r. by apply (IH i (S j)).
 Qed.
 Lemma natmap_elem_of_to_list_raw {A} (l : natmap_raw A) i x :
   (i,x) ∈ natmap_to_list_raw 0 l ↔ mjoin (l !! i) = Some x.
diff --git a/theories/nmap.v b/theories/nmap.v
index 37e71d37..5f78de7a 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -63,10 +63,9 @@ Proof.
   * intros ? t i x. unfold map_to_list. split.
     + destruct t as [[y|] t]; simpl.
       - rewrite elem_of_cons, elem_of_list_fmap.
-        intros [? | [[??] [??]]]; simplify_equality; simpl; [done |].
+        intros [? | [[??] [??]]]; simplify_equality'; [done |].
         by apply elem_of_map_to_list.
-      - rewrite elem_of_list_fmap.
-        intros [[??] [??]]; simplify_equality; simpl.
+      - rewrite elem_of_list_fmap; intros [[??] [??]]; simplify_equality'.
         by apply elem_of_map_to_list.
     + destruct t as [[y|] t]; simpl.
       - rewrite elem_of_cons, elem_of_list_fmap.
diff --git a/theories/option.v b/theories/option.v
index 705961d8..255652d6 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -209,6 +209,9 @@ Tactic Notation "simpl_option_monad" "by" tactic3(tac) :=
       assert (o = Some x') as H by tac
     | assert (o = None) as H by tac ]
   in repeat match goal with
+  | H : appcontext [@mret _ _ ?A] |- _ =>
+     change (@mret _ _ A) with (@Some A) in H
+  | |- appcontext [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A)
   | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
     let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
   | H : context [fmap (M:=option) (A:=?A) ?f ?o] |- _ =>
diff --git a/theories/stringmap.v b/theories/stringmap.v
index dd8fa2b2..104199a3 100644
--- a/theories/stringmap.v
+++ b/theories/stringmap.v
@@ -141,7 +141,7 @@ Proof.
     apply bool_decide_unpack, map_Forall_to_list in Hm; revert Hm.
     induction (NoDup_map_to_list m) as [|[p x] l Hpx];
       inversion 1 as [|??? Hm']; simplify_equality'; constructor; eauto.
-    rewrite elem_of_list_fmap; intros ([p' x']&?&?); simplify_equality.
+    rewrite elem_of_list_fmap; intros ([p' x']&?&?); simplify_equality'.
     cut (string_to_pos (string_of_pos p') = p'); [congruence|].
     rewrite Forall_forall in Hm'. eapply (Hm' (_,_)); eauto.
   * intros A [m Hm] s x; unfold map_to_list, lookup; simpl.
diff --git a/theories/tactics.v b/theories/tactics.v
index 8f63a7c7..95d310ba 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -205,7 +205,12 @@ Ltac simplify_equality := repeat
   | H : ?f _ = ?f _ |- _ => apply (injective f) in H
   | H : ?f _ _ = ?f _ _ |- _ => apply (injective2 f) in H; destruct H
     (* before [injection'] to circumvent bug #2939 in some situations *)
-  | H : _ = _ |- _ => injection' H
+  | H : ?f _ = ?f _ |- _ => injection' H
+  | H : ?f _ _ = ?f _ _ |- _ => injection' H
+  | H : ?f _ _ _ = ?f _ _ _ |- _ => injection' H
+  | H : ?f _ _ _ _ = ?f _ _ _ _ |- _ => injection' H
+  | H : ?f _ _ _ _ _ = ?f _ _ _ _ _ |- _ => injection' H
+  | H : ?f _ _ _ _ _ _ = ?f _ _ _ _ _ _ |- _ => injection' H
   | H : ?x = ?x |- _ => clear H
     (* unclear how to generalize the below *)
   | H1 : ?o = Some ?x, H2 : ?o = Some ?y |- _ =>
diff --git a/theories/zmap.v b/theories/zmap.v
index ac098a51..b41228d3 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -73,7 +73,7 @@ Proof.
   * intros ? t i x. unfold map_to_list. split.
     + destruct t as [[y|] t t']; simpl.
       - rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap.
-        intros [?|[[[??][??]]|[[??][??]]]]; simplify_equality; simpl; [done| |];
+        intros [?|[[[??][??]]|[[??][??]]]]; simplify_equality'; [done| |];
           by apply elem_of_map_to_list.
       - rewrite elem_of_app, !elem_of_list_fmap. intros [[[??][??]]|[[??][??]]];
           simplify_equality'; by apply elem_of_map_to_list.
-- 
GitLab