diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-16 18:37:36 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-16 18:44:44 +0200 |
| commit | 925f6ae9d1b7a1a893960740fb9ffc0c2c52aa27 (patch) | |
| tree | 48076164098f24b3332a91bd849f76cc412332a5 /kvx | |
| parent | 835feeaad46abe968713c39fbcd7c6a3e6fb31f4 (diff) | |
| download | compcert-kvx-925f6ae9d1b7a1a893960740fb9ffc0c2c52aa27.tar.gz compcert-kvx-925f6ae9d1b7a1a893960740fb9ffc0c2c52aa27.zip | |
replace exec_body_simulation_star' by exec_body_simulation_plus_gen
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/lib/IterList.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/kvx/lib/IterList.v b/kvx/lib/IterList.v index b9eb5922..49beb1c5 100644 --- a/kvx/lib/IterList.v +++ b/kvx/lib/IterList.v @@ -82,4 +82,15 @@ Proof. destruct (le_lt_dec n (List.length l)); try omega. intros; exploit (iter_tail_inject1 n (length l) l); try omega. rewrite iter_tail_reach_nil. auto. -Qed.
\ No newline at end of file +Qed. + +Lemma list_length_z_nat (A: Type) (l: list A): list_length_z l = Z.of_nat (length l). +Proof. + induction l; auto. + rewrite list_length_z_cons. simpl. rewrite Zpos_P_of_succ_nat. omega. +Qed. + +Lemma list_length_nat_z (A: Type) (l: list A): length l = Z.to_nat (list_length_z l). +Proof. + intros; rewrite list_length_z_nat, Nat2Z.id. auto. +Qed. |