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.
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.