source: src/utilities/state.ma @ 1882

Last change on this file since 1882 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 1.6 KB
Line 
1include "utilities/monad.ma".
2
3definition State ≝
4  λS : Type[0].MakeSetoidMonadProps
5  (* the monad *)
6  (λX.S → S × X)
7  (* return *)
8  (λX,x,s.〈s,x〉)
9  (* bind *)
10  (λX,Y,m,f,s. let 〈s', x〉 ≝ m s in f x s')
11  (* monad eq *)
12  (λX,c1,c2.∀s.c1 s = c2 s)
13  ????????.
14// normalize
15#X
16[ (* bind_proper *)
17  #Y #m #n #f #g #H #G #s >H elim (n s) #s' #x normalize @G
18| #m#s @pair_elim //
19| #Y#Z #m #f #g #s elim (m s) //
20]
21qed.
22
23definition state_monad ≝ λS.monad (State S).
24
25definition state_get : ∀S.state_monad S S ≝ λS,s.〈s,s〉.
26definition state_set : ∀S.S → state_monad S unit ≝ λS,s.λ_.〈s,it〉.
27definition state_run : ∀S,X. S → (state_monad S X) → X ≝ λS,X,s,c.'pi2 (c s).
28
29include "hints_declaration.ma".
30unification hint 0 ≔ S,X;
31N ≟ State S, M ≟ smax_def N
32(*---------------*) ⊢
33state_monad S X ≡ monad M X
34.
35
36definition StatePred ≝ λS.λPs : S → Prop.mk_MonadPred (State S)
37  (λX,P,m.∀s.Ps s → let m' ≝ m s in Ps (\fst m') ∧ P (\snd m')) ???.
38[ normalize /2/
39| normalize #X#Y#P1#P2 #m #H #f #G #s #Ps lapply (H … Ps)
40  elim (m s) #s' #x normalize * /2/
41| #X #P #Q #H #m normalize #G #s #Ps elim (G … Ps) /3/
42]
43qed.
44
45definition StateRel ≝ λS,T.λPs : S → T → Prop.mk_MonadRel (State S) (State T)
46  (λX,Y,P,m,n.∀s,t.Ps s t → let m' ≝ m s in let n' ≝ n t in
47    Ps (\fst m') (\fst n') ∧ P (\snd m') (\snd n')) ???.
48[ normalize /2/
49| normalize #X#Y#Z#W#P1#P2 #m #n #H #f #g #G #s #t #Ps lapply (H … Ps)
50  * elim (m s) elim (n t) /2/
51| #X #Y #P #Q #H #m #n normalize #G #s #t #Ps elim (G … Ps) /3/
52]
53qed.
54
Note: See TracBrowser for help on using the repository browser.