Library evidence

Require Export synEq.
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.

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.

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.

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.

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.

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

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.

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