|
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
|
| Rev | Line | |
|---|
| [761] | 1 | include "basics/types.ma". |
|---|
| 2 | |
|---|
| 3 | definition 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) ]. |
|---|
| [1316] | 5 | |
|---|
| 6 | lemma 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 ] |
|---|
| 9 | qed. |
|---|
| 10 | |
|---|
| 11 | lemma 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 | |
|---|
| [1551] | 18 | definition 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 | |
|---|
| [1316] | 21 | lemma 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.
