Library NPCSoundness

Require Import evidence.
Require Import operationalSemantics.
Require Import soundnessLemmas.
Require Import substLemmas.

Theorem NPCSound : forall phi phi' C s s' X,
(forall x, In x X -> exists v1, lookup s x = Some v1) ->
NPCEvid X phi C phi' -> Opsem s C s' ->
BEval phi' s' = Some true -> BEval phi s = Some true.
Proof.
intros. generalize dependent s. generalize dependent s'.
induction H0; intros.

inv H1. auto.

inv H1. inv H5. erewrite BsubstRes21A; eauto. inv H5. inv H6.

inv H1. inv H5. inv H5. erewrite BsubstRes21B; eauto. inv H6.

inv H3. inv H6. inv H6. inv H7. erewrite BsubstRes21H; eauto.

inv H1. simpl. rewrite H5. rewrite H2. auto.

inv H1.
eapply IHNPCEvid1; eauto. eapply IHNPCEvid2; eauto.
intros. edestruct H0. apply H1. edestruct increasingState.
apply H6. eexists. apply H3. eexists. eauto.

inv H1.

simpl. rewrite H8. erewrite IHNPCEvid1; eauto.
(apply splitAllVarsIn in H; destruct H).
(apply splitAllVarsIn in H1; destruct H1).
(apply splitAllVarsIn in H3; destruct H3).
(apply splitAllVarsIn in H4; destruct H4).
 edestruct EvalCompletes. assert (allVarsIn (fv (BExp phi2)) X = true). auto.
apply H6. apply H0. simpl in H6. destruct (BEval phi2 s). auto. inv H6.

simpl. rewrite H8. erewrite IHNPCEvid2; eauto.
(apply splitAllVarsIn in H; destruct H).
(apply splitAllVarsIn in H1; destruct H1).
(apply splitAllVarsIn in H3; destruct H3).
(apply splitAllVarsIn in H4; destruct H4).
edestruct EvalCompletes. assert (allVarsIn (fv (BExp phi1)) X = true).
auto. apply H6. apply H0. simpl in H6. destruct (BEval phi1 s). simpl. destruct b; auto.
inv H6.

assert (x:=l51 C s s'). rewrite <- H2. apply lookupsSameEvalSameB.
intros. apply x. subst. apply intersectionNullSymmetry2 in H1.
eapply intersectionNullNotIn in H1. apply H1. auto. auto.

remember (WHILE B DO C). induction H4; inv Heqc. apply H1. simpl.
rewrite H4. rewrite H2. auto.

eapply IHNPCEvid. apply IHOpsem2. apply H2. intros.
edestruct increasingState. apply H4_. apply H3. apply H5. eauto.
auto. apply H3. apply H4_.

Qed.