Library evidence
Require Export synEq.
Require Export twoAssn.
Require Export language.
Require Export synEq.
Require Export varLists.
Require Export twoAssn.
Require Export language.
Require Export synEq.
Require Export varLists.
Definition for triple
Aforall is for polymorphic triples
Inductive assns :=
| Assns : TwoAssns -> TwoAssns -> assns
| Aforall : (AExpr -> assns)-> assns.
| Assns : TwoAssns -> TwoAssns -> assns
| Aforall : (AExpr -> assns)-> assns.
Evidence for equality
Inductive EQEvid X : Expr -> Expr -> Prop :=
| ReflE : forall {e}, EQEvid X e e
| SymE : forall e1 e2, EQEvid X e1 e2 -> EQEvid X e2 e1
| SynEqE : forall e1 e2, allVarsIn ((fv e1) ++ (fv e2)) X = true
-> synEq e1 e2 = true -> EQEvid X e1 e2
| TransE : forall e1 e2 e3, allVarsIn (fv e1 ++ fv e2 ++ fv e3) X = true -> EQEvid X e1 e2 ->
EQEvid X e2 e3 -> EQEvid X e1 e3
| DecisionE : forall e1 e2, allVarsIn ((fv e1) ++ (fv e2)) X = true -> EQEvid X e1 e2.
| ReflE : forall {e}, EQEvid X e e
| SymE : forall e1 e2, EQEvid X e1 e2 -> EQEvid X e2 e1
| SynEqE : forall e1 e2, allVarsIn ((fv e1) ++ (fv e2)) X = true
-> synEq e1 e2 = true -> EQEvid X e1 e2
| TransE : forall e1 e2 e3, allVarsIn (fv e1 ++ fv e2 ++ fv e3) X = true -> EQEvid X e1 e2 ->
EQEvid X e2 e3 -> EQEvid X e1 e3
| DecisionE : forall e1 e2, allVarsIn ((fv e1) ++ (fv e2)) X = true -> EQEvid X e1 e2.
inDisjunction for rule below
Fixpoint inDisjunction b1 b2 : bool :=
if BSynEq b1 b2 then true else
match b2 with
| OrExpr b3 b4=> inDisjunction b1 b3 || inDisjunction b1 b4
| _ => false end.
if BSynEq b1 b2 then true else
match b2 with
| OrExpr b3 b4=> inDisjunction b1 b3 || inDisjunction b1 b4
| _ => false end.
Evidence for one implication
Inductive OIEvid X : BExpr -> BExpr -> Prop :=
| EQImpl : forall {b1 b2}, EQEvid X (BExp b1) (BExp b2) -> OIEvid X b1 b2
| FalseLeftImpl : forall b2, OIEvid X (BvalExpr false) b2
| TrueRightImpl : forall b1, OIEvid X b1 (BvalExpr true)
| TransImpl : forall b1 b2 b3,
OIEvid X b1 b2 -> OIEvid X b2 b3 -> OIEvid X b1 b3
| InDisjunctionImpl : forall b1 b2, allVarsIn ((BFv b1) ++ (BFv b2)) X = true -> inDisjunction b1 b2 = true -> OIEvid X b1 b2
| ContradictionImpl : forall b1,OIEvid X (AndExpr b1 (! b1)) (BvalExpr false)
| DecisionImpl : forall b1 b2,
OIEvid X b1 b2.
| EQImpl : forall {b1 b2}, EQEvid X (BExp b1) (BExp b2) -> OIEvid X b1 b2
| FalseLeftImpl : forall b2, OIEvid X (BvalExpr false) b2
| TrueRightImpl : forall b1, OIEvid X b1 (BvalExpr true)
| TransImpl : forall b1 b2 b3,
OIEvid X b1 b2 -> OIEvid X b2 b3 -> OIEvid X b1 b3
| InDisjunctionImpl : forall b1 b2, allVarsIn ((BFv b1) ++ (BFv b2)) X = true -> inDisjunction b1 b2 = true -> OIEvid X b1 b2
| ContradictionImpl : forall b1,OIEvid X (AndExpr b1 (! b1)) (BvalExpr false)
| DecisionImpl : forall b1 b2,
OIEvid X b1 b2.
foldOr for some two Implications
I use this rather than a simple fold so we
don't have to stick false in the end
Fixpoint foldOrHelp (b:BExpr) (l:list BExpr) :=
match l with
h::t => OrExpr b (foldOrHelp h t)
| [] => b
end.
Definition foldOr (l:list BExpr) :BExpr :=
match l with
h::t => foldOrHelp h t
| [] => BvalExpr false
end.
match l with
h::t => OrExpr b (foldOrHelp h t)
| [] => b
end.
Definition foldOr (l:list BExpr) :BExpr :=
match l with
h::t => foldOrHelp h t
| [] => BvalExpr false
end.
Evidence for two implications
Inductive TIEvid X : TwoAssns -> TwoAssns -> Prop :=
Contravar2I : forall {phi phi' }
(iota :OIEvid (BFv phi ++ BFv phi') phi phi') E,
allVarsIn (BFv phi ++ BFv phi') X = true ->
TIEvid X [(phi', E)] [(phi, E)]
| BinOp2Ibop : forall {E1 E2 e1 e2 op} phi, E1 = AExp e1 -> E2 = AExp e2 ->
TIEvid X [(phi, E1), (phi, E2)] [(phi, BExp (BopExpr e1 op e2))]
| BinOp2Inot : forall {e1} phi, TIEvid X [(phi, BExp e1)] [(phi, BExp (NotExpr e1))]
| BinOp2Ior : forall e1 e2 phi, TIEvid X [(phi, BExp e1), (phi, BExp e2)]
[(phi, BExp (OrExpr e1 e2))]
| BinOp2Iand : forall e1 e2 phi, TIEvid X [(phi, BExp e1), (phi, BExp e2)]
[(phi, BExp (AndExpr e1 e2))]
| BinOp2Iaop : forall {e1 e2 op} phi,
TIEvid X [(phi, AExp e1), (phi, AExp e2)] [(phi, AExp (AopExpr e1 op e2))]
| Trans2I : forall {Theta1 Theta1' Theta2 Theta Theta'}
(tau1 : TIEvid X Theta1 Theta1')
(tau2 : TIEvid X Theta2 Theta'),
Theta = (subtractAssns Theta2 Theta1') ++ Theta1 ->
TIEvid X Theta Theta'
| Union2I : forall {Theta1 Theta1' Theta2 Theta2'}
(tau1 : TIEvid X Theta1 Theta1')
(tau2 : TIEvid X Theta2 Theta2'),
TIEvid X (Theta1++Theta2) (Theta1'++Theta2')
| Superset2I : forall Theta1 Theta2,
superSet Theta1 Theta2 = true ->
TIEvid X Theta1 Theta2
| Vacusous2I : forall Theta,
vacuous Theta = true ->
TIEvid X [] Theta
| Const2I : forall E Theta phi,
fv E = [] ->
OIEvid X phi (foldOr (antecs Theta)) ->
TIEvid X Theta [(phi, E)]
| RhsEquiv2I : forall E E1 phi,
EQEvid X E E1 -> TIEvid X [(phi, E)] [(phi, E1)].
Contravar2I : forall {phi phi' }
(iota :OIEvid (BFv phi ++ BFv phi') phi phi') E,
allVarsIn (BFv phi ++ BFv phi') X = true ->
TIEvid X [(phi', E)] [(phi, E)]
| BinOp2Ibop : forall {E1 E2 e1 e2 op} phi, E1 = AExp e1 -> E2 = AExp e2 ->
TIEvid X [(phi, E1), (phi, E2)] [(phi, BExp (BopExpr e1 op e2))]
| BinOp2Inot : forall {e1} phi, TIEvid X [(phi, BExp e1)] [(phi, BExp (NotExpr e1))]
| BinOp2Ior : forall e1 e2 phi, TIEvid X [(phi, BExp e1), (phi, BExp e2)]
[(phi, BExp (OrExpr e1 e2))]
| BinOp2Iand : forall e1 e2 phi, TIEvid X [(phi, BExp e1), (phi, BExp e2)]
[(phi, BExp (AndExpr e1 e2))]
| BinOp2Iaop : forall {e1 e2 op} phi,
TIEvid X [(phi, AExp e1), (phi, AExp e2)] [(phi, AExp (AopExpr e1 op e2))]
| Trans2I : forall {Theta1 Theta1' Theta2 Theta Theta'}
(tau1 : TIEvid X Theta1 Theta1')
(tau2 : TIEvid X Theta2 Theta'),
Theta = (subtractAssns Theta2 Theta1') ++ Theta1 ->
TIEvid X Theta Theta'
| Union2I : forall {Theta1 Theta1' Theta2 Theta2'}
(tau1 : TIEvid X Theta1 Theta1')
(tau2 : TIEvid X Theta2 Theta2'),
TIEvid X (Theta1++Theta2) (Theta1'++Theta2')
| Superset2I : forall Theta1 Theta2,
superSet Theta1 Theta2 = true ->
TIEvid X Theta1 Theta2
| Vacusous2I : forall Theta,
vacuous Theta = true ->
TIEvid X [] Theta
| Const2I : forall E Theta phi,
fv E = [] ->
OIEvid X phi (foldOr (antecs Theta)) ->
TIEvid X Theta [(phi, E)]
| RhsEquiv2I : forall E E1 phi,
EQEvid X E E1 -> TIEvid X [(phi, E)] [(phi, E1)].
Evidence for necessary precondition
Inductive NPCEvid (X: list SkalVar) : BExpr -> Command -> BExpr -> Prop :=
SkipNPC : forall phi,
allVarsIn (BFv phi) X = true ->
NPCEvid X phi Skip phi
| AAssignNPC : forall phi x A,
allVarsIn (BFv phi ++ (AFv A)) X = true ->
NPCEvid X (BSubstA phi A x) (Assign x (AExp A)) phi
| BAssignNPC : forall phi x B,
allVarsIn (BFv phi ++ (BFv B)) X = true ->
NPCEvid X (BSubstB phi B x) (Assign x (BExp B)) phi
| HAssignNPC : forall phi x H,
allVarsIn (BFv phi ++ (HFv H)) X = true ->
NPCEvid X (BSubstH phi H x) (Assign x (HExp H)) phi
| AssertNPC : forall phi B,
allVarsIn (BFv phi ++ BFv B) X = true ->
NPCEvid X (AndExpr B phi) (Assert B) phi
| SeqNPC : forall {phi phi1 phi2 C1 C2}
(v1 : NPCEvid X phi1 C1 phi2)
(v2 : NPCEvid X phi2 C2 phi),
allVarsIn (varsUsedIn C1 ++ varsUsedIn C2 ++
BFv phi ++ BFv phi1 ++ BFv phi2) X = true ->
NPCEvid X phi1 (Seq C1 C2) phi
| CondNPC : forall {phi phi1 phi2 C1 C2} B
(v1 : NPCEvid X phi1 C1 phi)
(v2 : NPCEvid X phi2 C2 phi),
allVarsIn (varsUsedIn C1 ++ varsUsedIn C2 ++
BFv phi ++ BFv phi1 ++ BFv phi2) X = true ->
NPCEvid X ((phi1 b&& B) b|| (phi2 b&& !B)) (Cond B C1 C2) phi
| NotModNPC : forall C L phi,
allVarsIn (varsUsedIn C ++ BFv phi) X = true ->
Mods C = L ->
(IntersectionNullP L (BFv phi)) ->
NPCEvid X phi C phi
| WhileNPC : forall C phi B phi',
allVarsIn (varsUsedIn C ++ BFv phi ++ BFv phi' ++ BFv B) X = true ->
NPCEvid X phi C phi ->
(forall s, (BEval (AndExpr phi' (NotExpr B)) s) = Some true ->
BEval phi s = Some true) ->
NPCEvid X phi (While B C) phi'
.
Definition isSubstFunctionAB f := forall s u v,
AEval u s = Some v -> BEval (f u) s = BEval (f (IntExpr v)) s.
SkipNPC : forall phi,
allVarsIn (BFv phi) X = true ->
NPCEvid X phi Skip phi
| AAssignNPC : forall phi x A,
allVarsIn (BFv phi ++ (AFv A)) X = true ->
NPCEvid X (BSubstA phi A x) (Assign x (AExp A)) phi
| BAssignNPC : forall phi x B,
allVarsIn (BFv phi ++ (BFv B)) X = true ->
NPCEvid X (BSubstB phi B x) (Assign x (BExp B)) phi
| HAssignNPC : forall phi x H,
allVarsIn (BFv phi ++ (HFv H)) X = true ->
NPCEvid X (BSubstH phi H x) (Assign x (HExp H)) phi
| AssertNPC : forall phi B,
allVarsIn (BFv phi ++ BFv B) X = true ->
NPCEvid X (AndExpr B phi) (Assert B) phi
| SeqNPC : forall {phi phi1 phi2 C1 C2}
(v1 : NPCEvid X phi1 C1 phi2)
(v2 : NPCEvid X phi2 C2 phi),
allVarsIn (varsUsedIn C1 ++ varsUsedIn C2 ++
BFv phi ++ BFv phi1 ++ BFv phi2) X = true ->
NPCEvid X phi1 (Seq C1 C2) phi
| CondNPC : forall {phi phi1 phi2 C1 C2} B
(v1 : NPCEvid X phi1 C1 phi)
(v2 : NPCEvid X phi2 C2 phi),
allVarsIn (varsUsedIn C1 ++ varsUsedIn C2 ++
BFv phi ++ BFv phi1 ++ BFv phi2) X = true ->
NPCEvid X ((phi1 b&& B) b|| (phi2 b&& !B)) (Cond B C1 C2) phi
| NotModNPC : forall C L phi,
allVarsIn (varsUsedIn C ++ BFv phi) X = true ->
Mods C = L ->
(IntersectionNullP L (BFv phi)) ->
NPCEvid X phi C phi
| WhileNPC : forall C phi B phi',
allVarsIn (varsUsedIn C ++ BFv phi ++ BFv phi' ++ BFv B) X = true ->
NPCEvid X phi C phi ->
(forall s, (BEval (AndExpr phi' (NotExpr B)) s) = Some true ->
BEval phi s = Some true) ->
NPCEvid X phi (While B C) phi'
.
Definition isSubstFunctionAB f := forall s u v,
AEval u s = Some v -> BEval (f u) s = BEval (f (IntExpr v)) s.
Evidence for a precondition command and postcondition
Inductive TEvid (X: list SkalVar) : Command -> assns -> Prop :=
TSkipE : forall {Theta'} Theta, Theta'=Theta ->
allVarsIn (TwoAssnsFv Theta ++
TwoAssnsFv Theta') X =true ->
TEvid X Skip (Assns Theta' Theta)
| TAAssignE : forall Theta x A {Theta'}, Theta'= (TwoAssnsSubstA Theta x A) ->
allVarsIn (AFv A ++
TwoAssnsFv Theta ++
TwoAssnsFv Theta') X =true ->
TEvid X (Assign x (AExp A)) (Assns Theta' Theta)
| TBAssignE : forall Theta x B {Theta'}, Theta'= (TwoAssnsSubstB Theta x B) ->
allVarsIn (BFv B ++
TwoAssnsFv Theta ++
TwoAssnsFv Theta') X =true ->
TEvid X (Assign x (BExp B)) (Assns Theta' Theta)
| THAssignE : forall Theta x H {Theta'}, Theta'= (TwoAssnsSubstH Theta x H) ->
allVarsIn (HFv H ++
TwoAssnsFv Theta ++
TwoAssnsFv Theta') X =true ->
TEvid X (Assign x (HExp H)) (Assns Theta' Theta)
| TSeqE: forall {Theta1 Theta Theta2 Theta' C1 C2}
(eta2: TEvid X C2 (Assns Theta' Theta2))
(eta1: TEvid X C1 (Assns Theta1 Theta)),
allVarsIn ((varsUsedIn C1) ++ (varsUsedIn C2) ++
TwoAssnsFv Theta ++
TwoAssnsFv Theta1 ++
TwoAssnsFv Theta2) X =true ->
Theta=Theta' -> TEvid X (Seq C1 C2) (Assns Theta1 Theta2)
| TCondE: forall {Theta1 Theta Theta2 Theta' C1 C2}
(eta1: TEvid X C1 (Assns Theta1 Theta))
(eta2: TEvid X C2 (Assns Theta2 Theta)) B,
((andIntoTheta Theta1 B) ++
andIntoTheta Theta2 (NotExpr B) ++
conBoolAgreement Theta1 Theta2 B) = Theta' ->
allVarsIn ((varsUsedIn C1) ++ (varsUsedIn C2) ++ (BFv B) ++
TwoAssnsFv Theta ++
TwoAssnsFv Theta1 ++
TwoAssnsFv Theta2 ++
TwoAssnsFv Theta') X =true ->
TEvid X (Cond B C1 C2) (Assns Theta' Theta)
| TPreImplyE : forall {Theta Theta1 Theta2 Theta2' C}
(eta : TEvid X C (Assns Theta2' Theta1))
(tau : TIEvid X Theta Theta2),
allVarsIn ((varsUsedIn C) ++
TwoAssnsFv Theta ++
TwoAssnsFv Theta1 ++
TwoAssnsFv Theta2 ++
TwoAssnsFv Theta2') X =true ->
Theta2 = Theta2' -> TEvid X C (Assns Theta Theta1)
| TPostImplyE : forall {Theta Theta1 Theta2 Theta2' C}
(eta: TEvid X C (Assns Theta Theta2'))
(tau: TIEvid X Theta2 Theta1),
allVarsIn ((varsUsedIn C) ++
TwoAssnsFv Theta ++
TwoAssnsFv Theta1 ++
TwoAssnsFv Theta2 ++
TwoAssnsFv Theta2') X =true ->
Theta2' = Theta2 -> TEvid X C (Assns Theta Theta1)
| TNotModE : forall {C L}
(mu : (Mods C) = L) Theta,
allVarsIn ((varsUsedIn C) ++
TwoAssnsFv Theta) X =true ->
(IntersectionNullP L (TwoAssnsFv Theta)) ->
TEvid X C (Assns Theta Theta)
| ConseqNotModE : forall phi phi' E C L,
Mods C = L ->
NPCEvid X phi C phi' ->
(IntersectionNullP L (fv E)) ->
TEvid X C (Assns [(phi, E)] [(phi', E)])
| TAssertE : forall Theta Theta' B, allVarsIn (BFv B ++ TwoAssnsFv Theta) X= true ->
Theta'= andIntoTheta Theta B ->
TEvid X (Assert B) (Assns Theta' Theta)
| UnionE : forall {Theta1 Theta1' Theta2 Theta2' C X1 X2}
(eta: TEvid X1 C (Assns Theta1' Theta1))
(eta2: TEvid X2 C (Assns Theta2' Theta2)),
allVarsIn (X1++X2) X = true ->
TEvid X C (Assns (Theta1'++Theta2') (Theta1++Theta2))
| InstantiateE : forall a F C,
allVarsIn (AFv a) X = true ->
IntersectionNull (AFv a) (Mods C) = true ->
TEvid X C (Aforall F) -> TEvid X C (F a)
| ForAllE : forall F C, (forall a ,
allVarsIn (AFv a) X = true->
IntersectionNullP (AFv a) (Mods C) ->
TEvid X C (F a)) ->
TEvid X C (Aforall F).
TSkipE : forall {Theta'} Theta, Theta'=Theta ->
allVarsIn (TwoAssnsFv Theta ++
TwoAssnsFv Theta') X =true ->
TEvid X Skip (Assns Theta' Theta)
| TAAssignE : forall Theta x A {Theta'}, Theta'= (TwoAssnsSubstA Theta x A) ->
allVarsIn (AFv A ++
TwoAssnsFv Theta ++
TwoAssnsFv Theta') X =true ->
TEvid X (Assign x (AExp A)) (Assns Theta' Theta)
| TBAssignE : forall Theta x B {Theta'}, Theta'= (TwoAssnsSubstB Theta x B) ->
allVarsIn (BFv B ++
TwoAssnsFv Theta ++
TwoAssnsFv Theta') X =true ->
TEvid X (Assign x (BExp B)) (Assns Theta' Theta)
| THAssignE : forall Theta x H {Theta'}, Theta'= (TwoAssnsSubstH Theta x H) ->
allVarsIn (HFv H ++
TwoAssnsFv Theta ++
TwoAssnsFv Theta') X =true ->
TEvid X (Assign x (HExp H)) (Assns Theta' Theta)
| TSeqE: forall {Theta1 Theta Theta2 Theta' C1 C2}
(eta2: TEvid X C2 (Assns Theta' Theta2))
(eta1: TEvid X C1 (Assns Theta1 Theta)),
allVarsIn ((varsUsedIn C1) ++ (varsUsedIn C2) ++
TwoAssnsFv Theta ++
TwoAssnsFv Theta1 ++
TwoAssnsFv Theta2) X =true ->
Theta=Theta' -> TEvid X (Seq C1 C2) (Assns Theta1 Theta2)
| TCondE: forall {Theta1 Theta Theta2 Theta' C1 C2}
(eta1: TEvid X C1 (Assns Theta1 Theta))
(eta2: TEvid X C2 (Assns Theta2 Theta)) B,
((andIntoTheta Theta1 B) ++
andIntoTheta Theta2 (NotExpr B) ++
conBoolAgreement Theta1 Theta2 B) = Theta' ->
allVarsIn ((varsUsedIn C1) ++ (varsUsedIn C2) ++ (BFv B) ++
TwoAssnsFv Theta ++
TwoAssnsFv Theta1 ++
TwoAssnsFv Theta2 ++
TwoAssnsFv Theta') X =true ->
TEvid X (Cond B C1 C2) (Assns Theta' Theta)
| TPreImplyE : forall {Theta Theta1 Theta2 Theta2' C}
(eta : TEvid X C (Assns Theta2' Theta1))
(tau : TIEvid X Theta Theta2),
allVarsIn ((varsUsedIn C) ++
TwoAssnsFv Theta ++
TwoAssnsFv Theta1 ++
TwoAssnsFv Theta2 ++
TwoAssnsFv Theta2') X =true ->
Theta2 = Theta2' -> TEvid X C (Assns Theta Theta1)
| TPostImplyE : forall {Theta Theta1 Theta2 Theta2' C}
(eta: TEvid X C (Assns Theta Theta2'))
(tau: TIEvid X Theta2 Theta1),
allVarsIn ((varsUsedIn C) ++
TwoAssnsFv Theta ++
TwoAssnsFv Theta1 ++
TwoAssnsFv Theta2 ++
TwoAssnsFv Theta2') X =true ->
Theta2' = Theta2 -> TEvid X C (Assns Theta Theta1)
| TNotModE : forall {C L}
(mu : (Mods C) = L) Theta,
allVarsIn ((varsUsedIn C) ++
TwoAssnsFv Theta) X =true ->
(IntersectionNullP L (TwoAssnsFv Theta)) ->
TEvid X C (Assns Theta Theta)
| ConseqNotModE : forall phi phi' E C L,
Mods C = L ->
NPCEvid X phi C phi' ->
(IntersectionNullP L (fv E)) ->
TEvid X C (Assns [(phi, E)] [(phi', E)])
| TAssertE : forall Theta Theta' B, allVarsIn (BFv B ++ TwoAssnsFv Theta) X= true ->
Theta'= andIntoTheta Theta B ->
TEvid X (Assert B) (Assns Theta' Theta)
| UnionE : forall {Theta1 Theta1' Theta2 Theta2' C X1 X2}
(eta: TEvid X1 C (Assns Theta1' Theta1))
(eta2: TEvid X2 C (Assns Theta2' Theta2)),
allVarsIn (X1++X2) X = true ->
TEvid X C (Assns (Theta1'++Theta2') (Theta1++Theta2))
| InstantiateE : forall a F C,
allVarsIn (AFv a) X = true ->
IntersectionNull (AFv a) (Mods C) = true ->
TEvid X C (Aforall F) -> TEvid X C (F a)
| ForAllE : forall F C, (forall a ,
allVarsIn (AFv a) X = true->
IntersectionNullP (AFv a) (Mods C) ->
TEvid X C (F a)) ->
TEvid X C (Aforall F).