Add iff variant for app_inj_tail

The lemma is true in the other direction and can be useful in proofs.

1 files 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 *)