Invariant in the proof of AllGoodAlg, first attempt
- We would like to introduce the following definitions
(essentially the free theorem for the state monad):
property RelatedResult R =
{| r1,r2 | {fst r1}==={fst r2} /\ R {snd r1} {snd r2} |}
property MostlyStateIndependent R =
{| m | ∀ s1 . ∀ s2 .
R s1 s2 ==> RelatedResult R {runS m s1} {runS m s2} |}
assert ReturnS = ∀ x . ∀ R . MostlyStateIndependent R {return x}
assert BindS =
∀ m1 . ∀ xm2 . ∀ R .
MostlyStateIndependent R m1 ==>
(∀ x . MostlyStateIndependent R {xm2 x}) ==>
MostlyStateIndependent R {m1 >>= xm2}
- This is the way my first proof in Alfa was structured.
- But P-Logic is a first-order logic, so this is not allowed.