Prove more admitted theorems

6 files changed, 190 insertions, 47 deletions

diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v
index 2c3ae94..7b10ee0 100644
--- a/src/common/NonEmpty.v
+++ b/src/common/NonEmpty.v
@@ -305,3 +305,24 @@ Proof.
     + constructor. eapply H. constructor; tauto. eapply IHl.
       intros. eapply H. constructor; tauto.
 Qed.
+
+Lemma filter_None :
+  forall A f (x: non_empty A),
+    filter f x = None ->
+    Forall (fun x => f x = false) x.
+Proof.
+  induction x; cbn; intros.
+  - constructor. destruct_match; now auto.
+  - constructor. destruct_match; auto. destruct_match; try discriminate.
+    destruct_match; eauto. now destruct_match.
+Qed.
+
+Lemma In_map :
+  forall A B (f: A -> B) n (x: A),
+    In x n ->
+    In (f x) (map f n).
+Proof.
+  induction n; inversion 1; subst; cbn in *.
+  - constructor.
+  - clear H. inv H1; intuition (constructor; auto).
+Qed.
diff --git a/src/hls/AbstrSemIdent.v b/src/hls/AbstrSemIdent.v
index 1499ea9..909a1a1 100644
--- a/src/hls/AbstrSemIdent.v
+++ b/src/hls/AbstrSemIdent.v
@@ -125,21 +125,74 @@ Proof.
 Qed.
 
 Lemma sem_pred_expr_prune_predicated :
-  forall f_p y x v,
+  forall f_p ps x y v,
+    (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) ->
     sem_pred_expr f_p a_sem ctx x v ->
     prune_predicated x = Some y ->
     sem_pred_expr f_p a_sem ctx y v.
 Proof.
-  intros * SEM PRUNE. unfold prune_predicated in *. Admitted.
+  induction x.
+  - cbn in *; intros * HPREDSEM **. repeat destr.
+    inv H0. inv H. constructor; auto; cbn in *.
+    eapply sem_pexpr_eval; [eassumption|].
+    eapply sem_pexpr_eval_inv in H1; [|eassumption].
+    now rewrite eval_predf_deep_simplify.
+  - cbn in *; intros * HPREDSEM **. destruct_match; repeat destr.
+    2: { clear Heqb. inv H; cbn in *.
+         eapply sem_pexpr_eval_inv in H4; [|eassumption].
+         rewrite <- 2 eval_predf_deep_simplify with (peq:=peq) in H4.
+         setoid_rewrite Heqp in H4. now cbn in H4.
+         eauto. }
+    destruct_match.
+    + inv H0. inv H.
+      * constructor; auto. eapply sem_pexpr_eval; [eassumption|].
+        eapply sem_pexpr_eval_inv in H3; [|eassumption].
+        now rewrite eval_predf_deep_simplify.
+      * eapply sem_pred_expr_cons_false; eauto.
+        eapply sem_pexpr_eval; [eassumption|].
+        eapply sem_pexpr_eval_inv in H3; [|eassumption].
+        now rewrite eval_predf_deep_simplify.
+    + inv H0. inv H.
+      * constructor; auto.
+        eapply sem_pexpr_eval; [eassumption|].
+        eapply sem_pexpr_eval_inv in H3; [|eassumption].
+        now rewrite eval_predf_deep_simplify.
+      * cbn in *. exploit NE.filter_None. eapply Heqo. cbn. intros.
+        exploit sem_pred_expr_in_true. eapply H5. intros [p_true [e_true [HIN [HSEMP HASEM]]]].
+        pose proof (NE.In_map _ _ (fun x : Predicate.pred_op * A => (deep_simplify peq (fst x), snd x)) _ _ HIN).
+        cbn in *. eapply NE.Forall_forall in H; [|eassumption].
+        destr. clear H. cbn in *.
+        eapply sem_pexpr_eval_inv in HSEMP; [|eassumption].
+        rewrite <- 2 eval_predf_deep_simplify with (peq:=peq) in HSEMP.
+        setoid_rewrite Heqp in HSEMP. now cbn in HSEMP.
+Qed.
 
 Lemma sem_pred_expr_prune_predicated2 :
-  forall f_p y x v,
+  forall f_p ps x y v,
+    (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) ->
     sem_pred_expr f_p a_sem ctx y v ->
     prune_predicated x = Some y ->
     sem_pred_expr f_p a_sem ctx x v.
 Proof.
-  intros * SEM PRUNE. unfold prune_predicated in *.
-  Admitted.
+  induction x; intros * SEMPRED SEM PRUNE. unfold prune_predicated in *.
+  - cbn in *. destr. inv PRUNE. inv SEM.
+    destruct a; constructor; auto.
+    eapply sem_pexpr_eval_inv in H2; eauto.
+    eapply sem_pexpr_eval; eauto.
+    rewrite eval_predf_deep_simplify in H2; auto.
+  - cbn in *. destruct_match.
+    2: { destr. destruct a. eapply sem_pred_expr_cons_false; eauto.
+         eapply sem_pexpr_eval; eauto.
+         rewrite <- 2 eval_predf_deep_simplify with (peq:=peq). now setoid_rewrite Heqp.
+    }
+    destruct_match.
+    + inv PRUNE. destruct a; inv SEM; [constructor|eapply sem_pred_expr_cons_false]; eauto;
+      eapply sem_pexpr_eval; eauto; rewrite <- eval_predf_deep_simplify with (peq:=peq);
+      eapply sem_pexpr_eval_inv in H4; eauto.
+    + inv PRUNE. inv SEM. destruct a. constructor; auto.
+      eapply sem_pexpr_eval; eauto. eapply sem_pexpr_eval_inv in H2; eauto.
+      now rewrite <- eval_predf_deep_simplify with (peq:=peq).
+Qed.
 
 Lemma sem_pred_expr_pred_ret :
   forall (i: A) ps,
@@ -181,6 +234,23 @@ Proof.
     intros. eapply H0. constructor; tauto.
 Qed.
 
+Lemma sem_pred_expr_NEapp6 :
+  forall f_p a b v ps,
+    (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) ->
+    (forall x, NE.In x a -> eval_predf ps (fst x) = false) ->
+    sem_pred_expr f_p a_sem ctx (NE.app a b) v ->
+    sem_pred_expr f_p a_sem ctx b v.
+Proof.
+  induction a; crush.
+  - assert (IN: NE.In a (NE.singleton a)) by constructor.
+    inv H1; auto. eapply H0 in IN. eapply sem_pexpr_eval_inv in H5; eauto.
+    now setoid_rewrite H5 in IN.
+  - assert (NE.In a (NE.cons a a0)) by (constructor; tauto).
+    eapply H0 in H2. destruct a. inv H1.
+    + eapply sem_pexpr_eval_inv in H8; eauto. now setoid_rewrite H8 in H2.
+    + eapply IHa; eauto. intros. eapply H0. constructor; tauto.
+Qed.
+
 Lemma sem_pred_expr_NEapp3 :
   forall f_p ctx a b v,
     (forall x, NE.In x a -> sem_pexpr ctx (from_pred_op f_p (fst x)) false) ->
@@ -283,6 +353,29 @@ Proof.
   eapply sem_pexpr_eval; eauto. eauto.
 Qed.
 
+Lemma sem_pred_expr_map_Pand2 :
+  forall f_p ps x v p,
+    (forall x : positive, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) ->
+    eval_predf ps p = true ->
+    sem_pred_expr f_p a_sem ctx
+      (NE.map (fun x0 => (p ∧ fst x0, snd x0)) x) v ->
+    sem_pred_expr f_p a_sem ctx x v.
+Proof.
+  induction x; crush.
+  - inv H1. destruct a; constructor; auto. eapply sem_pexpr_eval; eauto.
+    eapply sem_pexpr_eval_inv in H5; eauto. rewrite eval_predf_Pand in H5.
+    now rewrite H0 in H5.
+  - inv H1.
+    + destruct a; constructor; auto. eapply sem_pexpr_eval; eauto.
+      eapply sem_pexpr_eval_inv in H7; eauto. rewrite eval_predf_Pand in H7.
+      now rewrite H0 in H7.
+    + destruct a; eapply sem_pred_expr_cons_false; eauto.
+      eapply sem_pexpr_eval; eauto.
+      eapply sem_pexpr_eval_inv in H7; eauto.
+      rewrite eval_predf_Pand in H7.
+      now rewrite H0 in H7.
+Qed.
+
 Lemma sem_pred_expr_app_predicated :
   forall f_p y x v p ps,
     sem_pred_expr f_p a_sem ctx x v ->
@@ -303,7 +396,13 @@ Lemma sem_pred_expr_app_predicated2 :
     (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) ->
     eval_predf ps p = true ->
     sem_pred_expr f_p a_sem ctx x v.
-Proof. Admitted.
+Proof.
+  intros * SEM PS EVAL. unfold app_predicated in *.
+  eapply sem_pred_expr_NEapp6 in SEM; eauto.
+  - eapply sem_pred_expr_map_Pand2; eauto.
+  - intros. eapply sem_pred_expr_map_not; [|eassumption].
+    rewrite eval_predf_negate. now rewrite EVAL.
+Qed.
 
 Lemma sem_pred_expr_ident :
   forall ps l l_,
@@ -465,18 +564,9 @@ Proof.
         inv H3. inv H1. eapply sem_pexpr_det in H0; try eassumption. discriminate.
         apply similar_refl. split; auto.
         apply sem_pred_expr_cons_false; auto.
-  - destruct x in *; cbn in *.
-    rewrite NE.app_NEmap in H0.
-    generalize dependent b; induction b; intros.
-    + cbn in *; repeat destr. inv Heqp0. inv H0.
-      * inv H6. inv H7. solve [repeat constructor; auto].
-      * inv H6. inv H1.
-        -- exploit IHa; eauto; intros. inv H1. split; auto.
-           apply sem_pred_expr_cons_false; eauto.
-        -- exploit IHa; eauto; intros. inv H1. inv H3.
-           eapply sem_pexpr_det in H0; try eassumption. discriminate.
-           apply similar_refl.
-    + Admitted.
+  - destruct x; cbn [fst snd] in *.
+    unfold predicated_prod in H0. cbn in H0.
+    rewrite NE.app_NEmap in H0. 
 
 Lemma sem_pred_expr_seq_app :
   forall A B (f: predicated (A -> B)) ps l f_ l_,
diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index d7b0e66..cb080c5 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -192,6 +192,16 @@ Lemma eval_predf_Por :
     eval_predf ps (p ∨ p') = eval_predf ps p || eval_predf ps p'.
 Proof. unfold eval_predf; split; simplify; auto with bool. Qed.
 
+Lemma eval_predf_simplify :
+  forall ps p,
+    eval_predf ps (simplify p) = eval_predf ps p.
+Proof. unfold eval_predf; intros. now rewrite simplify_correct. Qed.
+
+Lemma eval_predf_deep_simplify :
+  forall peq ps p,
+    eval_predf ps (deep_simplify peq p) = eval_predf ps p.
+Proof. unfold eval_predf; intros. now rewrite deep_simplify_correct. Qed.
+
 Lemma eval_predf_pr_equiv :
   forall p ps ps',
     (forall x, ps !! x = ps' !! x) ->
diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v
index c2cebdc..d3cc280 100644
--- a/src/hls/GiblePargenproofEquiv.v
+++ b/src/hls/GiblePargenproofEquiv.v
@@ -1023,6 +1023,21 @@ Section SEM_PRED_EXEC.
     eapply sem_pexpr_eval; eauto.
   Qed.
 
+  Lemma sem_pred_expr_in_true :
+    forall pe v,
+      sem_pred_expr f a_sem ctx pe v ->
+      exists p e, NE.In (p, e) pe
+                  /\ sem_pexpr ctx (from_pred_op f p) true
+                  /\ a_sem ctx e v.
+  Proof.
+    induction pe; crush.
+    - inv H. do 2 eexists; split; try split; eauto. constructor.
+    - inv H.
+      + do 2 eexists; split; try split; eauto. constructor; tauto.
+      + exploit IHpe; eauto. simplify.
+        do 2 eexists; split; try split; eauto. constructor; tauto.
+  Qed.
+
 End SEM_PRED_EXEC.
 
 Module HashExprNorm(HS: Hashable).
@@ -1221,21 +1236,6 @@ Module HashExprNorm(HS: Hashable).
         eapply H.wf_hash_table_distr; eauto. eauto.
   Qed.
 
-  Lemma sem_pred_expr_in_true :
-    forall pe v,
-      sem_pred_expr f a_sem ctx pe v ->
-      exists p e, NE.In (p, e) pe
-                  /\ sem_pexpr ctx (from_pred_op f p) true
-                  /\ a_sem ctx e v.
-  Proof.
-    induction pe; crush.
-    - inv H. do 2 eexists; split; try split; eauto. constructor.
-    - inv H.
-      + do 2 eexists; split; try split; eauto. constructor; tauto.
-      + exploit IHpe; eauto. simplify.
-        do 2 eexists; split; try split; eauto. constructor; tauto.
-  Qed.
-
   Definition pred_Ht_dec :
     forall x y: pred_op * HS.t, {x = y} + {x <> y}.
   Proof.
diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v
index 1051fe5..d340477 100644
--- a/src/hls/GiblePargenproofForward.v
+++ b/src/hls/GiblePargenproofForward.v
@@ -177,7 +177,7 @@ all be evaluable.
         destruct f as [fr fp fe]. cbn [forest_preds set_forest] in *.
         destruct (peq x res); subst.
         * rewrite forest_reg_gss in *. rewrite Regmap.gss in *.
-          eapply sem_pred_expr_prune_predicated; eauto.
+          eapply sem_pred_expr_prune_predicated; eauto. inv PRED; eassumption.
           eapply sem_pred_expr_app_predicated; [| |eauto].
           replace fp with (forest_preds {| forest_regs := fr; forest_preds := fp; forest_exit := fe |}) by auto.
           eapply sem_update_Iop; eauto. cbn in *.
@@ -215,7 +215,7 @@ all be evaluable.
         destruct f as [fr fp fe]. cbn [forest_preds set_forest] in *.
         destruct (peq x res); subst.
         * rewrite forest_reg_gss in *. rewrite Regmap.gss in *.
-          eapply sem_pred_expr_prune_predicated; eauto.
+          eapply sem_pred_expr_prune_predicated; eauto. inv PRED; eassumption.
           eapply sem_pred_expr_app_predicated; [| |eauto].
           replace fp with (forest_preds {| forest_regs := fr; forest_preds := fp; forest_exit := fe |}) by auto.
           eapply sem_update_Iload; eauto.
@@ -260,7 +260,7 @@ all be evaluable.
       apply exists_sem_pred in H. inversion_clear H as [r' [HNE HVAL]].
       exploit sem_merge_list. eapply SEM2. instantiate (2 := args). intro HSPE. eapply sem_pred_expr_ident2 in HSPE.
       inversion_clear HSPE as [l_ [HSPE1 HSPE2]].
-      eapply sem_pred_expr_prune_predicated; eauto.
+      eapply sem_pred_expr_prune_predicated; eauto. inv PRED; eassumption.
       eapply sem_pred_expr_app_predicated.
       eapply sem_pred_expr_seq_app_val; [solve [eauto]| |].
       eapply sem_pred_expr_seq_app; [solve [eauto]|].
@@ -473,7 +473,7 @@ all be evaluable.
       constructor.
       * constructor. intros. destruct (peq x res); subst.
         rewrite forest_reg_gss. cbn.
-        eapply sem_pred_expr_prune_predicated; eauto.
+        eapply sem_pred_expr_prune_predicated; eauto. inv H3; inv H9; eassumption.
         eapply sem_pred_expr_app_predicated_false. inv H3. inv H8. auto.
         inv H3. inv H9. eauto. rewrite eval_predf_Pand. cbn -[eval_predf].
         rewrite H0. auto. 
@@ -486,7 +486,7 @@ all be evaluable.
       constructor.
       * constructor. intros. destruct (peq x dst); subst.
         rewrite forest_reg_gss. cbn.
-        eapply sem_pred_expr_prune_predicated; eauto.
+        eapply sem_pred_expr_prune_predicated; eauto. inv H3; inv H9; eassumption.
         eapply sem_pred_expr_app_predicated_false. inv H3. inv H8. auto.
         inv H3. inv H9. eauto. rewrite eval_predf_Pand. cbn -[eval_predf].
         rewrite H0. auto. 
@@ -499,7 +499,7 @@ all be evaluable.
       constructor.
       * constructor. intros. rewrite forest_reg_gso by discriminate. inv H3. inv H8. auto.
       * constructor; intros. rewrite forest_reg_pred. inv H3. inv H9. auto.
-      * rewrite forest_reg_gss. cbn. eapply sem_pred_expr_prune_predicated; eauto.
+      * rewrite forest_reg_gss. cbn. eapply sem_pred_expr_prune_predicated; eauto. inv H3; inv H9; eassumption.
         eapply sem_pred_expr_app_predicated_false. inv H3. auto. inv H3. inv H9. eauto.
         rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H0. auto.
       * inv H3. auto.
@@ -528,7 +528,7 @@ all be evaluable.
       * constructor. inv H8. auto.
       * constructor. intros. inv H9. eauto.
       * auto.
-      * cbn. eapply sem_pred_expr_prune_predicated; [|eauto].
+      * cbn. eapply sem_pred_expr_prune_predicated; [| |eauto]. inv H9; eassumption.
         eapply sem_pred_expr_app_predicated_false; auto.
         inv H9. eauto.
         rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H0. auto.
@@ -548,7 +548,7 @@ all be evaluable.
       constructor.
       * constructor. intros. destruct (peq x r); subst.
         rewrite forest_reg_gss. cbn.
-        eapply sem_pred_expr_prune_predicated; eauto.
+        eapply sem_pred_expr_prune_predicated; eauto. inv H1; inv H8; eassumption.
         eapply sem_pred_expr_app_predicated_false. inv H1. inv H7. auto.
         inv H1. inv H8. eauto. rewrite eval_predf_Pand.
         rewrite H. eauto with bool.
@@ -561,7 +561,7 @@ all be evaluable.
       constructor.
       * constructor. intros. destruct (peq x r); subst.
         rewrite forest_reg_gss. cbn.
-        eapply sem_pred_expr_prune_predicated; eauto.
+        eapply sem_pred_expr_prune_predicated; eauto. inv H1; inv H8; eassumption.
         eapply sem_pred_expr_app_predicated_false. inv H1. inv H7. auto.
         inv H1. inv H8. eauto. rewrite eval_predf_Pand. cbn -[eval_predf].
         rewrite H. eauto with bool.
@@ -574,7 +574,7 @@ all be evaluable.
       constructor.
       * constructor. intros. rewrite forest_reg_gso by discriminate. inv H1. inv H7. auto.
       * constructor; intros. rewrite forest_reg_pred. inv H1. inv H8. auto.
-      * rewrite forest_reg_gss. cbn. eapply sem_pred_expr_prune_predicated; eauto.
+      * rewrite forest_reg_gss. cbn. eapply sem_pred_expr_prune_predicated; eauto. inv H1; inv H8; eassumption.
         eapply sem_pred_expr_app_predicated_false. inv H1. auto. inv H1. inv H8. eauto.
         rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H. eauto with bool.
       * inv H1. auto.
@@ -604,7 +604,7 @@ all be evaluable.
          * constructor. inv H7. auto.
          * constructor. intros. inv H8. eauto.
          * auto.
-         * cbn. eapply sem_pred_expr_prune_predicated; [|eauto].
+         * cbn. eapply sem_pred_expr_prune_predicated; [| |eauto]. inv H8; eassumption.
            eapply sem_pred_expr_app_predicated_false; auto.
            inv H8. eauto.
            rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H. eauto with bool.
@@ -675,7 +675,7 @@ all be evaluable.
     constructor. inv H9. intros. cbn. eauto.
     inv H10. constructor; intros. eauto.
     cbn.
-    eapply sem_pred_expr_prune_predicated; eauto.
+    eapply sem_pred_expr_prune_predicated; eauto. inv H10; eassumption.
     eapply sem_pred_expr_app_predicated.
     constructor. constructor. constructor.
     inv H10. eauto. cbn -[eval_predf] in *.
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v
index 92ad03f..99dfd77 100644
--- a/src/hls/Predicate.v
+++ b/src/hls/Predicate.v
@@ -386,11 +386,11 @@ Proof.
   solve [rewrite andb_true_r; auto | rewrite orb_false_r; auto].
 Qed.
 
+Local Opaque simplify'.
 Lemma simplify_correct :
   forall h a,
     sat_predicate (simplify h) a = sat_predicate h a.
 Proof.
-  Local Opaque simplify'.
   induction h; crush.
   - replace (sat_predicate h1 a && sat_predicate h2 a)
       with (sat_predicate (simplify h1) a && sat_predicate (simplify h2) a)
@@ -400,7 +400,29 @@ Proof.
       with (sat_predicate (simplify h1) a || sat_predicate (simplify h2) a)
       by crush.
     rewrite simplify'_correct. crush.
-    Local Transparent simplify'.
+Qed.
+Local Transparent simplify'.
+
+Lemma Plit_inj :
+  forall A (a b: bool * A), Plit a = Plit b -> a = b.
+Proof. now inversion 1. Qed.
+
+Lemma deep_simplify'_correct :
+  forall peq h a,
+    sat_predicate (deep_simplify' peq h) a = sat_predicate h a.
+Proof.
+  destruct h; auto; cbn in *;
+    destruct h1; destruct h2; intuition auto with *; destruct_match; auto;
+    clear Heqs; inv e; solve [now rewrite andb_diag | now rewrite orb_diag].
+Qed.
+
+Lemma deep_simplify_correct :
+  forall peq h a,
+    sat_predicate (deep_simplify peq h) a = sat_predicate h a.
+Proof.
+  induction h; auto;
+    intros; cbn -[deep_simplify']; rewrite deep_simplify'_correct;
+    cbn; rewrite IHh1; now rewrite IHh2.
 Qed.
 
 Fixpoint mult {A: Type} (a b: list (list A)) : list (list A) :=