Changeset 1134 for Deliverables/D3.3/idlookupbranch/utilities/option.ma
 Timestamp:
 Aug 29, 2011, 5:45:03 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/utilities/option.ma
r761 r1134 3 3 definition option_map : ∀A,B:Type[0]. (A → B) → option A → option B ≝ 4 4 λA,B,f,o. match o with [ None ⇒ None B  Some a ⇒ Some B (f a) ]. 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 18 lemma 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.