From f2fc2ac70aeceec2f3f7137acba5c0bf7a342a17 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Sun, 22 Aug 2021 00:41:55 +0100 Subject: Move list lemmas to own file --- src/common/ListExtra.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 src/common/ListExtra.v (limited to 'src/common') diff --git a/src/common/ListExtra.v b/src/common/ListExtra.v new file mode 100644 index 0000000..6b14a50 --- /dev/null +++ b/src/common/ListExtra.v @@ -0,0 +1,27 @@ +Require Export Coq.Lists.List. + +Require Import Coq.micromega.Lia. +Require Import vericert.common.Vericertlib. + +From Hammer Require Import Tactics. + +Lemma nth_error_length : forall {A} (l : list A) n x, + nth_error l n = Some x -> (n < length l)%nat. +Proof. + induction l; intros; simpl in *. + - destruct n; crush. + - destruct n; crush. + edestruct IHl; eauto with arith. +Qed. + +Lemma length_nth_error : forall {A} (l : list A) n, + (n < length l)%nat -> exists x, nth_error l n = Some x. +Proof. + induction l; intros; simpl in *. + - lia. + - destruct n; crush; eauto with arith. +Qed. + +Lemma combine_split : forall {A B} (l : list (A * B)), + List.combine (fst (List.split l)) (snd (List.split l)) = l. +Proof. hfcrush use: split_combine unfold: fst, snd inv: prod. Qed. -- cgit