diff options
| author | letouzey | 2009-07-24 13:35:13 +0000 |
|---|---|---|
| committer | letouzey | 2009-07-24 13:35:13 +0000 |
| commit | a666838951f9c53cd85c9d72474aa598ffe02a1e (patch) | |
| tree | e5d34a14ab3fa7384ff2f4d6ee66b70571c27324 | |
| parent | 7b15f852051889165d5f12a769a5d58349f693c2 (diff) | |
List: add a iff-based lemma about In and ++
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12249 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Lists/List.v | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 34a9723475..7e9711bba5 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -316,7 +316,12 @@ Section Facts. now_show (H = a \/ In a (y ++ m)). elim H2; auto. Qed. - + + Lemma in_app_iff : forall l l' (a:A), In a (l++l') <-> In a l \/ In a l'. + Proof. + split; auto using in_app_or, in_or_app. + Qed. + Lemma app_inv_head: forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2. Proof. @@ -1853,7 +1858,7 @@ End NatSeq. (** * Exporting hints and tactics *) -Hint Rewrite +Hint Rewrite rev_involutive (* rev (rev l) = l *) rev_unit (* rev (l ++ a :: nil) = a :: rev l *) map_nth (* nth n (map f l) (f d) = f (nth n l d) *) @@ -1861,9 +1866,6 @@ Hint Rewrite seq_length (* length (seq start len) = len *) app_length (* length (l ++ l') = length l + length l' *) rev_length (* length (rev l) = length l *) - : list. - -Hint Rewrite -> app_nil_r (* l ++ nil = l *) : list. |