 Timestamp:
 Oct 18, 2012, 3:57:33 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/polymorphicvariants2012/test.ma
r2402 r2403 4 4 λb. match b with [ true ⇒ True  false ⇒ False ]. 5 5 6 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. 7 6 8 inductive expr (E: Type[0]) : Type[0] ≝ 7 9 Num : nat > expr E 8  Plus : expr E > exprE > expr E9  Mul : expr E > exprE > expr E.10  Plus : E > E > expr E 11  Mul : E > E > expr E. 10 12 11 13 inductive tag : Type[0] := num : tag  plus : tag  mul : tag. … … 38 40 { 39 41 se_el :> expr E; 40 se_el_in: bool_to_Prop (is_in … l se_el)42 se_el_in: is_in … l se_el 41 43 }. 42 44 … … 46 48 coercion mk_sub_expr : 47 49 ∀l:list tag.∀E.∀e:expr E. 48 ∀p: bool_to_Prop (is_in ? l e).sub_expr l E49 ≝ mk_sub_expr on e:expr Eto sub_expr ? ?.50 ∀p:is_in ? l e.sub_expr l E 51 ≝ mk_sub_expr on e:expr ? to sub_expr ? ?. 50 52 51 53 (**************************************) 52 54 53 definition additive_expr : Type[0] → Type[0] ≝ λE. [plus] E. 55 definition eval_additive_expr: ∀E:Type[0]. (E → nat) → [plus] E → nat ≝ 56 λE,f,e. 57 match e return λe. is_in … [plus] e → nat with 58 [ Plus x y ⇒ λH. f x + f y 59  _ ⇒ λH:False. ? 60 ] (se_el_in ?? e). 61 elim H qed. 62 63 definition eval_multiplicative_expr: ∀E:Type[0]. (E → nat) → [mul] E → nat ≝ 64 λE,f,e. 65 match e return λe. is_in … [mul] e → nat with 66 [ Mul x y ⇒ λH. f x + f y 67  _ ⇒ λH:False. ? 68 ] (se_el_in ?? e). 69 elim H qed. 70 71 definition eval_additive_multiplicative_expr: ∀E:Type[0]. (E → nat) → [plus;mul] E → nat ≝ 72 λE,f,e. 73 match e return λe. is_in … [plus;mul] e → nat with 74 [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y) 75  Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y) 76  _ ⇒ λH:False. ? 77 ] (se_el_in ?? e). 78 [2,3: %  elim H] 79 qed.
Note: See TracChangeset
for help on using the changeset viewer.