Merge PR #12094: Extend app_inj_tail and other list lemmas

Reviewed-by: anton-trunov
Ack-by: herbelin

2 files changed, 39 insertions, 13 deletions

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).
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index e0eae7c287..76633ab201 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 *)
 
@@ -239,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:
@@ -260,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] *)
   (************************)