1 | include "basics/types.ma". |
---|
2 | include "utilities/monad.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 …. |
---|
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. |
---|