Ignore:
Timestamp:
May 15, 2012, 5:51:25 PM (8 years ago)
Author:
tranquil
Message:
  • lemma trace rel to eq flatten trace
  • some more properties of generic monad relations and predicates
  • removed 'iff notation from extralib as already there
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/monad.ma

    r1882 r1949  
    152152
    153153include "hints_declaration.ma".
    154 
     154alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
    155155unification hint 0 ≔ M, X;
    156156M' ≟ smax_def M, S ≟ setoid_of_monad M X
     
    226226  mk_SetoidMonadProps (mk_Monad monad m_return m_bind).
    227227 
     228include "basics/russell.ma".
     229 
    228230record MonadPred (M : Monad) : Type[1] ≝
    229231  { m_pred :> ∀X.pred_transformer X (monad M X)
     232  ; mp_inject : ∀X,P.(Σm.m_pred X P m) → monad M (Σx.P x)
    230233  ; mp_return : ∀X,P,x.P x → m_pred X P (return x)
    231234  ; mp_bind : ∀X,Y,Pin,Pout,m.m_pred X Pin m →
     
    233236                  m_pred ? Pout (m_bind … m f)
    234237  ; m_pred_mp : ∀X.modus_ponens ?? (m_pred X)
    235   }.
     238  ; mp_inject_eq : ∀X,P,m.pi1 ?? m = ! x ← mp_inject X P m ; return pi1 … x
     239  }.
     240
     241coercion coerc_mp_inject : ∀M.∀MP:MonadPred M.
     242  ∀X,P.∀m : Σm.m_pred ? MP X P m.monad M (Σx.P x) ≝
     243  mp_inject on _m : Sig (monad ??) (λm.m_pred ???? m) to monad ? (Sig ? (λx.? x)).
     244
     245lemma mp_inject_bind : ∀M : MonadProps.∀MP,X,P,Y.∀m.∀f : X → monad M Y.
     246  ! x ← mp_inject M MP X P m ; f (pi1 … x) = ! x ← pi1 … m ; f x.
     247#M#MP#X#P#Y#m#f >mp_inject_eq >m_bind_bind @m_bind_ext_eq #x >m_return_bind % qed.
    236248
    237249record MonadRel (M1 : Monad) (M2 : Monad) : Type[1] ≝
     
    242254  ; m_rel_mp : ∀X,Y.rel_modus_ponens ???? (m_rel X Y)
    243255  }.
     256
     257
Note: See TracChangeset for help on using the changeset viewer.