Library twoISoundnessProof

Require Import soundness.
Require Import evidence.
Require Import soundnessLemmas.
Require Import oiSoundness.
Require Import evalCompletion.
Require Import eqSoundness.

Lemma tAssnSubtract: forall s s' Theta Theta2, twoAssnsInterpretation s s' (subtractAssns Theta Theta2) ->
twoAssnsInterpretation s s' Theta2 -> twoAssnsInterpretation s s' Theta.
intros.
induction Theta. auto. simpl. split. clear IHTheta. simpl in H. destruct a. constructor.
intros. remember (contains Theta2 (b, e)). destruct b0.
eapply containsInterp in H0. Focus 2. apply Heqb0. simpl in H0. inv H0. inv H3.
apply H5; auto. simpl in H. destruct H. inv H. apply H5; auto. apply IHTheta.
simpl in H. destruct (contains Theta2 a). auto. simpl in H. destruct H. auto.
Qed.

Theorem subtractAssnsNilSame: forall Theta, subtractAssns Theta [] = Theta.
intros.
induction Theta. auto. simpl. rewrite IHTheta. auto.
Qed.

Lemma containsIn: forall x Theta, true=contains Theta x -> In x Theta.
intros. induction Theta. simpl in H. inv H. simpl in H. remember (twoAssnEqual a x).
destruct b. apply twoAssnEqual_eq2 in Heqb. subst. simpl. left. auto.
simpl. right. apply IHTheta. apply H.
Qed.

Lemma inSubtract: forall x Theta Theta2, In x Theta -> ~In x Theta2 -> In x (subtractAssns Theta Theta2).
intros. induction Theta. simpl in H. inv H.
simpl in H. destruct H. subst. simpl. remember (contains Theta2 x). destruct b. destruct H0. apply containsIn in Heqb.
auto.
simpl. left. auto.
simpl. remember (contains Theta2 a). destruct b. apply IHTheta. apply H.
simpl. right. apply IHTheta. apply H.
Qed.

Axiom assnEq_dec: forall (a: TwoAssn) b, {a=b} + {a<>b}.

Lemma superSetallIn : forall Theta1 Theta2, superSet Theta1 Theta2 =true ->
(forall t, In t Theta2 -> In t Theta1).
Proof.
intros. induction Theta2. inv H0. simpl in H. simpl in H0. destruct H0.
subst. remember (contains Theta1 t). destruct b. Focus 2. inv H. Focus 2.
remember (contains Theta1 a). destruct b. Focus 2. inv H. Focus 2.
apply IHTheta2. auto. auto. apply containsIn in Heqb. assumption.
Qed.

Lemma vacuousAllFalse : forall Theta s, vacuous Theta = true -> (forall b e, In (b,e) Theta ->
BEval b s = Some false).
intros. induction Theta. inv H0.
simpl in H. destruct a. destruct b0; inv H.
destruct b0. inv H2. simpl in H0. destruct H0. inv H. simpl. auto.
apply IHTheta. assumption. assumption.
Qed.

Theorem twoISoundnessProof: twoISoundness.
unfold twoISoundness.
intros Theta Theta' X s s' Evidence EvalExists. induction Evidence.
split.
unfold twoAImp. intros.

inv H0. simpl. intuition. constructor. intros. inv H1.
apply OISound in iota.
apply H5.
apply iota. intros. destruct EvalExists with (x:=x).
apply inAllVarsInTrans with (X:=(BFv phi ++ BFv phi')). auto. auto. auto.
assumption.
apply iota. intros. destruct EvalExists with (x:=x).
apply inAllVarsInTrans with (X:=(BFv phi ++ BFv phi')). auto. auto. auto.
assumption.

unfold twoIBack. intros. inv H0; inv H1. eexists. eexists.
split. simpl. left. auto. inv H0. rewrite H3.
apply OISound in iota. apply iota.
intros. destruct EvalExists with (x:=x).
apply inAllVarsInTrans with (X:=(BFv phi'0 ++ BFv phi')). eauto. auto. auto.
assumption. inv H0.

subst. split. constructor. inv H. constructor. intros. inv H0. inv H1. inv H0. intuition.
inv H4. inv H0.
simpl in *. destruct (AEval e1 s). destruct (AEval e2 s).
destruct (AEval e1 s'). destruct (AEval e2 s'). inv H5. inv H4. auto.
inv H4. inv H5. destruct (AEval e2 s'). inv H4. destruct (AEval e1 s'). auto. auto.
destruct (AEval e1 s'). inv H5. auto. simpl. auto.

unfold twoIBack. intros. inv H0. inv H1. exists phi'. exists (AExp e1). split.
simpl. left. auto. assumption. inv H1.

split. constructor. inv H. constructor. intros. inv H0. intuition. simpl. simpl in H3.
destruct (BEval e1 s). destruct (BEval e1 s'). destruct b; destruct b0; auto.
inv H3.
destruct (BEval e1 s'). inv H3. auto. simpl. auto.

unfold twoIBack. intros. inv H0. inv H1. exists phi'. exists (BExp e1). split.
simpl. left. auto. assumption. inv H1.

split. constructor. inv H. constructor. intros. inv H0. inv H1. inv H0. intuition. simpl in *.
destruct (BEval e1 s); destruct (BEval e1 s'); destruct (BEval e2 s);
destruct (BEval e2 s'); auto; try (inv H4; inv H0; auto).
simpl; auto.

unfold twoIBack. intros. inv H0. inv H1. exists phi'. exists (BExp e1). split.
simpl. left. auto. assumption. inv H1.

split. constructor. inv H. constructor. intros. inv H0. inv H1. inv H0. intuition. simpl in *.
destruct (BEval e1 s); destruct (BEval e1 s'); destruct (BEval e2 s);
destruct (BEval e2 s'); auto; try (inv H4; inv H0; auto).
simpl; auto.

unfold twoIBack. intros. inv H0. inv H1. exists phi'. exists (BExp e1). split.
simpl. left. auto. assumption. inv H1.

split. constructor. inv H. constructor. intros. inv H0. inv H1. inv H0. intuition. simpl in *.
destruct (AEval e1 s); destruct (AEval e1 s'); destruct (AEval e2 s);
destruct (AEval e2 s'); auto; try (inv H4; inv H0; auto).
simpl; auto.

unfold twoIBack. intros. inv H0. inv H1. exists phi'. exists (AExp e1). split.
simpl. left. auto. assumption. inv H1.

destruct IHEvidence1. destruct IHEvidence2. subst.

split.
unfold twoAImp. intros. apply tAssnInterpApp in H. destruct H.
unfold twoAImp in H0. unfold twoAImp in H2. apply H2.
apply H0 in H4. eapply tAssnSubtract in H4. Focus 2. apply H.
auto.

unfold twoIBack in *. intros. edestruct H3.
apply H. apply H4. destruct H5. destruct H5.
destruct (in_dec assnEq_dec (x, x0) Theta1').
assert (exists phi : BExpr,
       exists e : Expr, In (phi, e) Theta1 /\ BEval phi s = Some true).
eapply H1. Focus 3.
repeat (destruct H7).
eexists. eexists. split. Focus 2. apply H8. apply H6. apply i.
apply in_or_app. right. eauto.
exists x. exists x0. split. apply in_or_app. left. apply inSubtract; auto.
auto.

intuition.
unfold twoAImp. intros. unfold twoAImp in *.
apply tAssnInterpApp in H3. destruct H3.
apply tAssnAppInterp. apply H. apply H3.
apply H1. apply H4.

unfold twoIBack. intros. apply in_app_or in H4. destruct H4.
unfold twoIBack in H0.
edestruct H0. apply H3. apply H4. repeat (destruct H5).
exists x. exists x0. split. apply in_or_app. left. apply H5. auto.
unfold twoIBack in H2. edestruct H2. apply H3. apply H4. repeat (destruct H5).
exists x. exists x0. split. apply in_or_app. right. auto. auto.

split. unfold twoAImp. intros. induction Theta2. simpl. auto.
simpl in H. remember (contains Theta1 a). destruct b.
simpl. split. apply (containsInterp s s' Theta1 a Heqb) in H0.
simpl in H0. destruct H0. assumption. apply IHTheta2. apply H. inv H.

unfold twoIBack. intros. exists phi'. exists e'.
split.
assert (x:=superSetallIn Theta1 Theta2 H). apply x in H1. assumption. auto.

split.
unfold twoAImp. intros.
induction Theta. auto. simpl. split. destruct a. eapply vacuousAllFalse in H. Focus 2.
simpl. left. auto. constructor. intros. rewrite H in H1. inv H1.
simpl in H. destruct a. destruct b; inv H. destruct b. inv H2. apply IHTheta.
assumption.

unfold twoIBack. intros. eapply vacuousAllFalse in H. Focus 2. apply H1. rewrite H in H0.
inv H0.

split. unfold twoAImp. intros. simpl. intuition.

constructor. intros. apply notModEvalSame. auto.

unfold twoIBack. intros. simpl in H2. destruct H2; inv H2. apply OISound in H0.
specialize (H0 s). assert (BEval (foldOr (antecs Theta)) s = Some true).
apply H0. apply EvalExists. apply H1.
apply foldOrTrueExists in H0. destruct H0. destruct H0. exists x. exists x0. auto.
apply EvalExists. apply H1.

split. unfold twoAImp. intros. inv H0. constructor. inv H1. constructor.
intros. intuition. apply EQSound in H. rewrite H in H3. rewrite H in H3.
trivial. intros.

edestruct EvalExists; eauto. intros; edestruct EvalExists; eauto. auto.

unfold twoIBack. intros. simpl in H1. destruct H1. inv H1. exists phi'.
exists E. split; auto. simpl. left. auto. inv H1.
Qed.