Changeset 1882 for src/utilities/state.ma
 Timestamp:
 Apr 6, 2012, 8:02:10 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/state.ma
r1647 r1882 12 12 (λX,c1,c2.∀s.c1 s = c2 s) 13 13 ????????. 14 // 14 // normalize 15 15 #X 16 16 [ (* bind_proper *) 17 #Y #m#n #m_eq_n 18 #f #g #f_eq_g 19 #s 20 generalize in match (m_eq_n s); m_eq_n 21 normalize 22 #m_eq_n >m_eq_n m_eq_n 23 elim (n s) #s' #y 24 normalize @f_eq_g // 25  #m#s normalize 26 elim (m s) normalize /2 by / 27  #Y #Z #m #f #g #s normalize 28 elim (m s) normalize 29 #s' #x 30 elim (f x s') normalize 31 #s'' #y // 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) // 32 20 ] 33 21 qed. … … 41 29 include "hints_declaration.ma". 42 30 unification hint 0 ≔ S,X; 43 N ≟ State S, M ≟ smax_def N , O ≟ m_def M31 N ≟ State S, M ≟ smax_def N 44 32 (**) ⊢ 45 state_monad S X ≡ monad OX33 state_monad S X ≡ monad M X 46 34 . 47 35 36 definition 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 ] 43 qed. 44 45 definition 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 ] 53 qed. 54
Note: See TracChangeset
for help on using the changeset viewer.