diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-30 17:42:10 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-30 17:42:10 +0100 |
| commit | 0b1c04f301402802d0ecdc3aff1b8b56ab905176 (patch) | |
| tree | 290cab55f78f9733e5740b09ac7098d42ea89910 | |
| parent | ebac331582b9f7826732b33be9419ee154c7b525 (diff) | |
| download | vericert-0b1c04f301402802d0ecdc3aff1b8b56ab905176.tar.gz vericert-0b1c04f301402802d0ecdc3aff1b8b56ab905176.zip | |
Prove merge list_translation
| -rw-r--r-- | src/hls/AbstrSemIdent.v | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/src/hls/AbstrSemIdent.v b/src/hls/AbstrSemIdent.v index 1c0e345..4818c53 100644 --- a/src/hls/AbstrSemIdent.v +++ b/src/hls/AbstrSemIdent.v @@ -898,15 +898,29 @@ Proof. simplify. eapply Eapp_Econs_eq in H2; subst; auto. Qed. +Lemma of_to_list : + forall x, of_elist (to_elist x) = x. +Proof. + induction x; auto. + cbn. rewrite IHx; auto. +Qed. + Lemma sem_pred_expr_merge : - forall G (ctx: @Abstr.ctx G) ps l args, + forall ps l args, Forall2 (sem_pred_expr ps sem_ident ctx) args l -> sem_pred_expr ps sem_ident ctx (merge args) (to_elist l). Proof. induction l; intros. - inv H. cbn; repeat constructor. - inv H. cbn. unfold merge. - Admitted. + exploit NE.of_list_exists. intros [x0 HOFLIST]. rewrite HOFLIST. + replace (Econs a (to_elist l)) with (Eapp (Econs a (to_elist l)) Enil) + by apply Eapp_right_nil. + eapply sem_pred_expr_fold_right. constructor; auto. constructor. constructor. + cbn. apply NE.of_list_to_list in HOFLIST. + setoid_rewrite HOFLIST. constructor; eauto. + rewrite of_to_list. auto. +Qed. Lemma sem_pred_expr_merge2 : forall pr l l', |