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

Functions to translate between backend and frontend 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.