Prove fold_right over Elist

1 files changed, 74 insertions, 4 deletions

diff --git a/src/hls/AbstrSemIdent.v b/src/hls/AbstrSemIdent.v
index 30b287d..1c0e345 100644
--- a/src/hls/AbstrSemIdent.v
+++ b/src/hls/AbstrSemIdent.v
@@ -809,6 +809,21 @@ Proof.
   eapply sem_pred_expr_predicated_prod; eauto.
 Qed.
 
+Lemma sem_pred_expr_cons_pred_expr2 :
+  forall ps pr s a x,
+    (forall x, sem_pexpr ctx (get_forest_p' x pr) (ps !! x)) ->
+    sem_pred_expr pr sem_ident ctx (cons_pred_expr a s) x ->
+    exists s' e, sem_pred_expr pr sem_ident ctx s s'
+      /\ sem_pred_expr pr sem_ident ctx a e
+      /\ x = Econs e s'.
+Proof.
+  intros * HPRED **. unfold cons_pred_expr in *.
+  exploit sem_pred_expr_predicated_map2; eauto; simplify.
+  exploit sem_pred_expr_predicated_prod2; eauto; simplify.
+  destruct x0; cbn in *.
+  eexists; simplify; eauto.
+Qed.
+
 Lemma sem_pred_expr_fold_right :
   forall pr s a a' s',
     sem_pred_expr pr sem_ident ctx s s' ->
@@ -821,13 +836,67 @@ Proof.
   eapply sem_pred_expr_cons_pred_expr; eauto.
 Qed.
 
+Lemma Eapp_Econs :
+  forall x y z,
+    Eapp x (Econs y z) = Eapp (Eapp x (Econs y Enil)) z.
+Proof.
+  induction x; cbn; intros.
+  - auto.
+  - f_equal. auto.
+Qed.
+
+Lemma Eapp_Econs_eq' :
+  forall b' a' x,
+    Eapp b' (Econs x Enil) = Eapp a' (Econs x Enil) -> b' = a'.
+Proof.
+  induction b'; cbn; intros.
+  - destruct a'; auto. cbn in *.
+    inv H. destruct a'; eauto. cbn in *. discriminate.
+  - cbn in *. destruct a'. cbn in *. inv H.
+    { exfalso. destruct b'; cbn in *; discriminate. }
+    cbn in *. inv H. eauto. eapply IHb' in H2. subst. auto.
+Qed.
+
+Lemma Eapp_Econs_eq :
+  forall s' a' b',
+    Eapp a' s' = Eapp b' s' ->
+    a' = b'.
+Proof.
+  induction s'; cbn; intros.
+  - rewrite ! Eapp_right_nil in H; auto.
+  - rewrite Eapp_Econs in H. symmetry in H.
+    rewrite Eapp_Econs in H. eapply IHs' in H.
+    eapply Eapp_Econs_eq'; eauto.
+Qed.
+
+Lemma sem_pred_expr_fold_right2' :
+  forall ps pr s a x s',
+    (forall x, sem_pexpr ctx (get_forest_p' x pr) (ps !! x)) ->
+    sem_pred_expr pr sem_ident ctx s s' ->
+    sem_pred_expr pr sem_ident ctx (NE.fold_right cons_pred_expr s a) x ->
+    exists a', x = (Eapp a' s') /\ Forall2 (sem_pred_expr pr sem_ident ctx) (NE.to_list a) (of_elist a').
+Proof.
+  induction a; cbn; intros.
+  - exploit sem_pred_expr_cons_pred_expr2; eauto; simplify.
+    eapply sem_pred_expr_ident_det in H0; eauto; subst.
+    exists (Econs x1 Enil); split; auto.
+    constructor; [auto|constructor].
+  - exploit sem_pred_expr_cons_pred_expr2; eauto; simplify.
+    exploit IHa; eauto; simplify.
+    exists (Econs x1 x); split; auto.
+    constructor; auto.
+Qed.
+
 Lemma sem_pred_expr_fold_right2 :
-  forall A pr ctx s a a' s',
+  forall ps pr s a a' s',
+    (forall x, sem_pexpr ctx (get_forest_p' x pr) (ps !! x)) ->
     sem_pred_expr pr sem_ident ctx s s' ->
-    @sem_pred_expr A _ _ pr sem_ident ctx (NE.fold_right cons_pred_expr s a) (Eapp a' s') ->
+    sem_pred_expr pr sem_ident ctx (NE.fold_right cons_pred_expr s a) (Eapp a' s') ->
     Forall2 (sem_pred_expr pr sem_ident ctx) (NE.to_list a) (of_elist a').
 Proof.
-  induction a. Admitted.
+  intros. exploit sem_pred_expr_fold_right2'. eauto. eapply H0. eauto.
+  simplify. eapply Eapp_Econs_eq in H2; subst; auto.
+Qed.
 
 Lemma sem_pred_expr_merge :
   forall G (ctx: @Abstr.ctx G) ps l args,
@@ -836,7 +905,8 @@ Lemma sem_pred_expr_merge :
 Proof.
   induction l; intros.
   - inv H. cbn; repeat constructor.
-  - inv H. cbn. unfold merge. Admitted.
+  - inv H. cbn. unfold merge.
+  Admitted.
 
 Lemma sem_pred_expr_merge2 :
   forall pr l l',