Lvc.Spilling.AnnP

Require Import List Map Env AllInRel Exp AppExpFree RenamedApart.
Require Import IL Annotation AutoIndTac.
Require Import Liveness.Liveness LabelsDefined.

Set Implicit Arguments.

AnnP


Inductive ann_P
           (A : Type)
           (P : A Prop)
  : ann A Prop
  :=
  | annP0
      (a : A)
    : P a
       ann_P P (ann0 a)
  | annP1
      (a : A)
      (an : ann A)
    : P a
       ann_P P an
       ann_P P (ann1 a an)
  | annP2
      (a : A)
      (an1 an2 : ann A)
    : P a
       ann_P P an1
       ann_P P an2
       ann_P P (ann2 a an1 an2)
  | ann_PF
      (a : A)
      (anF : list (ann A))
      (an2 : ann A)
    : P a
       ( (an1 : ann A) n,
             get anF n an1
              ann_P P an1)
       ann_P P an2
       ann_P P (annF a anF an2)
.

Lemma ann_P_get
      (A : Type)
      (P : A Prop)
      (a : ann A)
  :
    ann_P P a P (getAnn a)
.
Proof.
  intro annP.
  induction annP; eauto.
Qed.

Instance ann_P_impl A
  : Proper (@pointwise_relation _ _ impl ==> eq ==> impl) (@ann_P A).
Proof.
  unfold Proper, respectful, impl; intros; subst.
  general induction H1; eauto using ann_P.
Qed.

Instance ann_P_iff A
  : Proper (@pointwise_relation _ _ iff ==> eq ==> iff) (@ann_P A).
Proof.
  unfold Proper, respectful, impl; intros; subst; split; intros.
  eapply ann_P_impl; eauto.
  eapply pointwise_subrelation; eauto using iff_impl_subrelation.
  eapply ann_P_impl; eauto.
  eapply pointwise_subrelation; eauto using iff_impl_subrelation.
  eapply pointwise_symmetric; eauto using CRelationClasses.iff_Symmetric.
Qed.

Lemma ann_P_setTopAnn A (P:AProp) an a
  : ann_P P an
     P a
     ann_P P (setTopAnn an a).
Proof.
  intros AN PA; inv AN; simpl; econstructor; eauto.
Qed.