Library forallTest

Require Import evidence.
Require Import substLemmas.
Require Import soundnessLemmas.

Definition x := AId 0.

Definition cmd := Assign (ASkalVar x) (AExp (AopExpr (SvarExpr x) aplus (IntExpr 1%Z))).
Definition w := AId 1.

Definition post := fun u => [(BopExpr u blt (IntExpr 3%Z), AExp (SvarExpr x))].
Definition c := Assign (ASkalVar x) (AExp(SvarExpr w)).
Definition pre := fun u => [(BopExpr u blt (IntExpr 3%Z), AExp (SvarExpr w))].

Definition fa : assns := Aforall (fun u =>
  Assns [(BopExpr u blt (IntExpr 3%Z), AExp (SvarExpr w))]
  [(BopExpr u blt (IntExpr 3%Z), AExp (SvarExpr x))]).

Definition X := [ASkalVar w, ASkalVar x].
Definition Y := [ASkalVar w, ASkalVar x].

Axiom NoFvNoSubst : forall {E} {A} {x}, IntersectionNullP (AFv E) [x] -> ASubstA E A x = E.

Definition evidFun := fun u=>

@TAAssignE X
[(BopExpr u blt (IntExpr 3%Z), AExp (SvarExpr x))] (ASkalVar x) (SvarExpr w)
[(BopExpr u blt (IntExpr 3%Z), AExp (SvarExpr w))].

Check evidFun.

Lemma blah: TEvid X c (fa).
Proof.
econstructor. intros.
apply evidFun. simpl. rewrite NoFvNoSubst. auto. auto.
simpl. repeat rewrite app_nil_r. repeat apply allVarsInSplit; auto.
Qed.

Print blah.

Lemma AAssignForall : forall Theta x A {Theta'},
              Theta'= (TwoAssnsSubstA Theta x A) ->
              allVarsIn (AFv A ++
              TwoAssnsFv Theta ++
              TwoAssnsFv Theta') X =true ->
              TEvid X TForall (Tforall Theta' (Assign x (AExp A)) Theta)

Print blah.