From d79c6b1de2a5b0efbe4d2e2c75b4a7c587df6767 Mon Sep 17 00:00:00 2001
From: Edward Wang
Date: Tue, 14 Apr 2020 06:02:28 +0000
Subject: Add iff variants for other list lemmas

---
 theories/Lists/List.v | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index db98973a79..76633ab201 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -246,10 +246,18 @@ Section Facts.
     rewrite <- plus_n_Sm, plus_n_O; reflexivity.
   Qed.
 
+  Lemma app_inv_head_iff:
+   forall l l1 l2 : list A, l ++ l1 = l ++ l2 <-> l1 = l2.
+  Proof.
+    induction l; split; intros; simpl; auto.
+    - apply IHl. inversion H. auto.
+    - subst. auto.
+  Qed.
+
   Lemma app_inv_head:
    forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2.
   Proof.
-    induction l; simpl; auto; injection 1; auto.
+    apply app_inv_head_iff.
   Qed.
 
   Lemma app_inv_tail:
@@ -267,6 +275,12 @@ Section Facts.
     injection H as [= H H0]; f_equal; eauto.
   Qed.
 
+  Lemma app_inv_tail_iff:
+    forall l l1 l2 : list A, l1 ++ l = l2 ++ l <-> l1 = l2.
+  Proof.
+    split; [apply app_inv_tail | now intros ->].
+  Qed.
+
   (************************)
   (** *** Facts about [In] *)
   (************************)
-- 
cgit v1.2.3