1 | include "basics/lists/listb.ma". |
---|
2 | |
---|
3 | definition bool_to_Prop : bool → Prop ≝ |
---|
4 | λb. match b with [ true ⇒ True | false ⇒ False ]. |
---|
5 | |
---|
6 | coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. |
---|
7 | |
---|
8 | inductive expr (E: Type[0]) : Type[0] ≝ |
---|
9 | Num : nat -> expr E |
---|
10 | | Plus : E -> E -> expr E |
---|
11 | | Mul : E -> E -> expr E. |
---|
12 | |
---|
13 | inductive tag : Type[0] := num : tag | plus : tag | mul : tag. |
---|
14 | |
---|
15 | definition eq_tag : tag -> tag -> bool := |
---|
16 | λt1,t2. |
---|
17 | match t1 with |
---|
18 | [ num => match t2 with [num => true | _ => false] |
---|
19 | | plus => match t2 with [plus => true | _ => false] |
---|
20 | | mul => match t2 with [mul => true | _ => false]]. |
---|
21 | |
---|
22 | definition Tag : DeqSet ≝ mk_DeqSet tag eq_tag ?. |
---|
23 | ** normalize /2/ % #abs destruct |
---|
24 | qed. |
---|
25 | |
---|
26 | definition tag_of_expr : ∀E:Type[0]. expr E -> tag := |
---|
27 | λE,e. |
---|
28 | match e with |
---|
29 | [ Num _ => num |
---|
30 | | Plus _ _ => plus |
---|
31 | | Mul _ _ => mul ]. |
---|
32 | |
---|
33 | (*definition is_a : ∀E: Type[0]. tag -> expr E -> Prop ≝ |
---|
34 | λE,t,e. eq_tag t (tag_of_expr \ldots e).*) |
---|
35 | |
---|
36 | definition is_in : ∀E: Type[0]. list tag -> expr E -> bool ≝ |
---|
37 | λE,l,e. memb Tag (tag_of_expr ? e) l. |
---|
38 | |
---|
39 | record sub_expr (l: list tag) (E: Type[0]) : Type[0] ≝ |
---|
40 | { |
---|
41 | se_el :> expr E; |
---|
42 | se_el_in: is_in … l se_el |
---|
43 | }. |
---|
44 | |
---|
45 | coercion sub_expr : ∀l:list tag. Type[0] → Type[0] |
---|
46 | ≝ sub_expr on _l: list tag to Type[0] → Type[0]. |
---|
47 | |
---|
48 | coercion mk_sub_expr : |
---|
49 | ∀l:list tag.∀E.∀e:expr E. |
---|
50 | ∀p:is_in ? l e.sub_expr l E |
---|
51 | ≝ mk_sub_expr on e:expr ? to sub_expr ? ?. |
---|
52 | |
---|
53 | (**************************************) |
---|
54 | |
---|
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. |
---|
80 | |
---|
81 | definition eval_additive_multiplicative_constant_expr: ∀E:Type[0]. (E → nat) → [plus;mul;num] E → nat ≝ |
---|
82 | λE,f,e. |
---|
83 | match e return λe. is_in … [plus;mul;num] e → nat with |
---|
84 | [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y) |
---|
85 | | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y) |
---|
86 | | Num n ⇒ λH. n |
---|
87 | ] (se_el_in ?? e). |
---|
88 | % qed. |
---|
89 | |
---|
90 | (*CSC: not accepted :-( |
---|
91 | inductive expr_no_const : Type[0] ≝ K : [plus;mul] expr_no_const → expr_no_const. |
---|
92 | *) |
---|
93 | |
---|
94 | inductive final_expr : Type[0] ≝ K : expr final_expr → final_expr. |
---|
95 | |
---|
96 | coercion K. |
---|
97 | |
---|
98 | let rec eval_final_expr e on e : nat ≝ |
---|
99 | match e with |
---|
100 | [ K e' ⇒ eval_additive_multiplicative_constant_expr final_expr eval_final_expr e']. |
---|
101 | cases e' try #x try #y % |
---|
102 | qed. |
---|
103 | |
---|
104 | example test: eval_final_expr (K (Mul ? (Num ? 2) (Num ? 3))) = 6. |
---|
105 | % qed. |
---|