source: src/utilities/option.ma @ 2896

Last change on this file since 2896 was 2770, checked in by mckinna, 7 years ago

WARNING: another big commit, touching many files in ASM/*.ma

This edit
a) prunes many redundant "include"s from ASM/*.ma hierarchy
b) adjusts the use of aliases from ASM/ and elsewhere (big, annoying, hard-to-debug disambiguation errors), from the earlier adjustment to ASM/ASM.ma
c) adds ONE (and once repeated) type annotation to ASM/Interpret.ma

As with the continual failures with Clight/switchRemoval.ma, the (revised) definition of execute_1_preinstruction causes no end of disambiguation thrashing. One type annotation (in the JMP case, to ensure that program_counter calculations actually produce values in Word) is enough to cut that particular Gordian knot. By russell-style reasoning, the annotation then gets repeated later, though in fact in that later instance is redundant...

File size: 2.8 KB
Line 
1include "basics/types.ma".
2include "utilities/monad.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".
15alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
16unification hint 0 ≔ X;
17N ≟ max_def Option
18(*---------------*) ⊢
19option X ≡ monad N X
20.
21
22definition 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
28lemma 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
34lemma 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
41lemma opt_safe_proof_irr : ∀A,m,prf1,prf2.
42  opt_safe A m prf1 = opt_safe A m prf2.
43  #A* // qed.
44
45definition opt_try_catch : ∀X.option X → (unit → X) → X ≝
46  λX,m,f.match m with [Some x ⇒ x | None ⇒ f it].
47
48notation > "'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
57notation < "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)}.
59notation < "hvbox('Try' \nbsp break m \nbsp break 'catch' \nbsp ⇒ \nbsp break f)" with precedence 46 for
60  @{'trycatch $m (λ_:$ty.$f)}.
61
62interpretation "option try and catch" 'trycatch m f = (opt_try_catch ? m f).
63
64definition 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/
74qed.
75
76definition opt_All : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred True).
77
78lemma 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
81definition opt_Exists : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred False).
82 
83lemma 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! *)
87definition 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.
Note: See TracBrowser for help on using the repository browser.