Library oiSoundness

Require Import soundness.
Require Import eqSoundness.
Require Import evalCompletion.

Theorem OISound : OISoundness.
unfold OISoundness.
intros. induction H.

apply EQSound in H. specialize (H s). simpl in H. remember (BEval b1 s). intuition. destruct o;
remember (BEval b2 s); destruct o. inv H2. auto. inv Heqo0. inv H2. inv H2. inv H1.

inv H1.

auto.

intuition.

edestruct BevalCompletes. apply splitAllVarsIn in H. destruct H. apply H3. apply H0. simpl in H3.
remember (BEval b2 s). destruct o. rewrite Heqo.

generalize dependent b. generalize dependent x.
induction b2; intros.

simpl in H2. remember (BSynEq b1 (BvarExpr b)). destruct b2. apply bSynEq_eq in Heqb2. subst.
auto. inv H2.

simpl in H2. remember (BSynEq b1 (BvalExpr b)). destruct b2. apply bSynEq_eq in Heqb2. subst.
auto. inv H2.

simpl in H2. remember (BSynEq b1 (BopExpr a b a0)). destruct b2. apply bSynEq_eq in Heqb2. subst.
auto. inv H2.

simpl in H2. remember (BSynEq b1 (b2_1 b&& b2_2)). destruct b0. apply bSynEq_eq in Heqb0. subst.
auto. inv H2.

simpl in H2. remember (BSynEq b1 (b2_1 b|| b2_2)). destruct b0. apply bSynEq_eq in Heqb0. subst.
auto.

simpl in H. apply splitAllVarsIn in H. destruct H.
apply splitAllVarsIn in H4. destruct H4.
simpl in Heqo.
remember (BEval b2_1 s). destruct o; remember (BEval b2_2 s); destruct o; inv Heqo.
apply orb_true_iff in H2. destruct H2.

simpl.

assert (Some b0 =Some true). eapply IHb2_1; auto.
apply allVarsInSplit; auto. inv H6. simpl in H3. inv H3. rewrite <- Heqo0.
rewrite <- Heqo1. auto.

assert (Some b2 = Some true). eapply IHb2_2; auto.
apply allVarsInSplit; auto. inv H6. simpl. rewrite <- Heqo0.
rewrite <- Heqo1. destruct b0; auto.

simpl in H2. remember (BSynEq b1 (!b2)). destruct b0. apply bSynEq_eq in Heqb0. subst.
auto. inv H2. inv H3.

Admitted.