Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 years ago)
Author:
tranquil
Message:

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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/state.ma

    r1647 r1882  
    1212  (λX,c1,c2.∀s.c1 s = c2 s)
    1313  ????????.
    14 //
     14// normalize
    1515#X
    1616[ (* 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) //
    3220]
    3321qed.
     
    4129include "hints_declaration.ma".
    4230unification hint 0 ≔ S,X;
    43 N ≟ State S, M ≟ smax_def N, O ≟ m_def M
     31N ≟ State S, M ≟ smax_def N
    4432(*---------------*) ⊢
    45 state_monad S X ≡ monad O X
     33state_monad S X ≡ monad M X
    4634.
    4735
     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 TracChangeset for help on using the changeset viewer.