diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-21 14:42:03 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-21 14:42:03 +0100 |
| commit | fc4bc25ca5d986831a02cddd87264b7b51943fc4 (patch) | |
| tree | 075f6cf97f3a35a0c6d34650806b295573288c5f /src/hls/AbstrSemIdent.v | |
| parent | 28352e0b7c53f7b0d3e610bf8507ee4b0901171d (diff) | |
| download | vericert-fc4bc25ca5d986831a02cddd87264b7b51943fc4.tar.gz vericert-fc4bc25ca5d986831a02cddd87264b7b51943fc4.zip | |
Prove evaluable_pred_expr_exists_RBsetpred
Diffstat (limited to 'src/hls/AbstrSemIdent.v')
| -rw-r--r-- | src/hls/AbstrSemIdent.v | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/src/hls/AbstrSemIdent.v b/src/hls/AbstrSemIdent.v index 36c3ffc..5c6b3eb 100644 --- a/src/hls/AbstrSemIdent.v +++ b/src/hls/AbstrSemIdent.v @@ -482,7 +482,7 @@ Lemma sem_pred_expr_flap : sem_pred_expr ps sem_ident ctx f f_ -> sem_pred_expr ps sem_ident ctx (flap f l) (f_ l). Proof. - induction f. unfold flap2; intros. inv H. inv H3. + induction f. unfold flap; intros. inv H. inv H3. constructor; eauto. constructor. intros. inv H. cbn. constructor; eauto. inv H5. constructor. @@ -501,6 +501,12 @@ Proof. eapply sem_pred_expr_cons_false; eauto. Qed. +Lemma sem_pred_expr_flap2_2 : + forall A B C (f: predicated (A -> B -> C)) ps l1 l2 x, + sem_pred_expr ps sem_ident ctx (flap2 f l1 l2) x -> + exists f_, sem_pred_expr ps sem_ident ctx f f_ /\ f_ l1 l2 = x. +Proof. Admitted. + Lemma sem_pred_expr_seq_app_val : forall A B V (s: @Abstr.ctx G -> B -> V -> Prop) (f: predicated (A -> B)) @@ -663,4 +669,16 @@ Proof. cbn; constructor; auto. Qed. +Lemma from_predicated_sem_pred_expr : + forall preds pe b, + sem_pred_expr preds sem_pred ctx pe b -> + sem_pexpr ctx (from_predicated true preds pe) b. +Proof. Admitted. + +Lemma from_predicated_sem_pred_expr2 : + forall preds pe b, + sem_pexpr ctx (from_predicated true preds pe) b -> + sem_pred_expr preds sem_pred ctx pe b. +Proof. Admitted. + End PROOF. |