source: src/utilities/option.ma @ 1882

Last change on this file since 1882 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 2.2 KB
Line 
1include "utilities/monad.ma".
2include "basics/types.ma".
3
4definition 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
14include "hints_declaration.ma".
15unification hint 0 ≔ X;
16N ≟ max_def Option
17(*---------------*) ⊢
18option X ≡ monad N X
19.
20
21definition opt_safe : ∀X.∀m : option X. m ≠ None X → X ≝
22λX,m,prf.match m return λx.m = x → X with
23  [ Some t ⇒ λ_.t
24  | None ⇒ λeq_m.?
25  ] (refl …). elim (absurd … eq_m prf) qed.
26
27lemma opt_to_opt_safe : ∀A,m,prf. m = Some ? (opt_safe A m prf).
28#A *
29[ #ABS elim (absurd ? (refl ??) ABS)
30| //
31] qed.
32
33lemma opt_safe_elim : ∀A.∀P : A → Prop.∀m,prf.
34  (∀x.m = Some ? x → P x) → P (opt_safe ? m prf).
35#A#P*
36[#prf elim(absurd … (refl ??) prf)
37|#x normalize #_ #H @H @refl
38] qed.
39
40definition opt_try_catch : ∀X.option X → (unit → X) → X ≝
41  λX,m,f.match m with [Some x ⇒ x | None ⇒ f it].
42
43notation > "'Try' m 'catch' opt (ident e opt( : ty)) ⇒ f" with precedence 46 for
44  ${ default
45    @{ ${ default
46      @{'trycatch $m (λ${ident e}:$ty.$f)}
47      @{'trycatch $m (λ${ident e}.$f)}
48    }}
49    @{'trycatch $m (λ_.$f)}
50  }.
51
52notation < "hvbox('Try' \nbsp break m \nbsp break 'catch' \nbsp ident e : ty \nbsp ⇒ \nbsp break f)" with precedence 46 for
53  @{'trycatch $m (λ${ident e}:$ty.$f)}.
54notation < "hvbox('Try' \nbsp break m \nbsp break 'catch' \nbsp ⇒ \nbsp break f)" with precedence 46 for
55  @{'trycatch $m (λ_:$ty.$f)}.
56
57interpretation "option try and catch" 'trycatch m f = (opt_try_catch ? m f).
58
59definition 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/
61qed.
62
63definition opt_All : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred True).
64 
65lemma opt_All_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_All A P o → opt_All ? Q o
66  ≝ m_pred_mp ….
67
68definition opt_Exists : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred False).
69 
70lemma opt_Exists_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_Exists A P o → opt_Exists ? Q o
71  ≝ m_pred_mp ….
72
Note: See TracBrowser for help on using the repository browser.