diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 94f93736..bd22371a 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -2300,6 +2300,18 @@ simpl. auto with zarith. Qed. +Definition vec_concat {T m n} (v : vec T m) (w : vec T n) : vec T (m + n). +refine (existT _ (projT1 v ++ projT1 w) _). +destruct v. +destruct w. +simpl. +unfold length_list in *. +rewrite <- e, <- e0. +rewrite app_length. +rewrite Nat2Z.inj_add. +reflexivity. +Defined. + Lemma skipn_length {A n} {l: list A} : (n <= List.length l -> List.length (skipn n l) = List.length l - n)%nat. revert l. induction n. |