Changeset 1949 for src/utilities/option.ma

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:

• src/utilities/option.ma (modified) (4 diffs)

src/utilities/option.ma

@@ -13 +13 @@
 
 include "hints_declaration.ma".
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
 unification hint 0 ≔ X;
 N ≟ max_def Option
@@ -38 +39 @@
 ] qed.
 
+lemma opt_safe_proof_irr : ∀A,m,prf1,prf2.
+  opt_safe A m prf1 = opt_safe A m prf2.
+  #A* // qed.
+
 definition opt_try_catch : ∀X.option X → (unit → X) → X ≝
   λX,m,f.match m with [Some x ⇒ x | None ⇒ f it].
@@ -57 +62 @@
 interpretation "option try and catch" 'trycatch m f = (opt_try_catch ? m f).
 
-definition OptPred ≝ λPdef : Prop.mk_MonadPred Option (λX,P,m.Try ! x ← m ; return P x catch ⇒ Pdef) ???.
-#X[2:#Y]#P1[1,3:#P2[2:#H]*] normalize /2/
+definition OptPred ≝ λPdef : Prop.mk_MonadPred Option
+  (λX,P,x.Try ! y ← x ; return P y catch ⇒ Pdef)
+  (λ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 ])
+  ????.
+[ @prf
+|*:
+#X[2:#Y]#P1[1,3:#P2[2:#H]]
+[1,2,4: * [5: *]] normalize /2/
 qed.
 
 definition opt_All : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred True).
- 
+
 lemma opt_All_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_All A P o → opt_All ? Q o
   ≝ m_pred_mp ….
@@ -70 +81 @@
 lemma opt_Exists_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_Exists A P o → opt_Exists ? Q o
   ≝ m_pred_mp ….
-