From fc4bc25ca5d986831a02cddd87264b7b51943fc4 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 21 May 2023 14:42:03 +0100
Subject: Prove evaluable_pred_expr_exists_RBsetpred

---
 src/hls/AbstrSemIdent.v | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

(limited to 'src/hls/AbstrSemIdent.v')

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.
-- 
cgit