| 1 | include "utilities/monad.ma". |
|---|
| 2 | include "basics/types.ma". |
|---|
| 3 | |
|---|
| 4 | definition Option ≝ MakeMonadProps |
|---|
| 5 | (* the monad *) |
|---|
| 6 | option |
|---|
| 7 | (* return *) |
|---|
| 8 | (λX.Some X) |
|---|
| 9 | (* bind *) |
|---|
| 10 | (λX,Y,m,f. match m with [ Some x ⇒ f x | None ⇒ None ?]) |
|---|
| 11 | ????. |
|---|
| 12 | // #X[|*:#Y[#Z]]*normalize//qed. |
|---|
| 13 | |
|---|
| 14 | include "hints_declaration.ma". |
|---|
| 15 | alias symbol "hint_decl" (instance 1) = "hint_decl_Type1". |
|---|
| 16 | unification hint 0 ≔ X; |
|---|
| 17 | N ≟ max_def Option |
|---|
| 18 | (*---------------*) ⊢ |
|---|
| 19 | option X ≡ monad N X |
|---|
| 20 | . |
|---|
| 21 | |
|---|
| 22 | definition opt_safe : ∀X.∀m : option X. m ≠ None X → X ≝ |
|---|
| 23 | λX,m,prf.match m return λx.m = x → X with |
|---|
| 24 | [ Some t ⇒ λ_.t |
|---|
| 25 | | None ⇒ λeq_m.? |
|---|
| 26 | ] (refl …). elim (absurd … eq_m prf) qed. |
|---|
| 27 | |
|---|
| 28 | lemma opt_to_opt_safe : ∀A,m,prf. m = Some ? (opt_safe A m prf). |
|---|
| 29 | #A * |
|---|
| 30 | [ #ABS elim (absurd ? (refl ??) ABS) |
|---|
| 31 | | // |
|---|
| 32 | ] qed. |
|---|
| 33 | |
|---|
| 34 | lemma opt_safe_elim : ∀A.∀P : A → Prop.∀m,prf. |
|---|
| 35 | (∀x.m = Some ? x → P x) → P (opt_safe ? m prf). |
|---|
| 36 | #A#P* |
|---|
| 37 | [#prf elim(absurd … (refl ??) prf) |
|---|
| 38 | |#x normalize #_ #H @H @refl |
|---|
| 39 | ] qed. |
|---|
| 40 | |
|---|
| 41 | lemma opt_safe_proof_irr : ∀A,m,prf1,prf2. |
|---|
| 42 | opt_safe A m prf1 = opt_safe A m prf2. |
|---|
| 43 | #A* // qed. |
|---|
| 44 | |
|---|
| 45 | definition opt_try_catch : ∀X.option X → (unit → X) → X ≝ |
|---|
| 46 | λX,m,f.match m with [Some x ⇒ x | None ⇒ f it]. |
|---|
| 47 | |
|---|
| 48 | notation > "'Try' m 'catch' opt (ident e opt( : ty)) ⇒ f" with precedence 46 for |
|---|
| 49 | ${ default |
|---|
| 50 | @{ ${ default |
|---|
| 51 | @{'trycatch $m (λ${ident e}:$ty.$f)} |
|---|
| 52 | @{'trycatch $m (λ${ident e}.$f)} |
|---|
| 53 | }} |
|---|
| 54 | @{'trycatch $m (λ_.$f)} |
|---|
| 55 | }. |
|---|
| 56 | |
|---|
| 57 | notation < "hvbox('Try' \nbsp break m \nbsp break 'catch' \nbsp ident e : ty \nbsp ⇒ \nbsp break f)" with precedence 46 for |
|---|
| 58 | @{'trycatch $m (λ${ident e}:$ty.$f)}. |
|---|
| 59 | notation < "hvbox('Try' \nbsp break m \nbsp break 'catch' \nbsp ⇒ \nbsp break f)" with precedence 46 for |
|---|
| 60 | @{'trycatch $m (λ_:$ty.$f)}. |
|---|
| 61 | |
|---|
| 62 | interpretation "option try and catch" 'trycatch m f = (opt_try_catch ? m f). |
|---|
| 63 | |
|---|
| 64 | definition OptPred ≝ λPdef : Prop.mk_InjMonadPred Option |
|---|
| 65 | (mk_MonadPred ? |
|---|
| 66 | (λX,P,x.Try ! y ← x ; return P y catch ⇒ Pdef) |
|---|
| 67 | ???) |
|---|
| 68 | (λ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 ]) |
|---|
| 69 | ?. |
|---|
| 70 | [4: @prf |
|---|
| 71 | |*: |
|---|
| 72 | #X[2:#Y]#P1[1,2:#P2[2:#H]] |
|---|
| 73 | [1,2,4: * [5: *]] normalize /2/ |
|---|
| 74 | qed. |
|---|
| 75 | |
|---|
| 76 | definition opt_All : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred True). |
|---|
| 77 | |
|---|
| 78 | lemma opt_All_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_All A P o → opt_All ? Q o |
|---|
| 79 | ≝ m_pred_mp …. |
|---|
| 80 | |
|---|
| 81 | definition opt_Exists : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred False). |
|---|
| 82 | |
|---|
| 83 | lemma opt_Exists_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_Exists A P o → opt_Exists ? Q o |
|---|
| 84 | ≝ m_pred_mp …. |
|---|
