Library evalCompletion

Require Import evidence.

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 splitAllVarsIn: forall a b X, allVarsIn (a ++ b) X =true -> allVarsIn a X =true
/\ allVarsIn b X =true.
intros. split. induction a. auto. simpl. simpl in H. remember (skalVarIn a X).
destruct b0. apply IHa. apply H. inv H.
induction a. auto. simpl. simpl in H. apply IHa. remember (skalVarIn a X). destruct b0. apply H. inv H.
Qed.

Theorem allVarsInSplit:forall a b X, allVarsIn a X =true -> allVarsIn b X =true ->
 allVarsIn (a ++ b) X =true.
intros. induction a. simpl. apply H0. simpl in *. remember (skalVarIn a X). destruct b0.
apply IHa. apply H. inversion H.
Qed.

Theorem skalVarInIn: forall x X, skalVarIn x X =true <-> In x X.
split. intros. induction X. inv H.
simpl in *. remember (beq_SkalVar x a). destruct b. symmetry in Heqb. apply beq_SkalVar_eq in Heqb.
subst. left. auto.

right. apply IHX. apply H.

intros. induction X. inv H. simpl in *. destruct H. subst. rewrite beq_SkalVar_refl.
auto. destruct (beq_SkalVar x a). auto. apply IHX. auto.
Qed.

Theorem varInEither: forall X Y a, allVarsIn X (a::Y)=true <-> (forall b, In b X -> b=a \/ In b Y).
Proof.
split.
intros. induction X. inv H0. simpl in H0. destruct H0. subst. simpl in *.
remember (beq_SkalVar b a). destruct b0. symmetry in Heqb0. apply beq_SkalVar_eq in Heqb0.
subst. left. auto.
remember (skalVarIn b Y). destruct b0. right. apply skalVarInIn. auto. inv H.
simpl in *. remember (beq_SkalVar a0 a). destruct b0. destruct IHX; try assumption.
auto. auto. apply IHX. remember (skalVarIn a0 Y). destruct b0. auto.
inv H. auto.

intros. induction X. auto.
simpl in *. edestruct H. auto. subst. rewrite beq_SkalVar_refl. apply IHX. intros.
apply H. right. auto.
remember (beq_SkalVar a0 a). destruct b. apply IHX. intros. apply H. auto.
rewrite <- skalVarInIn in H0. rewrite H0. apply IHX. intros. apply H. auto.
Qed.

Theorem allVarsInRefl: forall X, allVarsIn X X = true.
intros.
induction X. simpl. auto. simpl. rewrite beq_SkalVar_refl. destruct (varInEither X X a).
apply H0. intros. right. auto.
Qed.

Theorem allVarsInOr: forall X Y Z, allVarsIn X Z=true \/ allVarsIn X Y=true
-> allVarsIn X (Y++Z)=true.
intros X. induction X; intros. auto. destruct H. simpl. remember (skalVarIn a (Y++Z)).
destruct b. apply IHX. simpl in H. destruct (skalVarIn a Z). auto. inv H.
simpl in *. remember (skalVarIn a Z). destruct b. assert (skalVarIn a (Y++Z)=true).
apply skalVarInIn. apply in_or_app. symmetry in Heqb0. rewrite skalVarInIn in Heqb0. auto.
rewrite <- Heqb in H0. inv H0. inv H.

simpl. remember (skalVarIn a (Y++Z)).
destruct b. apply IHX. simpl in H. destruct (skalVarIn a Y). auto. inv H.
simpl in *. remember (skalVarIn a Y). destruct b. assert (skalVarIn a (Y++Z)=true).
apply skalVarInIn. apply in_or_app. symmetry in Heqb0. rewrite skalVarInIn in Heqb0. auto.
rewrite <- Heqb in H0. inv H0. inv H.
Qed.

Lemma inAllVarsInTrans: forall x X Y, In x X -> allVarsIn X Y =true -> In x Y.
intros x X. induction X; intros. inv H. simpl in H. destruct H. simpl in H0. remember (skalVarIn a Y).
destruct b. subst. symmetry in Heqb. rewrite skalVarInIn in Heqb. auto. inv H0. simpl in H0.
remember (skalVarIn a Y). destruct b. apply IHX. auto. auto. inv H0.
Qed.

Theorem allVarsInSkalVarIn: forall Y Z a, true=skalVarIn a Y -> allVarsIn Y Z = true ->
true = skalVarIn a Z.
intros Y. induction Y. intros. inv H.
intros. simpl in *. remember (beq_SkalVar a0 a). remember (skalVarIn a Z).
destruct b. destruct b0. symmetry in Heqb. apply beq_SkalVar_eq in Heqb. subst.
auto. inv H0. apply IHY. auto. destruct b0. auto. inv H0.
Qed.

Theorem allVarsInTrans: forall X Y Z, allVarsIn X Y =true -> allVarsIn Y Z = true ->
allVarsIn X Z = true.
Proof.
intros X. induction X. intros. auto.
intros. simpl in *. remember (skalVarIn a Z). remember (skalVarIn a Y). destruct b0. destruct b.
eapply IHX. eauto. auto. assert (true=skalVarIn a Z). eapply allVarsInSkalVarIn.
eauto. auto. rewrite <- Heqb in H1. inv H1.
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. destruct 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.