Library evidenceGenerator

Require Export evidence.
Require Export soundness.
Require Export soundnessLemmas.

Fixpoint generatePrecondition (c:Command) (post:TwoAssns) (X: list SkalVar): (TwoAssns * list SkalVar) :=
  match c with
  | Skip => (post, TwoAssnsFv post ++X)
  | Seq c1 c2 => match (generatePrecondition c2 post X) with (p, X1) =>
                    (generatePrecondition c1 (p) X1) end
  | Assign (x) A => (TwoAssnsSubst post x A, (varsUsedIn c ++ TwoAssnsFv post ++ X))
  
  | Cond B c1 c2 => let (p2,x2) := generatePrecondition c2 post X in
                      let (p1,x1) := generatePrecondition c1 post x2 in
                      ((andIntoTheta p1 B) ++
                      (andIntoTheta p2 (NotExpr B)) ++
                      conBoolAgreement p1 p2 B, (BFv B ++ varsUsedIn c1 ++ varsUsedIn c2 ++ TwoAssnsFv post
                      ++TwoAssnsFv p1 ++ TwoAssnsFv p2)++x2)
  | Assert b => (andIntoTheta post b, (BFv b) ++ X ++ TwoAssnsFv post)
  | _ => ([], X)
end
.

Lemma generatePreconditionXIncreases: forall C X Y pre post, (pre, X) = generatePrecondition C post Y ->
allVarsIn Y X = true.
intros C.
induction C; intros. inv H. apply allVarsInOr. left. apply allVarsInRefl.
simpl in H. remember (generatePrecondition C2 post Y). destruct p.
assert (allVarsIn Y l = true). eapply IHC2. apply Heqp.
assert (allVarsIn l X = true). eapply IHC1. apply H.
eapply allVarsInTrans. apply H0. auto.
inv H. apply allVarsInOr. left. apply allVarsInOr. left. apply allVarsInRefl.
inv H. apply allVarsInOr. left. apply allVarsInOr. right. apply allVarsInRefl.
inv H. remember (generatePrecondition C2 post Y). destruct p.
remember (generatePrecondition C1 post l). destruct p. inv H1.
apply allVarsInOr. left. eapply IHC2. apply Heqp.

simpl in *. inv H. apply allVarsInRefl.
simpl in *. inv H. apply allVarsInRefl.

Qed.

Lemma generatePreconditionXcontainsPost : forall C X Y pre post, (pre, X) = generatePrecondition C post Y ->
allVarsIn (TwoAssnsFv post) X = true.
Proof.
intros C. induction C; intros. inv H. apply allVarsInOr. right. apply allVarsInRefl.
inv H. remember (generatePrecondition C2 post Y). destruct p. assert (allVarsIn (TwoAssnsFv post) l=true).
eapply IHC2. apply Heqp. assert (allVarsIn (TwoAssnsFv t) X = true). eapply IHC1. eauto.
apply generatePreconditionXIncreases in H1. eapply allVarsInTrans in H1. apply H1. auto.
inv H. apply allVarsInOr. left. apply allVarsInOr. right. apply allVarsInRefl.

inv H. apply allVarsInOr. left. apply allVarsInOr. left. apply allVarsInRefl.

inv H. remember (generatePrecondition C2 post Y). destruct p. remember (generatePrecondition C1 post l).
destruct p. inv H1. apply allVarsInOr. right. apply allVarsInOr. left. apply allVarsInOr. left. apply allVarsInOr.
left. apply allVarsInOr. right. apply allVarsInRefl.

Admitted.
Lemma generatePreconditionVarsInC: forall C pre X Y post, (pre, X) = generatePrecondition C post Y ->
allVarsIn (varsUsedIn C) X = true.
Proof.
intros C. induction C; intros. auto.
simpl. inv H. remember (generatePrecondition C2 post Y). destruct p. apply allVarsInSplit.
eapply IHC1. eauto. assert (H2:=generatePreconditionXIncreases _ _ _ _ _ Heqp).
assert (H3:=generatePreconditionXIncreases _ _ _ _ _ H1).
assert ((allVarsIn (varsUsedIn C2) l) = true). eapply IHC2. apply Heqp.
eapply allVarsInTrans. apply H. apply H3. inv H. simpl. apply allVarsInOr. right. apply allVarsInRefl.
simpl in H. inv H. simpl. apply allVarsInOr. right. apply allVarsInRefl.
inv H. remember (generatePrecondition C2 post Y). destruct p. remember (generatePrecondition C1 post l).
destruct p. inv H1. simpl. apply allVarsInSplit. apply allVarsInOr. right. apply allVarsInOr. right.
apply allVarsInRefl. apply allVarsInSplit. apply allVarsInOr. right. apply allVarsInOr. left.
apply allVarsInOr. right. apply allVarsInRefl.
apply allVarsInOr. right. apply allVarsInOr. left.
apply allVarsInOr. left. apply allVarsInOr. right. apply allVarsInRefl.

Admitted.

Lemma generatePreconditionXIncreasesS: forall C X Y Z pre post, allVarsIn Z Y =true->
(pre,Z) = generatePrecondition C post X -> allVarsIn X Y=true.
intros C. induction C; intros. inv H0. apply splitAllVarsIn in H. destruct H.
auto.

inv H0. remember (generatePrecondition C2 post X). destruct p. eapply IHC2. Focus 2.
apply Heqp. eapply IHC1. apply H. apply H2.

inv H0. apply splitAllVarsIn in H. destruct H. apply splitAllVarsIn in H0.
destruct H0. auto.

inv H0. apply splitAllVarsIn in H. destruct H. apply splitAllVarsIn in H0. destruct H0. auto.
inv H0. remember (generatePrecondition C2 post X). destruct p.
remember (generatePrecondition C1 post l). destruct p. inv H2.
repeat (apply splitAllVarsIn in H; destruct H). apply splitAllVarsIn in H1.
destruct H1. apply splitAllVarsIn in H2. destruct H2. apply splitAllVarsIn in H3.
destruct H3.
eapply IHC2. Focus 2. eauto. auto.
Admitted.

Lemma allVarsInASubstA: forall e a x X, allVarsIn (AFv e) X = true -> allVarsIn (AFv a) X = true ->
allVarsIn (AFv (ASubstA e a x)) X = true.
Proof.
intros.
induction e using AExpr_ind_mut with
(P:= fun H =>allVarsIn (HFv H) X = true -> allVarsIn (HFv (HSubstA H a x)) X = true); auto.
simpl in *. apply splitAllVarsIn in H. destruct H. apply splitAllVarsIn in H1. destruct H1.
repeat apply allVarsInSplit; auto. simpl in *. remember (beq_SkalVar x (ASkalVar a0)).
destruct b. auto. auto. simpl. auto. simpl in H. apply splitAllVarsIn in H. destruct H.
simpl. apply allVarsInSplit. apply IHe1. auto. apply IHe2. auto.
simpl in *. apply splitAllVarsIn in H. destruct H. apply allVarsInSplit; auto.
Qed.

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

Lemma allVarsInASubstH: forall e a x X, allVarsIn (AFv e) X = true -> allVarsIn (HFv a) X = true ->
allVarsIn (AFv (ASubstH e a x)) X = true.
intros.
induction e using AExpr_ind_mut with
(P:= fun H =>allVarsIn (HFv H) X = true -> allVarsIn (HFv (HSubstH H a x)) X = true); auto.
simpl in *. remember (beq_SkalVar x (HSkalVar h)). destruct b; auto.
simpl in *. apply splitAllVarsIn in H. destruct H. apply splitAllVarsIn in H1. destruct H1.
repeat apply allVarsInSplit; auto.
simpl in *. apply splitAllVarsIn in H. destruct H. repeat apply allVarsInSplit; auto.
simpl in *. apply splitAllVarsIn in H. destruct H. repeat apply allVarsInSplit; auto.
Qed.

Lemma allVarsInHSubstH : forall e a x X, allVarsIn (HFv e) X = true -> allVarsIn (HFv a) X = true ->
allVarsIn (HFv (HSubstH e a x)) X = true.
intros. induction e; auto; simpl in *. destruct(beq_SkalVar x (HSkalVar h)); auto.
apply splitAllVarsIn in H. destruct H. apply splitAllVarsIn in H1. destruct H1.
repeat apply allVarsInSplit; auto; apply allVarsInASubstH; auto.
Qed.

Lemma allVarsInBSubstA: forall e a x X, allVarsIn (BFv e) X = true -> allVarsIn (AFv a) X = true ->
allVarsIn (BFv (BSubstA e a x)) X = true.
intros. induction e. simpl. simpl in H. remember (skalVarIn (BSkalVar b) X). destruct b0. auto. inv H.
simpl. auto.
simpl in *. apply splitAllVarsIn in H. destruct H. apply allVarsInSplit . apply allVarsInASubstA; auto.
apply allVarsInASubstA; auto.
simpl in *. apply splitAllVarsIn in H. destruct H. apply allVarsInSplit. apply IHe1. auto. apply IHe2. auto.
simpl in *. apply splitAllVarsIn in H. destruct H. apply allVarsInSplit. apply IHe1. auto. apply IHe2. auto.
simpl in *. apply IHe. auto.
Qed.

Lemma allVarsInBSubstB: forall e a x X, allVarsIn (BFv e) X = true -> allVarsIn (BFv a) X = true ->
allVarsIn (BFv (BSubstB e a x)) X = true.
Proof. intros. induction e. simpl in *.
remember (beq_SkalVar x (BSkalVar b)). destruct b0. symmetry in Heqb0. apply beq_SkalVar_eq in Heqb0.
subst. auto. simpl. remember (skalVarIn (BSkalVar b) X). destruct b0. auto. inv H.
simpl. auto. simpl in *. auto.
simpl in *. apply splitAllVarsIn in H. destruct H. apply allVarsInSplit. apply IHe1. auto. apply IHe2. auto.
simpl in *. apply splitAllVarsIn in H. destruct H. apply allVarsInSplit. apply IHe1. auto. apply IHe2. auto.
simpl in *. apply IHe. auto.
Qed.

Lemma allVarsInBSubstH: forall e a x X, allVarsIn (BFv e) X = true -> allVarsIn (HFv a) X = true ->
allVarsIn (BFv (BSubstH e a x)) X = true.
intros. induction e; auto.
simpl in *. apply splitAllVarsIn in H. destruct H. apply allVarsInSplit . apply allVarsInASubstH; auto.
apply allVarsInASubstH; auto.
simpl in *. apply splitAllVarsIn in H. destruct H. apply allVarsInSplit. apply IHe1. auto. apply IHe2. auto.
simpl in *. apply splitAllVarsIn in H. destruct H. apply allVarsInSplit. apply IHe1. auto. apply IHe2. auto.
Qed.

Lemma twoAssnsSubstAStillAllIn: forall post s a Y,
allVarsIn (TwoAssnsFv post) Y =true ->
allVarsIn (AFv a) Y =true ->
allVarsIn (TwoAssnsFv (TwoAssnsSubstA post s a)) Y = true.
Proof.
intros. induction post. simpl. auto.
simpl. remember (TwoAssnSubstA a0 s a). destruct t. apply allVarsInSplit. destruct a0. inv Heqt.
apply allVarsInSplit. simpl in H. apply splitAllVarsIn in H. destruct H.
apply splitAllVarsIn in H. destruct H. apply allVarsInBSubstA; auto.
simpl in H. apply splitAllVarsIn in H. destruct H. apply splitAllVarsIn in H.
destruct H. destruct e0; simpl. apply allVarsInASubstA; auto. apply allVarsInBSubstA; auto.
apply allVarsInHSubstA; auto.
apply IHpost. simpl in H. destruct a0. apply splitAllVarsIn in H. destruct H.
apply splitAllVarsIn in H. destruct H. auto.
Qed.

Lemma twoAssnsSubstBStillAllIn: forall post s a Y,
allVarsIn (TwoAssnsFv post) Y =true ->
allVarsIn (BFv a) Y =true ->
allVarsIn (TwoAssnsFv (TwoAssnsSubstB post s a)) Y = true.
Proof.
intros. induction post. simpl. auto.
simpl. remember (TwoAssnSubstB a0 s a). destruct t. apply allVarsInSplit. destruct a0. inv Heqt.
apply allVarsInSplit. simpl in H. apply splitAllVarsIn in H. destruct H.
apply splitAllVarsIn in H. destruct H. apply allVarsInBSubstB; auto.
simpl in H. apply splitAllVarsIn in H. destruct H. apply splitAllVarsIn in H.
destruct H. destruct e0; simpl. auto. apply allVarsInBSubstB; auto.
auto.
apply IHpost. simpl in H. destruct a0. apply splitAllVarsIn in H. destruct H.
apply splitAllVarsIn in H. destruct H. auto.
Qed.

Lemma twoAssnsSubstHStillAllIn: forall post s a Y,
allVarsIn (TwoAssnsFv post) Y =true ->
allVarsIn (HFv a) Y =true ->
allVarsIn (TwoAssnsFv (TwoAssnsSubstH post s a)) Y = true.
Proof.
intros. induction post; auto; simpl in *. destruct a0.
simpl in *. apply splitAllVarsIn in H. destruct H. apply splitAllVarsIn in H.
destruct H. repeat apply allVarsInSplit; auto. apply allVarsInBSubstH; auto.
destruct e; simpl; auto. apply allVarsInASubstH; auto. apply allVarsInBSubstH; auto.
apply allVarsInHSubstH; auto.
Qed.

Lemma twoAssnsSubstStillAllIn: forall post s a Y,
allVarsIn (TwoAssnsFv post) Y =true ->
allVarsIn (fv a) Y =true ->
allVarsIn (TwoAssnsFv (TwoAssnsSubst post s a)) Y = true.
Proof.
intros. destruct a. simpl. apply twoAssnsSubstAStillAllIn; auto.
apply twoAssnsSubstBStillAllIn; auto. simpl. apply twoAssnsSubstHStillAllIn; auto.
Qed.

Lemma generatePreconditionNotIntroduceVars: forall c post X Y Z pre, allVarsIn (varsUsedIn c) X=true ->
allVarsIn (TwoAssnsFv post) X =true -> allVarsIn Y X=true ->
(pre, Z) = (generatePrecondition c post Y) ->
allVarsIn (TwoAssnsFv pre) X = true /\ allVarsIn Z X = true.
Proof.
intros c.
induction c; intros; inv H2. intuition. apply allVarsInSplit; auto.
simpl in H. apply splitAllVarsIn in H. destruct H. simpl in H2. remember (generatePrecondition c2 post Y).
destruct p. edestruct (IHc1 t _ l _ pre). eauto. edestruct IHc2. eauto. eauto. Focus 2. eauto. auto.
auto. edestruct IHc2. eauto. eauto. eauto. eauto. auto. eauto. auto.
simpl in *. split. simpl. apply twoAssnsSubstStillAllIn. auto. auto.
repeat apply allVarsInSplit; auto.
split. apply andIntoThetaFV. auto. simpl in H. auto.
repeat apply allVarsInSplit; auto.

remember (generatePrecondition c2 post Y). destruct p.
remember (generatePrecondition c1 post l). destruct p. inv H4.
simpl in H. apply splitAllVarsIn in H. destruct H. apply splitAllVarsIn in H2.
destruct H2. edestruct (IHc1 post X l _ t0). eauto. auto.
edestruct (IHc2). eauto. eauto. eauto. eauto.
auto. eauto.
edestruct (IHc2 post X Y _ t); auto. apply Heqp.
split. repeat rewrite <- twoAssnsFvSplit. repeat apply allVarsInSplit; auto.
apply andIntoThetaFV. auto. auto. apply andIntoThetaFV; auto. apply conBoolAgreementFV; auto.
repeat apply allVarsInSplit; auto.

auto.

auto.

Qed.

Theorem generatePreconditionEvidence: forall C Y X Z post pre,
(pre, X) = generatePrecondition C post Z ->
allVarsIn X Y = true->
TEvid Y C (Assns pre post).
Proof.
intros C. induction C; intros. constructor.
inv H. auto. simpl in H. inv H. apply splitAllVarsIn in H0. destruct H0.
apply allVarsInSplit; auto.
simpl in H. remember (generatePrecondition C2 post Z).
destruct p.
assert (x:=generatePreconditionXIncreasesS C1 l Y X pre t H0 H).
assert (y:=generatePreconditionXIncreasesS C2 Z Y l t post x Heqp).
assert (z:=generatePreconditionVarsInC C2 t l Z post Heqp).
assert (w:=generatePreconditionVarsInC C1 pre X l t H).
assert (m:=allVarsInTrans _ _ _ w H0).
assert (n:=allVarsInTrans _ _ _ z x).
assert (o:=generatePreconditionXcontainsPost _ _ _ _ _ Heqp).
assert (p:=allVarsInTrans _ _ _ o x).
econstructor. eapply IHC2. eauto.
assert (H3:=generatePreconditionXIncreasesS C1 l Y X pre t H0 H). auto.
eapply IHC1. apply H. auto. repeat (apply allVarsInSplit). apply generatePreconditionVarsInC in H.
eapply allVarsInTrans in H0. apply H0. auto.
apply generatePreconditionVarsInC in Heqp. eapply generatePreconditionXIncreases in H.
eapply allVarsInTrans in H0. apply H0. eapply allVarsInTrans in H. apply H. auto.
eapply generatePreconditionNotIntroduceVars in Heqp. destruct Heqp. apply H1.
auto. auto. auto.

eapply generatePreconditionNotIntroduceVars in H. destruct H.
apply H. auto. auto.

eapply generatePreconditionNotIntroduceVars in Heqp. destruct Heqp. apply H1.
auto. auto. auto. auto. auto. auto.

simpl. destruct e. eapply TAAssignE. inv H. auto. simpl in H.
inv H. apply splitAllVarsIn in H0. destruct H0.
apply splitAllVarsIn in H0. destruct H0.
repeat (apply allVarsInSplit). auto. auto. apply twoAssnsSubstAStillAllIn; auto.
eapply TBAssignE. inv H. auto. simpl in H.
inv H. apply splitAllVarsIn in H0. destruct H0.
apply splitAllVarsIn in H0. destruct H0.
repeat (apply allVarsInSplit). auto. auto. apply twoAssnsSubstBStillAllIn; auto.

eapply THAssignE. inv H. auto. simpl in H.
inv H. apply splitAllVarsIn in H0. destruct H0.
apply splitAllVarsIn in H0. destruct H0.
repeat (apply allVarsInSplit). auto. auto. apply twoAssnsSubstHStillAllIn; auto.
inv H.
constructor. apply splitAllVarsIn in H0. destruct H0. apply splitAllVarsIn in H0.
destruct H0. apply allVarsInSplit; auto. auto.

inv H. remember (generatePrecondition C2 post Z). destruct p.
remember (generatePrecondition C1 post l). destruct p. inv H2.
apply splitAllVarsIn in H0. destruct H0. apply splitAllVarsIn in H. destruct H.
apply splitAllVarsIn in H1. destruct H1. apply splitAllVarsIn in H2.
destruct H2. apply splitAllVarsIn in H3. destruct H3. apply splitAllVarsIn in H4. destruct H4.
eapply TCondE. eapply IHC1. apply Heqp0. eapply generatePreconditionNotIntroduceVars in Heqp0.
destruct Heqp0. apply H7. apply H1. apply H3. apply H0.
eapply IHC2. apply Heqp. apply H0.
repeat apply allVarsInSplit; auto. repeat rewrite <- twoAssnsFvSplit. repeat apply allVarsInSplit; auto.
apply andIntoThetaFV; auto. apply andIntoThetaFV; auto. apply conBoolAgreementFV; auto.
simpl in H. inv H.
admit. admit. Qed.