diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-19 12:51:39 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-19 12:51:39 +0100 |
| commit | 3be880b441a4d2926c6b14b7bb25a04209fbbca6 (patch) | |
| tree | f5d3ed38b3d4494d0ef75de77cbfc072f88a9022 /src/hls/AbstrSemIdent.v | |
| parent | bc2c535af4288e06f285658ef2844aa45da9b302 (diff) | |
| download | vericert-3be880b441a4d2926c6b14b7bb25a04209fbbca6.tar.gz vericert-3be880b441a4d2926c6b14b7bb25a04209fbbca6.zip | |
Finish evaluability proof of RBop
Diffstat (limited to 'src/hls/AbstrSemIdent.v')
| -rw-r--r-- | src/hls/AbstrSemIdent.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/hls/AbstrSemIdent.v b/src/hls/AbstrSemIdent.v index 0cc8e9d..36c3ffc 100644 --- a/src/hls/AbstrSemIdent.v +++ b/src/hls/AbstrSemIdent.v @@ -96,10 +96,10 @@ Proof. Lemma sem_pred_expr_app_predicated_false2 : forall f_p y x v p ps, - sem_pred_expr f_p sem ctx (app_predicated p y x) v -> + sem_pred_expr f_p a_sem ctx (app_predicated p y x) v -> (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> eval_predf ps p = false -> - sem_pred_expr f_p sem ctx y v. + sem_pred_expr f_p a_sem ctx y v. Admitted. Lemma sem_pred_expr_pred_ret : @@ -601,7 +601,8 @@ Proof. rewrite Eapp_right_nil. auto. Qed. -Lemma sem_merge_list : (* [[id:f307d227-d0e9-49a0-823f-2d7e0db76972]] *) +(* [[id:f307d227-d0e9-49a0-823f-2d7e0db76972]] *) +Lemma sem_merge_list : forall f rs ps m args, sem ctx f ((mk_instr_state rs ps m), None) -> sem_pred_expr (forest_preds f) sem_val_list ctx |