From ece8843f95a28c3ac123cda70c9a870a90a37b85 Mon Sep 17 00:00:00 2001 From: Sébastien Hinderer Date: Wed, 17 Dec 2014 15:13:32 +0100 Subject: Adds two lemmas about hderror to the List standard library. --- theories/Lists/List.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'theories/Lists') diff --git a/theories/Lists/List.v b/theories/Lists/List.v index da851aae0..c004b156b 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -87,6 +87,18 @@ Section Facts. left; exists a, tail; reflexivity. Qed. + Lemma hd_error_tl_repr : forall l (a:A) r, + hd_error l = Some a /\ tl l = r <-> l = a :: r. + Proof. destruct l as [|x xs]. + - unfold hd_error, tl; intros a r. split; firstorder discriminate. + - intros. simpl. split. + * intros (H1, H2). inversion H1. rewrite H2. reflexivity. + * inversion 1. subst. auto. + Qed. + + Lemma hd_error_some_nil : forall l (a:A), hd_error l = Some a -> l <> nil. + Proof. unfold hd_error. destruct l; now discriminate. Qed. + Theorem length_zero_iff_nil (l : list A): length l = 0 <-> l=[]. Proof. -- cgit v1.2.3