# source:src/utilities/option.ma@1551

Last change on this file since 1551 was 1551, checked in by campbell, 9 years ago

Functions to translate between back-end and front-end values.

File size: 1013 bytes
Line
1include "basics/types.ma".
2
3definition option_map : ∀A,B:Type[0]. (A → B) → option A → option B ≝
4λA,B,f,o. match o with [ None ⇒ None B | Some a ⇒ Some B (f a) ].
5
6lemma option_map_none : ∀A,B,f,x.
7  option_map A B f x = None B → x = None A.
8#A #B #f * [ // | #a #E whd in E:(??%?); destruct ]
9qed.
10
11lemma option_map_some : ∀A,B,f,x,v.
12  option_map A B f x = Some B v → ∃y. x = Some ? y ∧ f y = v.
13#A #B #f *
14[ #v normalize #E destruct
15| #y #v normalize #E %{y} destruct % //
16] qed.
17
18definition option_map_def : ∀A,B:Type[0]. (A → B) → B → option A → B ≝
19λA,B,f,d,o. match o with [ None ⇒ d | Some a ⇒ f a ].
20
21lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → False.
22  (∀v. x = Some ? v → Q (P v)) →
23  Q (match x return λy.x = y → ? with [ Some v ⇒ λ_. P v | None ⇒ λE. match H E in False with [ ] ] (refl ? x)).
24#A #B #P #Q *
25[ #H cases (H (refl ??))
26| #a #H #p normalize @p @refl
27] qed.
28
Note: See TracBrowser for help on using the repository browser.