Library soundnessLemmas

Require Import soundness.
Require Import language.
Require Import evidence.
Require Import varLists.

Lemma twoAssnsFvSplit : forall a b, TwoAssnsFv a ++ TwoAssnsFv b = TwoAssnsFv (a++b).
intros. induction a. simpl. auto. destruct a. simpl. rewrite <- app_assoc. rewrite IHa. auto. Qed.

Lemma tAssnInterpApp: forall s s' Theta Theta1, twoAssnsInterpretation s s' (Theta ++ Theta1) ->
twoAssnsInterpretation s s' Theta /\ twoAssnsInterpretation s s' Theta1.
intros. induction Theta. simpl. auto. simpl. simpl in H. inv H.
assert (twoAssnsInterpretation s s' Theta /\ twoAssnsInterpretation s s' Theta1).
apply IHTheta. apply H1. destruct H.
split. split. apply H0.
 auto. auto.
Qed.

Lemma tAssnAppInterp: forall s s' Theta Theta1,
twoAssnsInterpretation s s' Theta -> twoAssnsInterpretation s s' Theta1 ->
twoAssnsInterpretation s s' (Theta ++ Theta1).
intros. induction Theta. simpl. apply H0. simpl. split. simpl in H. destruct H.
apply H.
apply IHTheta. simpl in H. destruct H. apply H1.
Qed.

Lemma containsInterp: forall s s' Theta a, true = contains Theta a ->
twoAssnsInterpretation s s' Theta ->
twoAssnsInterpretation s s' [a].
intros. simpl. split; try auto. destruct a. constructor. intros.
induction Theta. simpl in H. inv H. simpl in H.
remember (twoAssnEqual a (b,e)). destruct b0.
simpl in H0. destruct H0. destruct a. inv H0. apply twoAssnEqual_eq in Heqb0.
inv Heqb0. apply H5; auto. apply IHTheta. auto. simpl in H0. destruct H0. auto.
Qed.

Lemma andIntoThetaTrue: forall s s' Theta B, BEval B s = Some true -> BEval B s' = Some true ->
twoAssnsInterpretation s s' (andIntoTheta Theta B) -> twoAssnsInterpretation s s' Theta.
intros. induction Theta. auto. simpl. split.
clear IHTheta. destruct a. simpl in H1. destruct H1. clear H2. inv H1. constructor. intros.
simpl in H3. rewrite H0 in H3. rewrite H in H3. rewrite H1 in H3. rewrite H2 in H3.
apply H3; auto. apply IHTheta. destruct a. simpl in H1. destruct H1. apply H2.
Qed.

Theorem conBoolAgreementMustExist: forall phi1 phi2 E1 E2 Theta1 Theta2 B,
In (phi1, E1) Theta1 -> In (phi2, E2) Theta2 ->
In ((phi1 b&& B) b|| (phi2 b&& (! B)), BExp B) (conBoolAgreement Theta1 Theta2 B).
intros. generalize dependent Theta2. induction Theta1. inv H. destruct H. Focus 2.
assert (x:=(IHTheta1 H)). clear IHTheta1.
intros. assert (y:=(x _ H0)). clear x. destruct a. simpl. apply in_or_app. right. assumption.
subst. intros. clear IHTheta1.
induction Theta2. inv H0. destruct H0. Focus 2. assert (x:=IHTheta2 H). clear IHTheta2. destruct a.
simpl. clear H. right. simpl in x. apply in_app_or in x. destruct x. apply in_or_app. left. assumption.
apply in_or_app. right.
generalize dependent Theta2.
induction Theta1. intros. inv H. intros. destruct a. simpl in H.
apply in_app_or in H. destruct H. simpl. right. apply in_or_app. left. apply H.
simpl. right. apply in_or_app. right. apply IHTheta1. apply H. subst. simpl. left. auto.
Qed.

Theorem bevalToEval: forall b s, BEval b s= Some true -> Eval (BExp b) s= Some (BValue true).
intros. simpl. remember (BEval b s). destruct o. inv H. auto. inv H.
Qed.

Theorem AevalCompletes: forall X e s, allVarsIn (fv (AExp e)) X=true -> (forall x, In x X -> exists v, lookup s x = Some v) ->
 exists v1, AEval e s = Some v1.
intros.
induction e using AExpr_ind_mut with
(P:= fun h => allVarsIn (fv (HExp h)) X=true -> (forall x, In x X -> exists v, lookup s x = Some v) ->
 exists v1, HEval h s = Some v1); intros.
simpl in *.
 remember (skalVarIn (HSkalVar h) X). destruct b. assert (exists v, lookup s (HSkalVar h) = Some v).
apply H0. symmetry in Heqb. apply skalVarInIn in Heqb. auto. inv H2. simpl in H3. destruct (snd s h); inv H3; eauto. inv H.
simpl. eauto.

simpl in *. apply splitAllVarsIn in H. destruct H. apply splitAllVarsIn in H2. destruct H2.
assert (exists v, AEval e1 s = Some v). apply IHe2. auto. destruct H4. rewrite H4.
assert (exists v, AEval e2 s = Some v). apply IHe3. auto. destruct H5. rewrite H5.
assert (exists v1 : HVal, HEval h s = Some v1). apply IHe1. auto. auto. destruct H6. rewrite H6.
eauto.

assert (exists v, lookup s (ASkalVar a) = Some v). apply H0.
simpl in H. induction X. inv H. simpl. simpl in H. remember (beq_SkalVar (ASkalVar a) a0).
destruct b. symmetry in Heqb. apply beq_SkalVar_eq in Heqb. left. auto.
right. apply IHX; try assumption. simpl in H0. intros. destruct (H0 x). right. apply H1. exists x0. apply H2.
destruct H1. destruct x. exists a0.
simpl. simpl in H1. remember (fst (fst s) a). destruct o. inv H1. auto. inv H1. inv H1. simpl. destruct (fst (fst s) a); inv H3.
simpl in *. destruct (fst (fst s) a); inv H1.

simpl in *. eauto.

simpl in *. remember (AEval e1 s). destruct o. remember (AEval e2 s). destruct o.
eexists. auto. apply IHe2. apply splitAllVarsIn in H. destruct H.
apply H1. apply IHe1. apply splitAllVarsIn in H. destruct H. apply H.

simpl in *. apply splitAllVarsIn in H. destruct H.
intuition. destruct H3. destruct H4. rewrite H2. rewrite H3. eexists. reflexivity.
Qed.

Theorem HevalCompletes: forall X e s, allVarsIn (fv (HExp e)) X=true -> (forall x, In x X -> exists v, lookup s x = Some v) ->
 exists v1, HEval e s = Some v1.
Proof. intros. induction e. simpl in H. remember (skalVarIn (HSkalVar h) X). destruct b.
symmetry in Heqb. apply skalVarInIn in Heqb. simpl. assert (H3 := H0 (HSkalVar h) Heqb).
destruct H3. simpl in H1. destruct (snd s h); inv H1. eauto. inv H.
simpl in *. eauto. simpl in *. apply splitAllVarsIn in H. destruct H.
apply splitAllVarsIn in H1. destruct H1.

intuition. edestruct AevalCompletes. simpl. apply H2. eauto.
edestruct AevalCompletes. simpl. apply H1. eauto. rewrite H4.
rewrite H5. destruct H3. rewrite H3. eauto.
Qed.

Theorem BevalCompletes: forall X e s, allVarsIn (fv (BExp e)) X=true -> (forall x, In x X -> exists v, lookup s x = Some v) ->
 exists v1, Eval (BExp e) s = Some v1.
intros.
induction e. assert (exists v, lookup s (BSkalVar b) = Some v). apply H0.
simpl in H. induction X. inv H. simpl. simpl in H. remember (beq_SkalVar (BSkalVar b) a). destruct b0.
left. symmetry in Heqb0. apply beq_SkalVar_eq in Heqb0. auto.
right. apply IHX; try assumption. simpl in H0. intros. destruct (H0 x). right. apply H1.
exists x0. apply H2. inv H1. exists x. simpl. simpl in H2. destruct (snd (fst s) b). apply H2. inv H2.
eexists; simpl; auto.
simpl in H. apply splitAllVarsIn in H. destruct H. simpl. destruct (AevalCompletes X a s). simpl. apply H. apply H0. rewrite H2.
destruct (AevalCompletes X a0 s). simpl. assumption. assumption. rewrite H3. eexists. auto.

simpl in *. apply splitAllVarsIn in H. destruct H. remember (BEval e1 s). destruct o. remember (BEval e2 s). destruct o. eexists. auto.
apply IHe2; assumption. apply IHe1; assumption.

simpl in *. apply splitAllVarsIn in H. destruct H. remember (BEval e1 s). destruct o. remember (BEval e2 s). destruct o. eexists. auto.
apply IHe2; assumption. apply IHe1; assumption.

simpl in *. remember (BEval e s). destruct o. eexists; auto. apply IHe. apply H.
Qed.

Theorem EvalCompletes: forall X e s, allVarsIn (fv e) X=true -> (forall x, In x X -> exists v, lookup s x = Some v) ->
 exists v1, Eval e s = Some v1.
intros. destruct e. simpl. destruct (AevalCompletes X a s). apply H. apply H0. rewrite H1. eexists; auto.
destruct (BevalCompletes X b s). apply H. apply H0. eexists. apply H1.

simpl in H. simpl in *. edestruct HevalCompletes; eauto. rewrite H1. eauto.
Qed.

Lemma allVarsInASubstA : forall a A x X, allVarsIn (AFv A) X = true -> allVarsIn (AFv a) X = true ->
allVarsIn (AFv (ASubstA a A x)) X =true.
intros. induction a using AExpr_ind_mut with
(P:= fun h => allVarsIn (AFv A) X = true -> allVarsIn (HFv h) X = true ->
allVarsIn (HFv (HSubstA h A x)) X =true); intros; auto.

simpl in *. apply splitAllVarsIn in H1. destruct H1.
apply splitAllVarsIn in H2. destruct H2. intuition. repeat (apply allVarsInSplit); auto.

unfold ASubstA. simpl. simpl in H0. destruct (beq_SkalVar x (ASkalVar a)). apply H.
simpl. destruct (skalVarIn (ASkalVar a) X). auto. inv H0.
simpl. auto.
simpl. simpl in H0. apply splitAllVarsIn in H0. destruct H0. apply allVarsInSplit. apply IHa1. apply H0.
apply IHa2. apply H1.

simpl in *. apply splitAllVarsIn in H0. destruct H0. intuition. apply allVarsInSplit; auto.
Qed.

Lemma allVarsInASubstH : forall a A x X, allVarsIn (HFv A) X = true -> allVarsIn (AFv a) X = true ->
allVarsIn (AFv (ASubstH a A x)) X =true.
Proof.
intros. induction a using AExpr_ind_mut with
(P:= fun h => allVarsIn (HFv A) X = true -> allVarsIn (HFv h) X = true ->
allVarsIn (HFv (HSubstH h A x)) X =true); intros; auto.

simpl in *. remember (skalVarIn (HSkalVar h) X). destruct b; inv H1.
remember (beq_SkalVar x (HSkalVar h)). destruct b. auto. simpl. rewrite <- Heqb.
auto.

simpl in *. apply splitAllVarsIn in H1. destruct H1. apply splitAllVarsIn in H2.
destruct H2. intuition. repeat apply allVarsInSplit; auto.

simpl in *. apply splitAllVarsIn in H0. destruct H0. intuition. apply allVarsInSplit; auto.

simpl in *. apply splitAllVarsIn in H0. intuition. apply allVarsInSplit; auto.
Qed.

Lemma allVarsInHSubstH : forall a A x X, allVarsIn (HFv A) X = true -> allVarsIn (HFv a) X = true ->
allVarsIn (HFv (HSubstH a A x)) X =true.
intros. induction a; auto; simpl in *.

remember (beq_SkalVar x (HSkalVar h)). destruct b. auto. simpl.
rewrite H0. auto.

apply splitAllVarsIn in H0. destruct H0. apply splitAllVarsIn in H1. destruct H1. intuition.
repeat apply allVarsInSplit; auto. apply allVarsInASubstH; auto.
apply allVarsInASubstH; auto.

Qed.

Lemma allVarsInHSubstA : forall a A x X, allVarsIn (AFv A) X = true -> allVarsIn (HFv a) X = true ->
allVarsIn (HFv (HSubstA a A x)) X =true.
Proof.
intros. induction a; simpl in *; auto. apply splitAllVarsIn in H0. destruct H0.
 apply splitAllVarsIn in H1. destruct H1. intuition.
repeat (apply allVarsInSplit); auto. apply allVarsInASubstA; auto. apply allVarsInASubstA; auto.
Qed.

Lemma allVarsInBSubstA : forall b A x X, allVarsIn (BFv b) X = true -> allVarsIn (AFv A) X = true ->
(allVarsIn (BFv (BSubstA b A x)) X)=true.
intros. induction b. unfold BSubstA. simpl. simpl in H. destruct (skalVarIn (BSkalVar b) X). auto. inversion H.
simpl. auto.
simpl. simpl in H. apply splitAllVarsIn in H. destruct H. apply allVarsInSplit.
apply allVarsInASubstA; assumption. apply allVarsInASubstA; assumption.
simpl in H. apply splitAllVarsIn in H. destruct H. simpl. apply allVarsInSplit.
apply IHb1. assumption. apply IHb2. assumption.
simpl in H. apply splitAllVarsIn in H. destruct H. simpl. apply allVarsInSplit.
apply IHb1. assumption. apply IHb2. assumption.
simpl in H. simpl. apply IHb. assumption.
Qed.

Lemma allVarsInBSubstH : forall b A x X, allVarsIn (BFv b) X = true -> allVarsIn (HFv A) X = true ->
(allVarsIn (BFv (BSubstH b A x)) X)=true.
Proof.
intros.
induction b; simpl in *; auto.
apply splitAllVarsIn in H. destruct H. apply allVarsInSplit;
apply allVarsInASubstH; auto.
apply splitAllVarsIn in H. destruct H. intuition. apply allVarsInSplit; auto.
apply splitAllVarsIn in H. destruct H. intuition. apply allVarsInSplit; auto.

Qed.

Lemma allVarsInBSubstB : forall b A x X, allVarsIn (BFv b) X = true -> allVarsIn (BFv A) X = true ->
(allVarsIn (BFv (BSubstB b A x)) X)=true.
intros. induction b. simpl. simpl in H. destruct (beq_SkalVar x (BSkalVar b)). apply H0. simpl.
destruct (skalVarIn (BSkalVar b) X). auto. inv H.
auto. simpl. simpl in H. apply splitAllVarsIn in H. destruct H. apply allVarsInSplit; assumption.
simpl in *. apply splitAllVarsIn in H. destruct H. apply allVarsInSplit. apply IHb1; assumption.
apply IHb2. assumption.
simpl in *. apply splitAllVarsIn in H. destruct H. apply allVarsInSplit. apply IHb1; assumption.
apply IHb2. assumption.
simpl. apply IHb. apply H.
Qed.

Lemma andIntoThetaFV :forall Theta1 X B, allVarsIn (TwoAssnsFv Theta1) X = true ->
allVarsIn (BFv B) X = true ->
allVarsIn (TwoAssnsFv (andIntoTheta Theta1 B)) X = true.
intros.
induction Theta1. simpl. auto. destruct a. simpl.
simpl in H. apply splitAllVarsIn in H. destruct H. apply splitAllVarsIn in H.
destruct H.
repeat (apply allVarsInSplit). simpl in H.

apply H. apply H0. apply H2. apply IHTheta1. apply H1.
Qed.

Lemma conBoolAgreementHelpFV: forall b Theta2 B X,
allVarsIn (BFv b) X = true ->
allVarsIn (TwoAssnsFv Theta2) X = true ->
allVarsIn (BFv B) X = true ->
allVarsIn (TwoAssnsFv (conBoolAgreementHelp b Theta2 B)) X = true.
intros.
induction Theta2. simpl. auto.
destruct a. simpl in *. apply splitAllVarsIn in H0.
destruct H0. apply splitAllVarsIn in H0. destruct H0.
repeat (apply allVarsInSplit); try assumption. apply IHTheta2; try assumption.
Qed.


Lemma conBoolAgreementFV: forall Theta1 Theta2 B X,
allVarsIn (TwoAssnsFv Theta1) X= true ->
allVarsIn (TwoAssnsFv Theta2) X=true ->
allVarsIn (BFv B) X = true ->
allVarsIn (TwoAssnsFv (conBoolAgreement Theta1 Theta2 B)) X = true.
intros. induction Theta1. simpl. auto.
destruct a. simpl in *. apply splitAllVarsIn in H.
destruct H. apply splitAllVarsIn in H. destruct H.
 rewrite <- twoAssnsFvSplit.
apply allVarsInSplit. apply conBoolAgreementHelpFV; assumption.
apply IHTheta1; assumption.
Qed.

Theorem andIntoThetaSplit: forall Theta B X,
allVarsIn (TwoAssnsFv (andIntoTheta Theta B)) X = true ->
allVarsIn (TwoAssnsFv Theta) X = true.
intros. induction Theta. simpl. auto.
destruct a. simpl in H. repeat (apply splitAllVarsIn in H; destruct H).
simpl. repeat (apply allVarsInSplit); try assumption. apply IHTheta. apply H0.
Qed.

Theorem assnInassns: forall x1 x2 X Theta, In (x1,x2) Theta -> allVarsIn (TwoAssnsFv Theta) X = true ->
allVarsIn (BFv x1) X = true.
intros. induction Theta. inv H.
simpl in H. simpl in H0. apply splitAllVarsIn in H0. destruct H0.
destruct H. subst. clear IHTheta. apply splitAllVarsIn in H0. destruct H0. apply H.

apply IHTheta. apply H. apply H1.
Qed.

Theorem twoAssnsSubset: forall Theta e s s', twoAssnsInterpretation s s' Theta -> In e Theta ->
twoAssnsInterpretation s s' [e].
intros. simpl. split; auto. destruct e. constructor. intros. induction Theta. inv H0.
simpl in H0. destruct H0. subst. simpl in H. destruct H. inv H. apply H4; assumption.
apply IHTheta. simpl in H. destruct H. apply H3. apply H0.
Qed.

Theorem subsetTwoAssnsInterpretation: forall s s' th Theta, In th Theta -> twoAssnsInterpretation s s' Theta
-> twoAssnsInterpretation s s' [th].
Proof.
intros. simpl. split; auto. destruct th. constructor. intros.
induction Theta. inv H.
inv H0. inv H3. simpl in H. destruct H. inv H. apply H0; assumption.
apply IHTheta; assumption.
Qed.


Theorem condMismatch: forall t t' s s' X Theta1 Theta2 Theta B C1 C2,
backSat X C1 (Assns Theta1 Theta) ->
backSat X C2 (Assns Theta2 Theta) ->
(forall x : SkalVar,
     In x X ->
     exists v1 : Val,
       lookup s x = Some v1 /\ (exists v2 : Val, lookup s' x = Some v2)) ->
twoAssnsInterpretation s s' (andIntoTheta Theta1 B) ->
twoAssnsInterpretation s s' (andIntoTheta Theta2 (!B)) ->
twoAssnsInterpretation s s' (conBoolAgreement Theta1 Theta2 B) ->
allVarsIn (TwoAssnsFv Theta1) X = true ->
allVarsIn (TwoAssnsFv Theta2) X = true ->
BEval B s' = Some true ->
Opsem s' C1 t' ->
BEval B s = Some false ->
Opsem s C2 t ->
twoAssnsInterpretation t t' Theta.
Proof.
intros.
unfold backSat in H.
 induction Theta. simpl. auto.
simpl. split. clear IHTheta. destruct a. constructor. intros.
edestruct H; try eassumption. simpl. left. auto.
intros. edestruct H1. apply H13. repeat destruct H14. destruct H15.
exists x1. apply H14.
destruct H13. destruct H13.
clear H. unfold backSat in H0.
edestruct H0; try eassumption. simpl. left. auto.
intros.
edestruct H1. apply H. destruct H15. destruct H16. exists x2. apply H15.
destruct H. destruct H.
assert (y:=conBoolAgreementMustExist x x1 x0 x2 Theta1 Theta2 B H13 H).
assert (z: twoAssnsInterpretation s s' ([((x b&& B) b|| x1 b&& !B, BExp B)])). Focus 2.
simpl in z.
inv z. inv H16.
assert (Eval (BExp B) s = Eval (BExp B) s').
  apply H19. simpl. rewrite H9. rewrite H15. destruct (EvalCompletes X (BExp x) s).
simpl.
eapply assnInassns. eassumption. assumption. intros.
assert (exists v1 : Val, lookup s x3 = Some v1 /\ (exists v2 : Val, lookup s' x3 = Some v2)).
apply H1. assumption. destruct H18. destruct H18. eexists. apply H18. simpl in H16.
destruct (BEval x s). simpl. destruct b0; auto. inv H16. simpl.
rewrite H7. rewrite H14. destruct (EvalCompletes X (BExp x1) s'). simpl.
eapply assnInassns. eassumption. assumption.
intros. assert (exists v1 : Val, lookup s x3 = Some v1 /\ (exists v2 : Val, lookup s' x3 = Some v2)).
apply H1; assumption. destruct H18. destruct H18. destruct H20.
exists x5. assumption. simpl in H16. destruct (BEval x1 s'); inv H16.
simpl. auto. simpl in H16. rewrite H9 in H16. rewrite H7 in H16. inv H16.
eapply subsetTwoAssnsInterpretation; eassumption. apply IHTheta; try assumption. intros.
eapply H. apply H11. simpl. right. apply H12. apply H13. assumption. unfold backSat in H0.
unfold backSat. intros. eapply H0. apply H11. simpl. right. apply H12. apply H13.
assumption.
Qed.

Theorem twoAssnsStatesSymmetry: forall s s' Theta, twoAssnsInterpretation s s' Theta <->
twoAssnsInterpretation s' s Theta.
split; intros. induction Theta. simpl. auto.
simpl in *. destruct H. split. inv H. constructor. intros. symmetry. apply H1; assumption.
apply IHTheta. assumption.

induction Theta. simpl. auto.
simpl in *. destruct H. split. inv H. constructor. intros. symmetry. apply H1; assumption.
apply IHTheta. assumption.
Qed.

Theorem andIntoThetaMustExist: forall phi B e Theta, In (phi, e) Theta -> In (phi b&& B, e) (andIntoTheta Theta B).
Proof.
intros. induction Theta. auto. destruct a. destruct H. inv H. left. auto.
right. apply IHTheta. auto.
Qed.

Lemma appCons: forall L (x:SkalVar) L2, (L++[x])++L2 = L++x::L2.
intros. induction L. simpl. auto. simpl. rewrite IHL. auto.
Qed.


Lemma l51 : forall C s t x, ~In x (Mods C) ->
Opsem s C t -> lookup s x = lookup t x.
Proof.
intros. induction H0. auto. rewrite <- IHOpsem2. rewrite IHOpsem1. auto.
simpl in H. intuition. simpl in H. intuition.
subst. simpl in H. intuition. destruct x0. destruct s. destruct p. simpl.
destruct x. simpl. remember (a0 a1). destruct o.
remember (beq_SkalVar (ASkalVar (AId z)) (ASkalVar a1)).
destruct b0. symmetry in Heqb0. apply beq_SkalVar_eq in Heqb0. inv Heqb0.
clear H2. destruct H0. auto. auto.
remember (beq_SkalVar (ASkalVar (AId z)) (ASkalVar a1)). destruct b0.
symmetry in Heqb0. apply beq_SkalVar_eq in Heqb0. inv Heqb0. intuition.
auto.
intuition. intuition.

subst. simpl in H. intuition. clear H2. destruct x0. destruct s. destruct p. simpl.
destruct x. simpl. remember (a a0). destruct o. auto. auto. simpl.
remember (b0 b1). destruct o. remember (beq_SkalVar (BSkalVar (BId z)) (BSkalVar b1)).
destruct b3. symmetry in Heqb3. apply beq_SkalVar_eq in Heqb3. inv Heqb3. intuition.
auto. remember (beq_SkalVar (BSkalVar (BId z)) (BSkalVar b1)).
destruct b2. symmetry in Heqb2. apply beq_SkalVar_eq in Heqb2. intuition.
auto. auto. simpl in H. intuition.

subst. simpl in *. intuition. clear H2. destruct x0. destruct s. destruct p. simpl.
destruct x. simpl. remember (a a0). destruct o. auto. auto. simpl.
remember (b b0). destruct o. auto. auto. simpl. remember (beq_SkalVar (HSkalVar (HId z)) (HSkalVar h1)).
destruct b0. symmetry in Heqb0. apply beq_SkalVar_eq in Heqb0. inv Heqb0. intuition.
auto.

simpl in H. intuition.

simpl in *. intuition.

simpl in *. intuition.

simpl in *. intuition.

simpl in *. intuition. rewrite H1. rewrite H2. auto.

simpl in *. intuition.

subst.
assert ( H4' :
  forall i : nat,
     i <= ZZeroMax v ->
     lookup (f i) x = lookup (f (S i)) x).
  intros i X1. assert (X := H4 i X1). destruct (f i). destruct p. simpl in *. destruct x. simpl in *.
remember (beq_SkalVar (ASkalVar q) (ASkalVar a0)). destruct b0. symmetry in Heqb0. apply beq_SkalVar_eq in Heqb0.
inv Heqb0. intuition. auto. auto. auto.
  clear H4.

cut (forall i : nat,
      (i <= ZZeroMax v) ->
      (In x (Mods C) -> False) -> lookup (f 0) x = lookup (f (S i)) x).
intros HH. rewrite lookupNeqa. destruct (ZZeroMax v). auto. apply HH. auto. auto.
remember (beq_SkalVar (ASkalVar q) x). destruct b. symmetry in Heqb. apply beq_SkalVar_eq in Heqb.
intuition. auto.

intros i. induction i; intros. apply H4'. auto. auto. rewrite <- H4'. apply IHi. intuition. auto.
intuition. simpl in *. destruct s. destruct p. simpl in *.

destruct x; simpl. remember (beq_SkalVar (ASkalVar q) (ASkalVar a0)). destruct b0.
intuition. symmetry in Heqb0. apply beq_SkalVar_eq in Heqb0. inv Heqb0. intuition.
auto. auto. auto.
Qed.

Lemma splitBIn: forall v L1 L2, skalVarIn v (L1 ++ L2)=skalVarIn v L1 || skalVarIn v L2.
intros. induction L1. simpl. auto. simpl. rewrite IHL1. destruct (beq_SkalVar v a). auto.
auto.
Qed.

Lemma lookupsSameEvalSameA: forall s s' e , (forall v, In v (AFv e) -> lookup s v = lookup s' v) ->
AEval e s = AEval e s'.
intros. induction e using AExpr_ind_mut with
(P:=fun h => (forall v, In v (HFv h) -> lookup s v = lookup s' v) ->
HEval h s = HEval h s').

simpl. assert (lookup s (HSkalVar h) = lookup s' (HSkalVar h)). apply H.
simpl. left. auto. simpl in H0. destruct (snd s h); destruct (snd s' h); inv H0; auto.
auto.

simpl in *. rewrite IHe2. rewrite IHe3. rewrite IHe1. auto.
intros. apply H. intuition. intros; apply H; intuition. intros. apply H.
intuition.

 simpl. assert (lookup s (ASkalVar a) = lookup s' (ASkalVar a)).
apply H. simpl. auto.
simpl in H0. destruct (fst (fst s) a). destruct (fst (fst s') a). inv H0. auto. inv H0.
destruct (fst (fst s') a). inv H0. auto. simpl. auto. simpl.
rewrite IHe2. rewrite IHe1. auto. intros. apply H. simpl. apply in_or_app. left.
assumption. intros. apply H. simpl. apply in_or_app. right. auto.

simpl in *. rewrite IHe. rewrite IHe0. auto. intros; apply H; intuition.
intros; apply H; intuition.
Qed.

Lemma lookupsSameEvalSameH: forall s s' e , (forall v, In v (HFv e) -> lookup s v = lookup s' v) ->
HEval e s = HEval e s'.
Proof.
intros. induction e.
simpl in *. assert (lookup s (HSkalVar h) = lookup s' (HSkalVar h)). apply H. auto.
simpl in H0. destruct (snd s h); destruct (snd s' h); inv H0; auto.

auto.

simpl in *. rewrite IHe. erewrite (lookupsSameEvalSameA s s').
erewrite (lookupsSameEvalSameA s s'); auto.
intros. apply H. intuition.
intros. apply H. intuition.
intros. apply H. intuition.
Qed.

Lemma lookupsSameEvalSameB: forall s s' e , (forall v, In v (BFv e) -> lookup s v = lookup s' v) ->
BEval e s = BEval e s'.
Proof.
intros. induction e; simpl; try auto.
assert (lookup s (BSkalVar b) = lookup s' (BSkalVar b)).
apply H. simpl. auto.
simpl in H0. destruct (snd (fst s) b). destruct (snd (fst s') b). inv H0.
 auto.
inv H0. destruct (snd (fst s') b). inv H0. auto.
assert (AEval a s = AEval a s'). apply lookupsSameEvalSameA. intros.
apply H. simpl. apply in_or_app. left. assumption. rewrite H0.
assert (AEval a0 s = AEval a0 s'). apply lookupsSameEvalSameA. intros.
apply H. simpl. apply in_or_app. right. assumption. rewrite H1. auto.

rewrite IHe1. rewrite IHe2. auto. intros. apply H. simpl. apply in_or_app.
right. assumption. intros. apply H. simpl. apply in_or_app. left. assumption.

rewrite IHe1. rewrite IHe2. auto. intros. apply H. simpl. apply in_or_app.
right. assumption. intros. apply H. simpl. apply in_or_app. left. assumption.

rewrite IHe. auto. apply H.
Qed.

Lemma opsemSameEvalSameA: forall e t t' s s' C, Opsem s C t -> Opsem s' C t' ->
AEval e s = AEval e s' ->
IntersectionNullP (fv (AExp e)) (Mods C) -> AEval e t = AEval e t'.
intros. assert (x:=(l51 C s t)).
assert (y:=lookupsSameEvalSameA s t e).
rewrite <- y. Focus 2. intros. apply x. auto. simpl in H2.
assert (z:=intersectionNullNotIn v (AFv e) (Mods C)).
assert (~ In v (Mods C)). apply z. assumption. assumption.
apply inSkalVarInFalse in H4. symmetry in H4. rewrite <- skalVarInIn.
unfold not. intros. rewrite <- H4 in H5. inv H5. apply H.
clear x. clear y. assert (x:=(l51 C s' t')).
assert (y:=lookupsSameEvalSameA s' t' e).
rewrite <- y. Focus 2. intros. apply x. auto. simpl in H2.
assert (z:=intersectionNullNotIn v (AFv e) (Mods C)).
assert (~ In v (Mods C)). apply z. assumption. assumption.
apply inSkalVarInFalse in H4. symmetry in H4. rewrite <- skalVarInIn.
unfold not. intros. rewrite <- H4 in H5. inv H5.
assumption.
assumption.
Qed.

Lemma opsemSameEvalSameB: forall e t t' s s' C, Opsem s C t -> Opsem s' C t' ->
BEval e s = BEval e s' ->
IntersectionNullP (fv (BExp e)) (Mods C) -> BEval e t = BEval e t'.
intros. assert (x:=(l51 C s t)).
assert (y:=lookupsSameEvalSameB s t e).
rewrite <- y. Focus 2. intros. apply x. auto. simpl in H2.
assert (z:=intersectionNullNotIn v (BFv e) (Mods C)).
assert (~ In v (Mods C)). apply z. assumption. assumption.
apply inSkalVarInFalse in H4. symmetry in H4. rewrite <- skalVarInIn.
unfold not. intros. rewrite <- H4 in H5. inv H5. assumption.
clear x. clear y. assert (x:=(l51 C s' t')).
assert (y:=lookupsSameEvalSameB s' t' e).
rewrite <- y. Focus 2. intros. apply x. auto. simpl in H2.
assert (z:=intersectionNullNotIn v (BFv e) (Mods C)).
assert (~ In v (Mods C)). apply z. assumption. assumption.
apply inSkalVarInFalse in H4. symmetry in H4. rewrite <- skalVarInIn.
unfold not. intros. rewrite <- H4 in H5. inv H5. assumption.
assumption.
Qed.

Lemma opsemSameEvalSameH: forall e t t' s s' C, Opsem s C t -> Opsem s' C t' ->
HEval e s = HEval e s' ->
IntersectionNullP (fv (HExp e)) (Mods C) -> HEval e t = HEval e t'.
Proof.
intros. assert (x:=(l51 C s t)).
assert (y:=lookupsSameEvalSameH s t e).
rewrite <- y. Focus 2. intros. apply x. auto. simpl in H2.
assert (z:=intersectionNullNotIn v (HFv e) (Mods C)).
assert (~ In v (Mods C)). apply z. assumption. assumption.
apply inSkalVarInFalse in H4. symmetry in H4. rewrite <- skalVarInIn.
unfold not. intros. rewrite <- H4 in H5. inv H5. assumption.
clear x. clear y. assert (x:=(l51 C s' t')).
assert (y:=lookupsSameEvalSameH s' t' e).
rewrite <- y. Focus 2. intros. apply x. auto. simpl in H2.
assert (z:=intersectionNullNotIn v (HFv e) (Mods C)).
assert (~ In v (Mods C)). apply z. assumption. assumption.
apply inSkalVarInFalse in H4. symmetry in H4. rewrite <- skalVarInIn.
unfold not. intros. rewrite <- H4 in H5. inv H5. assumption.
assumption.
Qed.

Lemma app_nil_and : forall {A} a (b: list A), a++b = [] <-> a=[] /\ b = [] .
Proof.
intros. split; intros. destruct a; destruct b; auto; inv H.
destruct H. destruct a; inv H0. auto. inv H.
Qed.

Lemma opsemSameEvalSame: forall e t t' s s' C, Opsem s C t -> Opsem s' C t' ->
Eval e s = Eval e s' ->
IntersectionNullP (fv (e)) (Mods C) -> Eval e t = Eval e t'.
intros. destruct e. simpl. simpl in H1. erewrite opsemSameEvalSameA; try (eassumption).
auto. destruct (AEval a s). destruct (AEval a s'); inv H1. auto. destruct (AEval a s'); inv H1.
auto.
simpl in *. erewrite opsemSameEvalSameB; try (eassumption).
auto. destruct (BEval b s). destruct (BEval b s'); inv H1. auto. destruct (BEval b s'); inv H1.
auto.
simpl in *. erewrite opsemSameEvalSameH; try (eassumption). auto.
destruct (HEval h s); destruct (HEval h s'); inv H1; auto.
Qed.

Lemma in_trans: forall v phi x Theta, In v (BFv phi) -> In (phi, x) Theta ->
In v (TwoAssnsFv Theta).
intros. induction Theta. simpl in H0. inv H0.
destruct a. simpl. simpl in H0.
destruct H0. apply in_or_app. left. inv H0. apply in_or_app. left. assumption.
apply in_or_app. right. apply IHTheta. auto.
Qed.

Lemma notModEvalSameA: forall E s s' , AFv E = [] -> AEval E s = AEval E s'.
Proof.
intros.

induction E using AExpr_ind_mut with
(P:= (fun h => HFv h = [] -> HEval h s = HEval h s')); intros; inv H; auto.
simpl. repeat rewrite app_nil_and in H1. intuition.
rewrite H0. rewrite H3. rewrite H4. auto.

apply app_nil_and in H1. intuition. simpl. rewrite H1. rewrite H2. auto.
apply app_nil_and in H1. intuition. simpl. rewrite H1. rewrite H2. auto.
Qed.

Lemma notModEvalSameH: forall E s s' , HFv E = [] -> HEval E s = HEval E s'.
Proof.
intros. induction E; inv H; auto.
simpl. repeat rewrite app_nil_and in H1. intuition.
rewrite H0. rewrite (notModEvalSameA a s s'). rewrite (notModEvalSameA a0 s s').
auto. auto. auto.
Qed.

Lemma notModEvalSameB: forall B s s' , BFv B = [] -> BEval B s = BEval B s'.
Proof.
intros. induction B; inv H; auto.
apply app_nil_and in H1. destruct H1. simpl. rewrite (notModEvalSameA a s s'); auto.
rewrite (notModEvalSameA a0 s s'); auto.
apply app_nil_and in H1. intuition. simpl. rewrite H1. rewrite H2. auto.
apply app_nil_and in H1. intuition. simpl. rewrite H1. rewrite H2. auto.
specialize (IHB H1). simpl. rewrite IHB. auto.

Qed.

Lemma notModEvalSame: forall E s s', fv E = [] -> Eval E s = Eval E s'.
intros. destruct E; simpl. erewrite notModEvalSameA; auto.
erewrite notModEvalSameB; auto.
erewrite notModEvalSameH; auto.
Qed.

Lemma inAntecs: forall b Theta, In b (antecs Theta) -> exists e, In (b,e) Theta.
Proof.
intros. generalize dependent b. induction Theta; intros. inv H. simpl in *.
destruct a. simpl in H. destruct H. subst. eauto.
specialize (IHTheta b H). destruct IHTheta. exists x. right. auto.
Qed.

Lemma foldOrTrueHelpExists: forall s b Theta, BEval (foldOrHelp b Theta) s = Some true ->
(BEval b s = Some true \/ exists phi,
                          (In (phi) Theta /\ BEval phi s = Some true)).
Proof.
intros. generalize dependent b. induction Theta; intros. simpl in H. auto.
simpl in H. remember (BEval b s). destruct o. remember ((BEval (foldOrHelp a Theta))s).
destruct o; inv H. destruct b0; destruct b1; auto. right. simpl. clear H1.
edestruct IHTheta. symmetry in Heqo0. apply Heqo0. exists a. split.
auto. auto. destruct H. exists x. intuition. inv H.
Qed.

Lemma foldOrTrueExists: forall s Theta, BEval (foldOr (antecs Theta)) s = Some true ->
exists phi, exists e, (In (phi, e) Theta /\ BEval phi s = Some true).
Proof.
intros.
induction Theta. inv H.
simpl in *. destruct a. simpl in *. apply foldOrTrueHelpExists in H.
destruct H. exists b. exists e. intuition.
destruct H. exists x. destruct H.
apply inAntecs in H. destruct H. exists x0. eauto.
Qed.