Ignore:
Timestamp:
Aug 29, 2011, 5:45:03 PM (8 years ago)
Author:
campbell
Message:

Extra results for non-failing map updates.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/utilities/option.ma

    r761 r1134  
    33definition option_map : ∀A,B:Type[0]. (A → B) → option A → option B ≝
    44λ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
     18lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → False.
     19  (∀v. x = Some ? v → Q (P v)) →
     20  Q (match x return λy.x = y → ? with [ Some v ⇒ λ_. P v | None ⇒ λE. match H E in False with [ ] ] (refl ? x)).
     21#A #B #P #Q *
     22[ #H cases (H (refl ??))
     23| #a #H #p normalize @p @refl
     24] qed.
     25
Note: See TracChangeset for help on using the changeset viewer.