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 | let rec sublist (S:DeqSet) (l1:list S) (l2:list S) on l1 : bool ≝ |
---|
54 | match l1 with |
---|
55 | [ nil ⇒ true |
---|
56 | | cons hd tl ⇒ memb S hd l2 ∧ sublist S tl l2 ]. |
---|
57 | |
---|
58 | lemma sublist_hd_tl_to_memb: |
---|
59 | ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2. |
---|
60 | sublist S (hd::tl) l2 → memb S hd l2. |
---|
61 | #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize // |
---|
62 | qed. |
---|
63 | |
---|
64 | lemma sublist_hd_tl_to_sublist: |
---|
65 | ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2. |
---|
66 | sublist S (hd::tl) l2 → sublist S tl l2. |
---|
67 | #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize // #H cases H |
---|
68 | qed. |
---|
69 | |
---|
70 | let rec sub_expr_elim_type |
---|
71 | (E:Type[0]) (fixed_l: list tag) (orig: fixed_l E) |
---|
72 | (Q: fixed_l E → Prop) |
---|
73 | (l: list tag) |
---|
74 | on l : sublist Tag l fixed_l → Prop ≝ |
---|
75 | match l return λl. sublist Tag l fixed_l → Prop with |
---|
76 | [ nil ⇒ λH. Q orig |
---|
77 | | cons hd tl ⇒ λH. |
---|
78 | let tail_call ≝ sub_expr_elim_type E fixed_l orig Q tl ? in |
---|
79 | match hd return λt. memb Tag t fixed_l → Prop with |
---|
80 | [ num ⇒ λH. (∀n. Q (Num … n)) → tail_call |
---|
81 | | plus ⇒ λH. (∀x,y. Q (Plus … x y)) → tail_call |
---|
82 | | mul ⇒ λH. (∀x,y. Q (Mul … x y)) → tail_call |
---|
83 | ] (sublist_hd_tl_to_memb Tag hd tl fixed_l H)]. |
---|
84 | /2/ qed. |
---|
85 | |
---|
86 | |
---|
87 | |
---|
88 | (**************************************) |
---|
89 | |
---|
90 | definition eval_additive_expr: ∀E:Type[0]. (E → nat) → [plus] E → nat ≝ |
---|
91 | λE,f,e. |
---|
92 | match e return λe. is_in … [plus] e → nat with |
---|
93 | [ Plus x y ⇒ λH. f x + f y |
---|
94 | | _ ⇒ λH:False. ? |
---|
95 | ] (se_el_in ?? e). |
---|
96 | elim H qed. |
---|
97 | |
---|
98 | definition eval_multiplicative_expr: ∀E:Type[0]. (E → nat) → [mul] E → nat ≝ |
---|
99 | λE,f,e. |
---|
100 | match e return λe. is_in … [mul] e → nat with |
---|
101 | [ Mul x y ⇒ λH. f x * f y |
---|
102 | | _ ⇒ λH:False. ? |
---|
103 | ] (se_el_in ?? e). |
---|
104 | elim H qed. |
---|
105 | |
---|
106 | definition eval_additive_multiplicative_expr: ∀E:Type[0]. (E → nat) → [plus;mul] E → nat ≝ |
---|
107 | λE,f,e. |
---|
108 | match e return λe. is_in … [plus;mul] e → nat with |
---|
109 | [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y) |
---|
110 | | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y) |
---|
111 | | _ ⇒ λH:False. ? |
---|
112 | ] (se_el_in ?? e). |
---|
113 | [2,3: % | elim H] |
---|
114 | qed. |
---|
115 | |
---|
116 | definition eval_additive_multiplicative_constant_expr: ∀E:Type[0]. (E → nat) → [plus;mul;num] E → nat ≝ |
---|
117 | λE,f,e. |
---|
118 | match e return λe. is_in … [plus;mul;num] e → nat with |
---|
119 | [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y) |
---|
120 | | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y) |
---|
121 | | Num n ⇒ λH. n |
---|
122 | ] (se_el_in ?? e). |
---|
123 | % qed. |
---|
124 | |
---|
125 | (*CSC: not accepted :-( |
---|
126 | inductive expr_no_const : Type[0] ≝ K : [plus;mul] expr_no_const → expr_no_const. |
---|
127 | *) |
---|
128 | |
---|
129 | inductive final_expr : Type[0] ≝ K : expr final_expr → final_expr. |
---|
130 | |
---|
131 | coercion K. |
---|
132 | |
---|
133 | let rec eval_final_expr e on e : nat ≝ |
---|
134 | match e with |
---|
135 | [ K e' ⇒ eval_additive_multiplicative_constant_expr final_expr eval_final_expr e']. |
---|
136 | cases e' try #x try #y % |
---|
137 | qed. |
---|
138 | |
---|
139 | example test: eval_final_expr (K (Mul ? (Num ? 2) (Num ? 3))) = 6. |
---|
140 | % qed. |
---|