From c10635f9e6890a6171c5c1cc8eb6e3298d2006b1 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 29 May 2023 16:13:24 +0100 Subject: Prove more admitted theorems --- src/common/NonEmpty.v | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'src/common') diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v index 2c3ae94..7b10ee0 100644 --- a/src/common/NonEmpty.v +++ b/src/common/NonEmpty.v @@ -305,3 +305,24 @@ Proof. + constructor. eapply H. constructor; tauto. eapply IHl. intros. eapply H. constructor; tauto. Qed. + +Lemma filter_None : + forall A f (x: non_empty A), + filter f x = None -> + Forall (fun x => f x = false) x. +Proof. + induction x; cbn; intros. + - constructor. destruct_match; now auto. + - constructor. destruct_match; auto. destruct_match; try discriminate. + destruct_match; eauto. now destruct_match. +Qed. + +Lemma In_map : + forall A B (f: A -> B) n (x: A), + In x n -> + In (f x) (map f n). +Proof. + induction n; inversion 1; subst; cbn in *. + - constructor. + - clear H. inv H1; intuition (constructor; auto). +Qed. -- cgit