Changeset 1976 for src/utilities/state.ma
 Timestamp:
 May 21, 2012, 7:04:21 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/state.ma
r1882 r1976 1 1 include "utilities/monad.ma". 2 2 3 definition State≝3 definition state_monad ≝ 4 4 λS : Type[0].MakeSetoidMonadProps 5 5 (* the monad *) … … 21 21 qed. 22 22 23 definition state_monad ≝ λS.monad (State S).24 25 23 definition state_get : ∀S.state_monad S S ≝ λS,s.〈s,s〉. 26 24 definition state_set : ∀S.S → state_monad S unit ≝ λS,s.λ_.〈s,it〉. 27 25 definition state_run : ∀S,X. S → (state_monad S X) → X ≝ λS,X,s,c.'pi2 (c s). 28 26 29 include "hints_declaration.ma". 30 unification hint 0 ≔ S,X; 31 N ≟ State S, M ≟ smax_def N 32 (**) ⊢ 33 state_monad S X ≡ monad M X 34 . 35 36 definition StatePred ≝ λS.λPs : S → Prop.mk_MonadPred (State S) 27 definition state_pred ≝ λS.λPs : S → Prop.mk_MonadPred (state_monad S) 37 28 (λX,P,m.∀s.Ps s → let m' ≝ m s in Ps (\fst m') ∧ P (\snd m')) ???. 38 [ normalize /2 /29 [ normalize /2 by conj/ 39 30  normalize #X#Y#P1#P2 #m #H #f #G #s #Ps lapply (H … Ps) 40 31 elim (m s) #s' #x normalize * /2/ … … 43 34 qed. 44 35 45 definition StateRel ≝ λS,T.λPs : S → T → Prop.mk_MonadRel ( State S) (StateT)36 definition StateRel ≝ λS,T.λPs : S → T → Prop.mk_MonadRel (state_monad S) (state_monad T) 46 37 (λX,Y,P,m,n.∀s,t.Ps s t → let m' ≝ m s in let n' ≝ n t in 47 38 Ps (\fst m') (\fst n') ∧ P (\snd m') (\snd n')) ???.
Note: See TracChangeset
for help on using the changeset viewer.