Require Import Assertions.
Require Import Guassign.
Require Import Atoms.
Require Import BoundedIteration.
Require Import Kernel.
Require Import KernelVCG.

Lemma atpostfinder_renforce_vc p pre bound l:
  vc_eval (vcl (atpostfinder p pre bound l)) → (vc_eval l).
Proof.
  destruct p; unfold soft_or, ret, bind, check_entails in × |- *; simpl in × |- *;
  intuition eauto with echecker.
Qed.

Hint Resolve atpostfinder_renforce_vc: echecker.

Lemma atpostfinder_increases_bound p pre bound l:
  Zpos bound ≤ Zpos (pbnd (value (atpostfinder p pre bound l))).
Proof.
  destruct p; unfold soft_or, ret, bind, check_entails in × |- *; simpl in × |- *;
  try (intros; omega).
  intros; eauto with echecker.
  intros; eauto with echecker.
Qed.

Hint Resolve atpostfinder_increases_bound: echecker.

Lemma atpostfinder_cbounds_post p pre bound l:
  cbounds bound pre → atbounds bound p
     → cbounds (pbnd (value (atpostfinder p pre bound l))) (post (value (atpostfinder p pre bound l))).
Proof.
  destruct p; unfold soft_or, ret, bind, check_entails in × |- *; simpl in × |- *; try tauto.
  intuition eauto with checker echecker.
  intuition; autorewrite with rchecker; omega.
Qed.

Hint Resolve atpostfinder_cbounds_post: echecker.

Lemma atpostfinder_awlp p pre bound1 bound2 l: vc_eval (vcl (atpostfinder p pre bound2 l)) →
   cbounds bound2 pre → atbounds bound1 p → (Zpos bound1) ≤ (Zpos bound2) →
    ∀ s s0, (frameeq 0 bound1 s0 s) → eval pre s0 →
       awlp p (extend (post (value (atpostfinder p pre bound2 l))) bound1 bound2 s0) s.
Proof.
 destruct p; simpl; unfold soft_or, ret, bind, check_entails, extend; simpl.
intuition.
 eapply guassign_vc; eauto.
intuition.
 eapply ex_intro.
 intuition eauto with checker echecker.
intuition.
 intuition eauto with echecker.
 eapply ex_intro ; intuition eauto with checker echecker.
intuition.
 eapply ex_intro; intuition eauto with checker echecker.
intros X H H0 H1 s s0.
   constructor 1 with (x:=add bound2 (s0 (vid x)) (add (vid x) (teval t s0) s0)); simpl.
   intuition.
   rewrite trename_tbounds; eauto with checker echecker.
   rewrite add_out. auto with checker.
   omega.
   rewrite rename_cbounds; auto.
   unfold frameeq.
   intros; rewrite add_out.
   eapply add_morphism; eauto with echecker.
   omega.
   unfold frameeq.
   intros.
   rewrite add_out.
   rewrite add_out.
   auto.
   omega.
   omega.
Qed.

Notation "'reswf' x" := (cbounds (pbnd x) (post x)) (at level 20).

Section Le_iter_proofs.

Variable body next: cond → positive → aenvironment → monad (postfinder_result cond).
Variable kb kn: (state→ Prop) → state → Prop.
Variable bound1 bound2: positive.

Hypothesis body_renforce_vc: ∀ pre bound aenv l,
  vc_eval (vcl (body pre bound aenv l)) → (vc_eval l).

Hypothesis next_renforce_vc: ∀ pre bound aenv l,
  vc_eval (vcl (next pre bound aenv l)) → (vc_eval l).

Hypothesis body_increases_bound: ∀ pre bound aenv l, Zpos bound ≤ Zpos (pbnd (value (body pre bound aenv l))).

Hypothesis next_increases_bound: ∀ pre bound aenv l, Zpos bound ≤ Zpos (pbnd (value (next pre bound aenv l))).

Hypothesis bound1_bound2: Zpos bound1 ≤ Zpos bound2.

Hypothesis body_reswf: ∀ pre bound aenv l, Zpos bound2 ≤ Zpos bound → cbounds bound pre → aebounds bound aenv →
       reswf (value (body pre bound aenv l)).

Hypothesis next_reswf: ∀ pre bound aenv l, Zpos bound2 ≤ Zpos bound → cbounds bound pre → aebounds bound aenv →
       reswf (value (next pre bound aenv l)).

Hypothesis kb_monotonic:
  ∀ (P Q: state → Prop) s, kb P s →
    (∀ s, P s → Q s) → kb Q s.

Hypothesis kn_monotonic:
  ∀ (P Q: state → Prop) s, kn P s →
    (∀ s, P s → Q s) → kn Q s.

Hypothesis body_kb: ∀ pre bound aenv l, vc_eval (vcl (body pre bound aenv l))
  → Zpos bound2 ≤ Zpos bound → cbounds bound pre → aebounds bound aenv
    → ∀ s s0, (frameeq 0 bound1 s0 s) → eval pre s0 →
       kb (extend (post (value (body pre bound aenv l))) bound1 bound s0) s.

Hypothesis next_kn: ∀ pre bound aenv l, vc_eval (vcl (next pre bound aenv l))
  → Zpos bound2 ≤ Zpos bound → cbounds bound pre → aebounds bound aenv
    → ∀ s s0, (frameeq 0 bound1 s0 s) → eval pre s0 →
       kn (extend (post (value (next pre bound aenv l))) bound1 bound s0) s.

Lemma postfinder_le_iter_renforce_vc n: ∀ ol pre bound aenv z l,
  vc_eval (vcl (postfinder_le_iter n ol body next pre bound aenv z l)) → (vc_eval l).
Proof.
  induction n; simpl; eauto.
Qed.

Lemma postfinder_le_iter_increases_bound_1 n: ∀ ol pre bound aenv z l,
        Zpos bound ≤ Zpos (pbnd (value (postfinder_le_iter n ol body next pre bound aenv z l))).
Proof.
  induction n; simpl; auto with zarith.
  intros; eapply Zle_trans.
  2: eauto.
  eauto.
Qed.
Hint Resolve postfinder_le_iter_increases_bound_1: echecker.

Lemma postfinder_le_iter_increases_bound_2 n: ∀ ol pre bound aenv z l,
     Zpos bound ≤ Zpos (pbnd (snd (post (value (postfinder_le_iter n ol body next pre bound aenv z l))))).
Proof.
  induction n; simpl. auto with zarith.
  intros. eapply Zle_trans.
  2: eapply Zle_Pmax_l.
  eauto.
Qed.
Hint Resolve postfinder_le_iter_increases_bound_2: echecker.

Lemma postfinder_le_iter_cbounds_1 n: ∀ bound ol pre aenv z l,
   Zpos bound2 ≤ Zpos bound → cbounds bound pre → aebounds bound aenv →
        cbounds (pbnd (value (postfinder_le_iter n ol body next pre bound aenv z l)))
                (fst (post (value (postfinder_le_iter n ol body next pre bound aenv z l)))).
Proof.
  induction n; simpl.
  intuition.
  intros bound ol pre aenv z l H H0 H1.
  eapply body_reswf.
    eauto with echecker.
    eapply IHn; eauto.
    eauto with echecker.
Qed.
Hint Resolve postfinder_le_iter_cbounds_1: echecker.

Notation "<<< x , l , z , a >>>" := (value (body (fst (post (value x)))
                                            (pbnd (value x))
                                            (oadd l (fst (post (value x))) z a)
                                            (vcl x))) (at level 20).

Lemma le_iter_tech1 n bound ol pre aenv z l :
  Zpos bound2 ≤ Zpos bound
→
 Zpos bound2 ≤
 Zpos (pbnd (<<< (postfinder_le_iter n ol body next pre bound aenv (z - 1) l), ol, z, aenv >>>)).
Proof.
  intros.
  eapply Zle_trans.
  2: eapply body_increases_bound.
  eauto with echecker.
Qed.
Hint Resolve le_iter_tech1: le_iter_tech.

Lemma le_iter_tech2 n bound ol pre aenv z l :
   Zpos bound2 ≤ Zpos bound
   → cbounds bound pre
   → aebounds bound aenv
   → reswf <<< (postfinder_le_iter n ol body next pre bound aenv (z - 1) l), ol, z, aenv >>>.
Proof.
  intros; eapply body_reswf; eauto.
  eauto with echecker.
  eapply postfinder_le_iter_cbounds_1; eauto.
  apply oadd_aebounds.
  eauto with echecker.
  eapply postfinder_le_iter_cbounds_1; eauto.
Qed.
Hint Resolve le_iter_tech2: le_iter_tech.

Lemma le_iter_tech3 n bound ol pre aenv z l :
   Zpos bound2 ≤ Zpos bound
   → cbounds bound pre
   → aebounds bound aenv
   → aebounds
    (pbnd
       (<<< postfinder_le_iter n ol body next pre bound aenv (z - 1) l, ol, z, aenv >>>))
     (oadd ol
       (post
         (<<< postfinder_le_iter n ol body next pre bound aenv (z - 1) l, ol, z, aenv >>>)) z aenv).
Proof.
 intros; apply oadd_aebounds; auto with le_iter_tech.
 eapply aebounds_Zle; auto with le_iter_tech.
 eauto with echecker.
Qed.
Hint Resolve le_iter_tech3: le_iter_tech.

Lemma postfinder_le_iter_reswf n: ∀ bound ol pre aenv z l, Zpos bound2 ≤ Zpos bound → cbounds bound pre → aebounds bound aenv →
       reswf (snd (post (value (postfinder_le_iter n ol body next pre bound aenv z l)))).
Proof.
  induction n; simpl.
  intuition.
  intros bound ol pre aenv z l H H0 H1.
  constructor 1.
  eapply cbounds_Zle.
    eapply IHn; eauto with echecker.
    eauto with echecker.
  eapply cbounds_Zle.
    eapply next_reswf; auto with le_iter_tech.
    auto with le_iter_tech.
  auto with echecker.
Qed.
Hint Resolve postfinder_le_iter_reswf: echecker.

Lemma postfinder_le_iter_Kwlp_1 n: ∀ bound ol pre aenv z l, Zpos bound2 ≤ Zpos bound
   → vc_eval (vcl (postfinder_le_iter n ol body next pre bound aenv z l))
   → cbounds bound pre → aebounds bound aenv → ∀ s s0, (frameeq 0 bound1 s0 s) → eval pre s0 →
         Kwlp_iter n kb (extend (fst (post (value (postfinder_le_iter n ol body next pre bound aenv z l)))) bound1 bound s0) s.
Proof.
  induction n; simpl.
  unfold extend; intros; eapply ex_intro.
  constructor 1; eauto. intuition.
  intros.
  eapply Kiter_monotonic; auto.
  eapply IHn; eauto.
  unfold extend; intros s1 X.
  decompose [ex and] X; clear X.
  eapply kb_monotonic.
  eapply body_kb; eauto.
  eauto with echecker.
  auto with echecker.
  eauto with echecker.
  unfold extend; intros s2 X; eapply ex_monotonic; eauto.
  clear X; simpl.
  intuition.
  eapply frameeq_trans.
  2: eauto.
  eapply frameeq_Zle; eauto with echecker.
Qed.

Lemma postfinder_le_iter_Kwlp_2 n: ∀ bound ol pre aenv z l, Zpos bound2 ≤ Zpos bound
   → vc_eval (vcl (postfinder_le_iter n ol body next pre bound aenv z l))
   → cbounds bound pre → aebounds bound aenv → ∀ s s0, (frameeq 0 bound1 s0 s) → eval pre s0 →
         Kwlp_le_iter n kb (kn (extend (post (snd (post (value (postfinder_le_iter n ol body next pre bound aenv z l))))) bound1 bound s0)) s.
Proof.
  induction n; simpl.
  intros; eapply next_kn; eauto with echecker.
  intros. constructor 1.
  eapply Kle_iter_monotonic; auto.
  eapply IHn; eauto.
  intros.
  eapply kn_monotonic; eauto.
  unfold extend; intros; eapply ex_monotonic; eauto.
  simpl; intros; intuition.
  eapply Kiter_monotonic; auto.
  eapply postfinder_le_iter_Kwlp_1; eauto.
  unfold extend; intros s1 X.
  decompose [ex and] X; clear X.
  eapply kb_monotonic.
  eapply body_kb; eauto.
  eauto with echecker.
  auto with echecker.
  eauto with echecker.
  unfold extend; intros s2 X; decompose [ex and] X; clear X.
  eapply kn_monotonic.
  eapply next_kn; eauto; auto with le_iter_tech.
  unfold extend; intros s3 X; eapply ex_monotonic; eauto.
  clear X; simpl.
  intuition.
  eapply frameeq_trans.
  2: eauto.
  eapply frameeq_trans.
  2: (eapply frameeq_Zle; eauto with echecker).
  eapply frameeq_Zle; eauto.
  eapply Zle_trans.
  2: eapply body_increases_bound.
  auto with echecker.
Qed.

End Le_iter_proofs.

Fixpoint postfinder_renforce_vc (p:kernel) pre bound aenv l {struct p}:
  vc_eval (vcl (postfinder p pre bound aenv l)) → (vc_eval l).
Proof.
  destruct p; simpl ;
   intro H0;
  unfold soft_or, ret, bind, check_entails in × |- *; simpl in × |- *;
  do_except_on @biter ltac:( intuition eauto with echecker).
  generalize (postfinder_renforce_vc _ _ _ _ _ H0); clear H0; intro H0.
  generalize (postfinder_renforce_vc _ _ _ _ _ H0); clear H0; intro H0.
  eapply postfinder_le_iter_renforce_vc; eauto.
  generalize l H0; clear l H0.
  biter_ind.
  unfold bind; simpl.
  intuition eauto with echecker.
  generalize l H0; clear l H0.
  branch_ind.
  eauto with echecker.
Qed.

Hint Resolve postfinder_renforce_vc: echecker.

Fixpoint postfinder_increases_bound (p:kernel) pre bound aenv l {struct p}:
   Zpos bound ≤ Zpos (pbnd (value (postfinder p pre bound aenv l))).
Proof.
  destruct p; simpl;
  unfold soft_or, ret, bind, check_entails in × |- *; simpl in × |- *; try (intros; omega).
  eapply Zle_trans.
  2: apply Zle_Pmax_l.
  eapply postfinder_le_iter_increases_bound_2; eauto with echecker.
  unfold bind; simpl. generalize l; clear l.
  biter_ind; simpl.
  intros; try omega.
  eauto with echecker.
  auto with echecker.
  unfold bind; simpl; eauto with echecker.
  eauto with echecker.
  eapply Zle_trans.
  2: apply postfinder_increases_bound; eauto with echecker.
  auto with echecker.
  eauto with echecker.
  auto with echecker.
  branch_ind.
Qed.
Hint Resolve postfinder_increases_bound: echecker.

Hint Resolve swap_rbounds: echecker.

Hint Resolve le_iter_tech1 le_iter_tech2 le_iter_tech3: le_iter_tech.

Lemma postfinder_cbounds_reswf (p: kernel):
 ∀ pre bound aenv l,
    cbounds bound pre → Kbounds bound p → aebounds bound aenv →
     reswf (value (postfinder p pre bound aenv l)).
Proof.
  induction p; intros pre bound aenv l; simpl;
  unfold soft_or, ret, bind, check_entails in × |- *; simpl in × |- *; try tauto.
  intuition.
  eapply cbounds_Zle.
    apply postfinder_le_iter_reswf with (bound2:=bound); auto with zarith;
    eauto with echecker.
    auto with echecker.
  cutrewrite (Z_of_nat n = (Z_of_nat n) + 1 - 1); try omega.
  cutrewrite ((Z_of_nat n) + 1 - 1 + 1 = (Z_of_nat n) + 1); try omega.
  eapply cbounds_Zle.
    eapply IHp2.
    eapply le_iter_tech2; eauto with zarith echecker.
    eapply Kbounds_Zle; eauto with le_iter_tech zarith echecker.
  eapply le_iter_tech3; eauto with zarith echecker.
  auto with echecker.
  unfold bind; simpl. intros H1 H2.
  generalize l; clear l.
  biter_ind; simpl; auto.
  intros n K l H3; constructor 1.
  eapply cbounds_Zle.
  eapply H3; auto with zarith echecker.
  auto with zarith echecker.
  eapply cbounds_Zle.
  eapply H; auto with zarith.
  auto with echecker.
  intuition eauto with echecker.
  unfold bind; simpl; intuition.
  eapply IHp2; eauto with echecker.
  intuition eauto with echecker.
  intuition eauto with echecker.
  intuition eauto with echecker.
  intuition. eapply cbounds_Zle; simpl.
  eapply cbounds_rsubst.
  eapply swap_rbounds.
  constructor 1; auto with zarith.
  eapply Zlt_le_trans; eauto.
  eapply Zle_trans.
  2: eapply postfinder_increases_bound.
  auto with echecker.
   simpl.
  constructor 1; auto with zarith.
  eapply Zlt_le_trans; eauto.
  2: eapply postfinder_increases_bound.
  auto with checker.
  simpl.
  apply IHp; simpl; eauto with echecker.
  intuition; autorewrite with rchecker; omega.
  simpl.
  auto with zarith.
  eauto with echecker.
  case (Zeq_bool (abranch (afind (labid label) aenv)) (labmin label)); simpl; intuition.
  branch_ind.
Qed.
Hint Resolve postfinder_cbounds_reswf postfinder_le_iter_increases_bound_1 postfinder_le_iter_cbounds_1: echecker.

Fixpoint postfinder_Kwlp (p: kernel) pre bound1 bound2 aenv l {struct p}:
  vc_eval (vcl (postfinder p pre bound2 aenv l)) →
   cbounds bound2 pre → Kbounds bound1 p → (Zpos bound1) ≤ (Zpos bound2) → aebounds bound2 aenv →
    ∀ s s0, (frameeq 0 bound1 s0 s) → eval pre s0 →
       Kwlp p (extend (post (value (postfinder p pre bound2 aenv l))) bound1 bound2 s0) s.
Proof.
 destruct p; simpl .
  unfold soft_or, ret, bind, check_entails; simpl.
  intros.
  intuition.
  eapply Kle_iter_monotonic. eauto with echecker.
  eapply postfinder_le_iter_Kwlp_2 with (body:=postfinder p1) (next:=postfinder p3) (kb:=Kwlp p1) (kn:=Kwlp p3); eauto with echecker.
  intros; eapply Kwlp_monotonic; eauto.
  unfold extend; intros; eapply ex_monotonic; eauto.
  simpl; intros; intuition.
  eapply Kiter_monotonic. eauto with echecker.
  eapply postfinder_le_iter_Kwlp_1 with (body:=postfinder p1) (next:=postfinder p3) (kb:=Kwlp p1); eauto with echecker.
  unfold extend; intros s1 X.
  decompose [ex and] X; clear X.
  eapply Kwlp_monotonic.
  generalize (postfinder_renforce_vc _ _ _ _ _ H); clear H; intro H.
  eapply postfinder_Kwlp; eauto.
  eauto with zarith echecker.
  eauto with zarith echecker.
  apply oadd_aebounds; eauto with echecker.
  unfold extend; intros s2 X; decompose [ex and] X; clear X.
  eapply Kwlp_monotonic.
  eapply postfinder_Kwlp; eauto.
  cutrewrite (Z_of_nat n = (Z_of_nat n) + 1 - 1); try omega.
  cutrewrite ((Z_of_nat n) + 1 - 1 + 1 = (Z_of_nat n) + 1); try omega.
  eapply le_iter_tech2; eauto with zarith echecker.
  cutrewrite (Z_of_nat n = (Z_of_nat n) + 1 - 1); try omega.
  cutrewrite ((Z_of_nat n) + 1 - 1 + 1 = (Z_of_nat n) + 1); try omega.
  eapply le_iter_tech1; eauto with zarith echecker.
  cutrewrite (Z_of_nat n = (Z_of_nat n) + 1 - 1); try omega.
  cutrewrite ((Z_of_nat n) + 1 - 1 + 1 = (Z_of_nat n) + 1); try omega.
  eapply le_iter_tech3; eauto with zarith echecker.
  unfold extend; intros s3 X; eapply ex_monotonic; eauto.
  clear X; simpl.
  intuition.
  eapply frameeq_trans.
  2: eauto.
  eapply frameeq_trans.
  2: (eapply frameeq_Zle; eauto with echecker).
  eapply frameeq_Zle; eauto.
  eapply Zle_trans.
  2: eapply postfinder_increases_bound.
  auto with echecker.
intros H H0 H1 H2 H3 s s0 H4 H5 z.
  generalize l H; clear l H.
  biter_ind; simpl; auto.
  intros n K H6 H7 l H8 H10.
  biter_split_le H10.
  intros. eapply Kwlp_monotonic.
  eapply H7; eauto with echecker.
  unfold extend; simpl; intros.
  eapply ex_monotonic; eauto.
  simpl; intros; intuition.
  clear H7 H10.
  generalize (postfinder_renforce_vc _ _ _ _ _ H8); simpl.
  intros H9; eapply Kwlp_monotonic.
  eapply postfinder_Kwlp; eauto with echecker.
  unfold extend; intros s1 X; eapply ex_monotonic; eauto.
  simpl; intuition.
intros; eapply atpostfinder_awlp; eauto.
   intuition.
   eapply Kwlp_monotonic.
   eapply postfinder_Kwlp; eauto with echecker.
   unfold extend; intros s1 X; decompose [ex and] X; clear X.
   eapply Kwlp_monotonic.
   eapply postfinder_Kwlp; eauto with echecker.
   unfold extend; intros s2 X; eapply ex_monotonic; eauto.
   clear X; simpl; intuition eauto with echecker.
   intuition.
   generalize (postfinder_renforce_vc _ _ _ _ _ H); simpl.
   intuition.
   eapply Kwlp_monotonic.
   eapply postfinder_Kwlp; eauto with echecker.
   unfold extend; intros s1 X; eapply ex_monotonic; eauto.
   clear X; simpl; intuition eauto with echecker.
   eapply Kwlp_monotonic.
   eapply postfinder_Kwlp; eauto with echecker.
   unfold extend; intros s1 X; eapply ex_monotonic; eauto.
   clear X; simpl; intuition eauto with echecker.
   intuition.
   generalize (postfinder_renforce_vc _ _ _ _ _ H7); simpl.
   intuition.
   eapply Kwlp_monotonic.
   eapply postfinder_Kwlp; eauto with echecker.
   unfold extend; intros s1 X; eapply ex_monotonic; eauto.
   clear X; simpl; intuition eauto with echecker.
   intuition.
   eapply Kwlp_monotonic.
   eapply postfinder_Kwlp; eauto with echecker.
   unfold extend; intros s1 X; eapply ex_monotonic; eauto.
   clear X; simpl; intuition eauto with echecker.
   intuition.
   constructor 1 with (x:=extend (aeval inv aenv) bound1 bound2 s0).
   unfold extend; constructor 1.
   eapply ex_intro; intuition eauto with checker echecker.
   constructor 1.
   intros s' X; decompose [and ex] X; clear X.
   intros; eapply Kwlp_monotonic.
   eapply postfinder_Kwlp; eauto with echecker.
   unfold extend; intros s1 X; eapply ex_monotonic; eauto.
   clear X; simpl; intuition eauto with echecker.
   unfold extend; auto.  intros H0 H1 H2 H3 H4 s s0 H5 H6. intuition.
 eapply Kwlp_monotonic.
 eapply postfinder_Kwlp with (s0:=(add bound2 (s0 (vid x)) (add (vid x) (s0 (vid x)) s0))) (bound2:=(bound2+1)%positive); eauto.
 simpl; intuition; autorewrite with rchecker; omega.
 eauto with echecker.
 eauto with echecker.
 eapply frameeq_trans.
 eapply add_frameeq_out_2; auto.
 eapply frameeq_trans.
 2: apply H5.
 unfold frameeq; intros; rewrite add_id; auto.
 simpl.
 constructor 1.
 rewrite add_out.
 rewrite add_in.
 rewrite add_in; auto.
 omega.
 rewrite rename_cbounds; auto.
 unfold extend; intros s1 X; case X; clear X.
 intros s2 X. case X; clear X.
 intros H9 X; case X; clear X.
 intros H10 H11.
 constructor 1 with (x:=add (vid x) (s2 bound2) (add bound2 (s2 (vid x)) s2)).
 intuition.
 rewrite rsubst_eval_rlift.
 erewrite ext_eval.
 eapply H9.
 intros x0; rewrite swap_rlift.
 simpl.
 rewrite add_in. unfold add at 1.
 case (POrderedType.Positive_as_DT.eq_dec (vid x) x0).
 intros; subst.
 rewrite add_out.
 rewrite add_in.
 auto.
 omega.
 intros; unfold add at 1.
 case (POrderedType.Positive_as_DT.eq_dec bound2 x0).
 intros; subst; auto.
 intros; repeat (rewrite add_out2; auto).
 eapply add_morphism; eauto with echecker.
 unfold frameeq in × |- ×.
 rewrite H11.
 rewrite add_in; intuition.
 intuition.
 eapply frameeq_trans.
 eapply add_frameeq_out_2; auto.
 auto.
 eapply frameeq_trans.
 eapply add_frameeq_out_1; auto.
 eapply frameeq_trans.
 eapply add_frameeq_out_2; auto with zarith.
 eapply frameeq_trans.
 eapply frameeq_Zle.
 eapply H11.
 auto with echecker.
 eapply frameeq_trans.
 eapply add_frameeq_out_2; auto with zarith.
 eapply add_frameeq_out_1; auto with checker.
 eauto with echecker.
  case (Zeq_bool (abranch (afind (labid label) aenv)) (labmin label)); simpl;
  intuition.
intros H H0 H1 H2 H3 s s0 H4 H5.
  generalize l H; clear l H.
  branch_ind.
  simpl.
  intros l H6; case H6; clear H6; intros H6.
  case (H6 _ H5).
  intros z H6 H7 H8; constructor 1 with (x:=z).
  intuition.
Qed.

Definition Kvcg p := vcl (Kvcgen p nil).

Hint Resolve bound_Kbounds: checker.

Theorem Kvcg_correctness (p: kernel):
  vc_eval (Kvcg p) → ∀ s, Kwlp p (fun s ⇒ True) s.
Proof.
  unfold Kvcg, Kvcgen; simpl; intuition.
  eapply Kwlp_monotonic; auto.
  eapply postfinder_Kwlp.
  eapply H.
  simpl; auto with checker.
  auto with checker.
  auto with checker.
  auto with checker.
  unfold frameeq; eauto.
  simpl; auto with checker.
Qed.