[2770] | 1 | include "basics/types.ma". |
---|
[1635] | 2 | include "utilities/monad.ma". |
---|
[1640] | 3 | |
---|
[1647] | 4 | definition Option ≝ MakeMonadProps |
---|
[1635] | 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 ?]) |
---|
[1882] | 11 | ????. |
---|
| 12 | // #X[|*:#Y[#Z]]*normalize//qed. |
---|
[1635] | 13 | |
---|
| 14 | include "hints_declaration.ma". |
---|
[1949] | 15 | alias symbol "hint_decl" (instance 1) = "hint_decl_Type1". |
---|
[1635] | 16 | unification hint 0 ≔ X; |
---|
[1882] | 17 | N ≟ max_def Option |
---|
[1635] | 18 | (*---------------*) ⊢ |
---|
[1882] | 19 | option X ≡ monad N X |
---|
[1635] | 20 | . |
---|
[1640] | 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.? |
---|
[1882] | 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 | |
---|
[1949] | 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 | |
---|
[1882] | 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 | |
---|
[1976] | 64 | definition OptPred ≝ λPdef : Prop.mk_InjMonadPred Option |
---|
| 65 | (mk_MonadPred ? |
---|
| 66 | (λX,P,x.Try ! y ← x ; return P y catch ⇒ Pdef) |
---|
| 67 | ???) |
---|
[1949] | 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 ]) |
---|
[1976] | 69 | ?. |
---|
| 70 | [4: @prf |
---|
[1949] | 71 | |*: |
---|
[1976] | 72 | #X[2:#Y]#P1[1,2:#P2[2:#H]] |
---|
[1949] | 73 | [1,2,4: * [5: *]] normalize /2/ |
---|
[1882] | 74 | qed. |
---|
| 75 | |
---|
| 76 | definition opt_All : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred True). |
---|
[1949] | 77 | |
---|
[1882] | 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 |
---|
[2767] | 84 | ≝ m_pred_mp …. |
---|
| 85 | |
---|
| 86 | (* moved from ASM/ASM.ma! *) |
---|
| 87 | definition partial_injection : ∀A,B.(A → option B) → Prop ≝ |
---|
| 88 | λA,B,f.∀x,y,z.f x = Some ? z → f y = Some ? z → x = y. |
---|