Finish forward and backward proofs for predicated proof

1 files changed, 0 insertions, 90 deletions

diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index 6bfc654..caad4b5 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -552,96 +552,6 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       rewrite eval_predf_negate. rewrite H0. auto.
   Qed.
 
-  Lemma sem_pexpr_evaluable :
-    forall A ctx f_p ps,
-      (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) ->
-      forall p, exists b, @sem_pexpr A ctx (from_pred_op f_p p) b.
-  Proof.
-    induction p; crush.
-    - destruct_match. inv Heqp0. destruct b. econstructor. eauto.
-      econstructor. eapply sem_pexpr_negate. eauto.
-    - econstructor. constructor.
-    - econstructor. constructor.
-    - destruct x0, x; solve [eexists; constructor; auto].
-    - destruct x0, x; solve [eexists; constructor; auto].
-  Qed.
-
-  Lemma sem_pexpr_eval1 :
-    forall A ctx f_p ps,
-      (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) ->
-      forall p,
-        eval_predf ps p = false ->
-        @sem_pexpr A ctx (from_pred_op f_p p) false.
-  Proof.
-    induction p; crush.
-    - destruct_match. inv Heqp0.
-      destruct b.
-      + cbn in H0. rewrite <- H0. eauto.
-      + replace false with (negb true) by auto.
-        apply sem_pexpr_negate. cbn in H0.
-        apply negb_true_iff in H0. rewrite negb_involutive in H0.
-        rewrite <- H0. eauto.
-     - constructor.
-     - rewrite eval_predf_Pand in H0.
-       apply andb_false_iff in H0. inv H0. eapply IHp1 in H1.
-       pose proof (sem_pexpr_evaluable _ _ _ _ H p2) as EVAL.
-       inversion_clear EVAL as [x EVAL2].
-       replace false with (false && x) by auto.
-       constructor; auto.
-       eapply IHp2 in H1.
-       pose proof (sem_pexpr_evaluable _ _ _ _ H p1) as EVAL.
-       inversion_clear EVAL as [x EVAL2].
-       replace false with (x && false) by eauto with bool.
-       apply sem_pexpr_Pand; auto.
-     - rewrite eval_predf_Por in H0.
-       apply orb_false_iff in H0. inv H0.
-       replace false with (false || false) by auto.
-       apply sem_pexpr_Por; auto.
-  Qed.
-
-  Lemma sem_pexpr_eval2 :
-    forall A ctx f_p ps,
-      (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) ->
-      forall p,
-        eval_predf ps p = true ->
-        @sem_pexpr A ctx (from_pred_op f_p p) true.
-  Proof.
-    induction p; crush.
-    - destruct_match. inv Heqp0.
-      destruct b.
-      + cbn in H0. rewrite <- H0. eauto.
-      + replace true with (negb false) by auto.
-        apply sem_pexpr_negate. cbn in H0.
-        apply negb_true_iff in H0.
-        rewrite <- H0. eauto.
-     - constructor.
-     - rewrite eval_predf_Pand in H0.
-       apply andb_true_iff in H0. inv H0.
-       replace true with (true && true) by auto.
-       constructor; auto.
-     - rewrite eval_predf_Por in H0.
-       apply orb_true_iff in H0. inv H0. eapply IHp1 in H1.
-       pose proof (sem_pexpr_evaluable _ _ _ _ H p2) as EVAL.
-       inversion_clear EVAL as [x EVAL2].
-       replace true with (true || x) by auto.
-       apply sem_pexpr_Por; auto.
-       eapply IHp2 in H1.
-       pose proof (sem_pexpr_evaluable _ _ _ _ H p1) as EVAL.
-       inversion_clear EVAL as [x EVAL2].
-       replace true with (x || true) by eauto with bool.
-       apply sem_pexpr_Por; auto.
-  Qed.
-
-  Lemma sem_pexpr_eval :
-    forall A ctx f_p ps b,
-      (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) ->
-      forall p,
-        eval_predf ps p = b ->
-        @sem_pexpr A ctx (from_pred_op f_p p) b.
-  Proof.
-    intros; destruct b; eauto using sem_pexpr_eval1, sem_pexpr_eval2.
-  Qed.
-
   Lemma sem_pred_expr_NEapp :
     forall A B C sem f_p ctx a b v,
       sem_pred_expr f_p sem ctx a v ->