From ad89d85911927f0e95df7a72fe51aec0ab964d94 Mon Sep 17 00:00:00 2001
From: Edward Wang
Date: Mon, 13 Apr 2020 18:14:44 -0400
Subject: Add iff variant for app_inj_tail

The lemma is true in the other direction and can be useful in proofs.
---
 theories/Lists/List.v | 31 +++++++++++++++++++------------
 1 file changed, 19 insertions(+), 12 deletions(-)

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index e0eae7c287..db98973a79 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -207,24 +207,31 @@ Section Facts.
     now destruct Heq as [[Heq1 Heq2]|[Heq1 Heq2]]; inversion_clear Heq2.
   Qed.
 
-  Lemma app_inj_tail :
-    forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] -> x = y /\ a = b.
+  Lemma app_inj_tail_iff :
+    forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] <-> x = y /\ a = b.
   Proof.
     induction x as [| x l IHl];
       [ destruct y as [| a l] | destruct y as [| a l0] ];
       simpl; auto.
-    - intros a b [= ].
-      auto.
-    - intros a0 b [= H1 H0].
-      apply app_cons_not_nil in H0 as [].
-    - intros a b [= H1 H0].
-      assert ([] = l ++ [a]) by auto.
-      apply app_cons_not_nil in H as [].
-    - intros a0 b [= <- H0].
-      destruct (IHl l0 a0 b H0) as (<-,<-).
-      split; auto.
+    - intros a b. split.
+      + intros [= ]. auto.
+      + intros [H0 H1]. subst. auto.
+    - intros a0 b. split.
+      + intros [= H1 H0]. apply app_cons_not_nil in H0 as [].
+      + intros [H0 H1]. inversion H0.
+    - intros a b. split.
+      + intros [= H1 H0]. assert ([] = l ++ [a]) by auto. apply app_cons_not_nil in H as [].
+      + intros [H0 H1]. inversion H0.
+    - intros a0 b. split.
+      + intros [= <- H0]. specialize (IHl l0 a0 b). apply IHl in H0. destruct H0. subst. split; auto.
+      + intros [H0 H1]. inversion H0. subst. auto.
   Qed.
 
+  Lemma app_inj_tail :
+    forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] -> x = y /\ a = b.
+  Proof.
+    apply app_inj_tail_iff.
+  Qed.
 
   (** Compatibility with other operations *)
 
-- 
cgit v1.2.3


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


From f2ba2ad48dfa72f293702f4f86565b12f0302d4b Mon Sep 17 00:00:00 2001
From: Edward Wang
Date: Mon, 7 Sep 2020 03:23:44 +0000
Subject: Add changelog entry

---
 doc/changelog/10-standard-library/12094-app_inj_tail.rst | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/10-standard-library/12094-app_inj_tail.rst

diff --git a/doc/changelog/10-standard-library/12094-app_inj_tail.rst b/doc/changelog/10-standard-library/12094-app_inj_tail.rst
new file mode 100644
index 0000000000..702fbb3d64
--- /dev/null
+++ b/doc/changelog/10-standard-library/12094-app_inj_tail.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Extend some list lemmas to both directions: `app_inj_tail_iff`, `app_inv_head_iff`, `app_inv_tail_iff`.
+  (`#12094 <https://github.com/coq/coq/pull/12094>`_,
+  fixes `#12093 <https://github.com/coq/coq/issues/12093>`_,
+  by Edward Wang).
-- 
cgit v1.2.3