Add equivalence classes

1 files changed, 0 insertions, 99 deletions

diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v
index 946a243..48fe922 100644
--- a/src/hls/GiblePargenproofForward.v
+++ b/src/hls/GiblePargenproofForward.v
@@ -273,105 +273,6 @@ all be evaluable.
     + auto.
   Qed.
 
-  Lemma sem_pexpr_not_in :
-    forall G (ctx: @ctx G) p0 ps p e b,
-      ~ PredIn p p0 ->
-      sem_pexpr ctx (from_pred_op ps p0) b ->
-      sem_pexpr ctx (from_pred_op (PTree.set p e ps) p0) b.
-  Proof.
-    induction p0; auto; intros.
-    - cbn. destruct p. unfold get_forest_p'.
-      assert (p0 <> p) by
-        (unfold not; intros; apply H; subst; constructor).
-      rewrite PTree.gso; auto.
-    - cbn in *.
-      assert (X: ~ PredIn p p0_1 /\ ~ PredIn p p0_2) by
-        (split; unfold not; intros; apply H; constructor; tauto).
-      inversion_clear X as [X1 X2].
-      inv H0. inv H4.
-      specialize (IHp0_1 _ p e _ X1 H0). constructor. tauto.
-      specialize (IHp0_2 _ p e _ X2 H0). constructor. tauto.
-      constructor; auto.
-    - cbn in *.
-      assert (X: ~ PredIn p p0_1 /\ ~ PredIn p p0_2) by
-        (split; unfold not; intros; apply H; constructor; tauto).
-      inversion_clear X as [X1 X2].
-      inv H0. inv H4.
-      specialize (IHp0_1 _ p e _ X1 H0). constructor. tauto.
-      specialize (IHp0_2 _ p e _ X2 H0). constructor. tauto.
-      constructor; auto.
-  Qed.
-
-  Lemma sem_pred_not_in :
-    forall A B G (ctx: @ctx G) (s: @Abstr.ctx G -> A -> B -> Prop) l v p e ps,
-      sem_pred_expr ps s ctx l v ->
-      predicated_not_inP p l ->
-      sem_pred_expr (PTree.set p e ps) s ctx l v.
-  Proof.
-    induction l.
-    - intros. unfold predicated_not_inP in H0.
-      destruct a. constructor. apply sem_pexpr_not_in.
-      eapply H0. econstructor. inv H. auto. inv H. auto.
-    - intros. inv H. constructor. unfold predicated_not_inP in H0.
-      eapply sem_pexpr_not_in. eapply H0. constructor. left. eauto.
-      auto. auto.
-      apply sem_pred_expr_cons_false. apply sem_pexpr_not_in. eapply H0.
-      constructor. tauto. auto. auto.
-      eapply IHl. eauto. eapply predicated_not_inP_cons; eauto.
-  Qed.
-
-  Lemma pred_fold_true' :
-    forall A l pred y,
-      fold_left (fun a (p : positive * predicated A) => a && predicated_not_in pred (snd p)) l y = true ->
-      y = true.
-  Proof.
-    induction l; crush.
-    exploit IHl; try eassumption; intros.
-    eapply andb_prop in H0; tauto.
-  Qed.
-
-  Lemma pred_fold_true :
-    forall A pred l p y,
-      fold_left (fun (a : bool) (p : positive * predicated A) => a && predicated_not_in pred (snd p)) l y = true ->
-      y = true ->
-      list_norepet (map fst l) ->
-      In p l ->
-      predicated_not_in pred (snd p) = true.
-  Proof.
-    induction l; crush.
-    inv H1. inv H2.
-    - cbn in *. now eapply pred_fold_true' in H.
-    - cbn in *; eapply IHl; try eassumption.
-      eapply pred_fold_true'; eauto.
-  Qed.
-
-  Lemma pred_not_in_forestP :
-    forall pred f,
-      predicated_not_in_forest pred f = true ->
-      forall x, predicated_not_inP pred (f #r x).
-  Proof.
-    unfold predicated_not_in_forest, predicated_not_in_pred_expr; intros.
-    destruct (RTree.get x (forest_regs f)) eqn:?.
-    - eapply andb_prop in H. inv H. rewrite PTree.fold_spec in H0.
-      unfold RTree.get in Heqo.
-      exploit pred_fold_true. eauto. auto. apply PTree.elements_keys_norepet.
-      apply PTree.elements_correct; eauto.
-      intros. eapply predicated_not_inP_equiv. unfold "#r".
-      unfold RTree.get. rewrite Heqo. auto.
-    - unfold "#r". rewrite Heqo. unfold predicated_not_inP; intros.
-    inv H0. inversion 1.
-  Qed.
-
-  Lemma pred_not_in_forest_exitP :
-    forall pred f,
-      predicated_not_in_forest pred f = true ->
-      predicated_not_inP pred (forest_exit f).
-  Proof.
-    intros.
-    eapply predicated_not_inP_equiv. unfold predicated_not_in_forest in H.
-    eapply andb_prop in H; tauto.
-  Qed.
-
   Lemma sem_update_Isetpred:
     forall A (ctx: @ctx A) f pr p0 c args b rs m,
       predicated_mutexcl (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f))) ->