diff options
| author | Edward Wang | 2020-04-14 06:02:28 +0000 |
|---|---|---|
| committer | Edward Wang | 2020-09-07 05:53:55 +0000 |
| commit | d79c6b1de2a5b0efbe4d2e2c75b4a7c587df6767 (patch) | |
| tree | 9c40fc4ebd66e6d50bd09da101ee0eca294f6cfa | |
| parent | ad89d85911927f0e95df7a72fe51aec0ab964d94 (diff) | |
Add iff variants for other list lemmas
| -rw-r--r-- | theories/Lists/List.v | 16 |
1 files changed, 15 insertions, 1 deletions
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] *) (************************) |