Changeset 1949 for src/utilities


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
Location:
src/utilities
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

    r1930 r1949  
    4242qed.
    4343
    44 interpretation "logical iff" 'iff x y = (iff x y).
     44(* Paolo: already in library, generates ambiguity
     45interpretation "logical iff" 'iff x y = (iff x y).*)
    4546
    4647(* bool *)
  • src/utilities/lists.ma

    r1882 r1949  
    134134] qed.
    135135
     136alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
    136137unification hint 0 ≔ X ;
    137138N ≟ max_def List
  • 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
  • src/utilities/option.ma

    r1882 r1949  
    1313
    1414include "hints_declaration.ma".
     15alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
    1516unification hint 0 ≔ X;
    1617N ≟ max_def Option
     
    3839] qed.
    3940
     41lemma opt_safe_proof_irr : ∀A,m,prf1,prf2.
     42  opt_safe A m prf1 = opt_safe A m prf2.
     43  #A* // qed.
     44
    4045definition opt_try_catch : ∀X.option X → (unit → X) → X ≝
    4146  λX,m,f.match m with [Some x ⇒ x | None ⇒ f it].
     
    5762interpretation "option try and catch" 'trycatch m f = (opt_try_catch ? m f).
    5863
    59 definition OptPred ≝ λPdef : Prop.mk_MonadPred Option (λX,P,m.Try ! x ← m ; return P x catch ⇒ Pdef) ???.
    60 #X[2:#Y]#P1[1,3:#P2[2:#H]*] normalize /2/
     64definition OptPred ≝ λPdef : Prop.mk_MonadPred Option
     65  (λX,P,x.Try ! y ← x ; return P y catch ⇒ Pdef)
     66  (λX,P,m_sig.match m_sig with [ mk_Sig m prf ⇒ match m return λx.Try ! y ← x ; return P y catch ⇒ Pdef → option (Σy.?) with [ Some x ⇒ λprf.Some ? x | None ⇒ λ_.None ? ] prf ])
     67  ????.
     68[ @prf
     69|*:
     70#X[2:#Y]#P1[1,3:#P2[2:#H]]
     71[1,2,4: * [5: *]] normalize /2/
    6172qed.
    6273
    6374definition opt_All : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred True).
    64  
     75
    6576lemma opt_All_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_All A P o → opt_All ? Q o
    6677  ≝ m_pred_mp ….
     
    7081lemma opt_Exists_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_Exists A P o → opt_Exists ? Q o
    7182  ≝ m_pred_mp ….
    72 
Note: See TracChangeset for help on using the changeset viewer.