diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-29 16:13:24 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-29 16:13:24 +0100 |
| commit | c10635f9e6890a6171c5c1cc8eb6e3298d2006b1 (patch) | |
| tree | a5f0e39431138796d297913b37578f758a45257f /src/common | |
| parent | 0c5c896490ee0d4b553f26d00b2ad2a971d25d4f (diff) | |
| download | vericert-c10635f9e6890a6171c5c1cc8eb6e3298d2006b1.tar.gz vericert-c10635f9e6890a6171c5c1cc8eb6e3298d2006b1.zip | |
Prove more admitted theorems
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/NonEmpty.v | 21 |
1 files changed, 21 insertions, 0 deletions
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. |