diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-30 18:47:47 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-30 18:47:47 +0100 |
| commit | 747cb7c6fa026a0bfa2338fc8ca6edcd8be4a95d (patch) | |
| tree | f4205c7953d134f2e5d83ef76498087ac635654d | |
| parent | 6e50ba5cfb17d173aaced6b960cedd3fcb0073c4 (diff) | |
| download | vericert-747cb7c6fa026a0bfa2338fc8ca6edcd8be4a95d.tar.gz vericert-747cb7c6fa026a0bfa2338fc8ca6edcd8be4a95d.zip | |
Remove unnecessary assumption from sem_merge_list
| -rw-r--r-- | src/hls/AbstrSemIdent.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/hls/AbstrSemIdent.v b/src/hls/AbstrSemIdent.v index a0a4b8b..adb2388 100644 --- a/src/hls/AbstrSemIdent.v +++ b/src/hls/AbstrSemIdent.v @@ -945,14 +945,13 @@ Qed. (* [[id:f307d227-d0e9-49a0-823f-2d7e0db76972]] *) Lemma sem_merge_list : - forall f rs pr ps m args, - (forall x, sem_pexpr ctx (get_forest_p' x pr) (ps !! x)) -> + 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 (merge (list_translation args f)) (rs ## args). Proof. - induction args; intros * HPRED **; crush. cbn. constructor; constructor. - unfold merge. specialize (IHargs HPRED H). + induction args; intros * **; crush. cbn. constructor; constructor. + unfold merge. specialize (IHargs H). eapply sem_pred_expr_ident2 in IHargs. inversion_clear IHargs as [l_ [HSEM HVAL]]. destruct_match; [|exfalso; eapply NE.of_list_contra; eauto]. |