blob: 6b14a50fecac69ad98772f23ca1e3989c0f8b5da (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
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.
|
