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/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.