source: src/utilities/state.ma @ 1976

Last change on this file since 1976 was 1976, checked in by tranquil, 8 years ago
  • monads: just changed some defs, which had to be propagated in some files
  • ASM/CostProof.ma: linked cost as defined there to the one in StructuredTraces? that uses fold
  • added a library for permutations of lists (useful with fold AC ops on lists)
  • first draft of abstract_status implementation for joint languages (file joint/as_semantics.ma)
File size: 1.4 KB
Line 
1include "utilities/monad.ma".
2
3definition state_monad ≝
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_get : ∀S.state_monad S S ≝ λS,s.〈s,s〉.
24definition state_set : ∀S.S → state_monad S unit ≝ λS,s.λ_.〈s,it〉.
25definition state_run : ∀S,X. S → (state_monad S X) → X ≝ λS,X,s,c.'pi2 (c s).
26
27definition state_pred ≝ λS.λPs : S → Prop.mk_MonadPred (state_monad S)
28  (λX,P,m.∀s.Ps s → let m' ≝ m s in Ps (\fst m') ∧ P (\snd m')) ???.
29[ normalize /2 by conj/
30| normalize #X#Y#P1#P2 #m #H #f #G #s #Ps lapply (H … Ps)
31  elim (m s) #s' #x normalize * /2/
32| #X #P #Q #H #m normalize #G #s #Ps elim (G … Ps) /3/
33]
34qed.
35
36definition StateRel ≝ λS,T.λPs : S → T → Prop.mk_MonadRel (state_monad S) (state_monad T)
37  (λX,Y,P,m,n.∀s,t.Ps s t → let m' ≝ m s in let n' ≝ n t in
38    Ps (\fst m') (\fst n') ∧ P (\snd m') (\snd n')) ???.
39[ normalize /2/
40| normalize #X#Y#Z#W#P1#P2 #m #n #H #f #g #G #s #t #Ps lapply (H … Ps)
41  * elim (m s) elim (n t) /2/
42| #X #Y #P #Q #H #m #n normalize #G #s #t #Ps elim (G … Ps) /3/
43]
44qed.
45
Note: See TracBrowser for help on using the repository browser.