diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-22 00:41:55 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-22 00:41:55 +0100 |
commit | f2fc2ac70aeceec2f3f7137acba5c0bf7a342a17 (patch) | |
tree | 4fdfd1eb539e6a50d5ce2f66bd595a6a0112fe43 | |
parent | 1d52421edaec304a9a9e3c5a368af7af31e9ff3c (diff) | |
download | vericert-f2fc2ac70aeceec2f3f7137acba5c0bf7a342a17.tar.gz vericert-f2fc2ac70aeceec2f3f7137acba5c0bf7a342a17.zip |
Move list lemmas to own file
-rw-r--r-- | src/common/ListExtra.v | 27 | ||||
-rw-r--r-- | src/hls/HTLgenspec.v | 22 |
2 files changed, 28 insertions, 21 deletions
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. diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 4e9c072..934f3f4 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -27,6 +27,7 @@ Require Import compcert.lib.Maps. Require compcert.verilog.Op. Require Import vericert.common.Vericertlib. +Require Import vericert.common.ListExtra. Require Import vericert.hls.Verilog. Require Import vericert.hls.ValueInt. Require Import vericert.hls.HTL. @@ -345,27 +346,6 @@ Lemma map_externctrl_params_spec : forall args n param_pairs fn s s' i, Proof. sauto use: helper__map_externctrl_params_spec. Qed. Hint Resolve map_externctrl_params_spec : htlspec. -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. - Lemma iter_expand_instr_spec : forall l prog fin rtrn stack s s' i x c, HTLMonadExtra.collectlist (transf_instr (Globalenvs.Genv.globalenv prog) fin rtrn stack) l s = OK x s' i -> |