[2514] | 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 | record test (A:Type[0]) (B:Type[0]) (C:Type[0]) : Type[0] ≝ |
---|
| 9 | { a:A; b:B; c:C }. |
---|
| 10 | |
---|
| 11 | inductive tag : Type[0] := a : tag | b : tag | c : tag. |
---|
| 12 | |
---|
| 13 | definition tag_of_pos : nat → tag ≝ |
---|
| 14 | λn. if eqb n 0 then a else if eqb n 1 then b else c. |
---|
| 15 | |
---|
| 16 | definition type_of_tag : tag → Type[0] ≝ |
---|
| 17 | λt. |
---|
| 18 | match t with |
---|
| 19 | [ a ⇒ nat |
---|
| 20 | | b ⇒ bool |
---|
| 21 | | c ⇒ nat ]. |
---|
| 22 | |
---|
| 23 | definition eq_tag : tag → tag → bool ≝ |
---|
| 24 | λt1,t2. |
---|
| 25 | match t1 with |
---|
| 26 | [ a => match t2 with [a => true | _ => false] |
---|
| 27 | | b => match t2 with [b => true | _ => false] |
---|
| 28 | | c => match t2 with [c => true | _ => false]]. |
---|
| 29 | |
---|
| 30 | definition Tag : DeqSet ≝ mk_DeqSet tag eq_tag ?. |
---|
| 31 | ** normalize /2/ % #abs destruct |
---|
| 32 | qed. |
---|
| 33 | |
---|
| 34 | let rec Types (n:nat) on n : Type[1] ≝ |
---|
| 35 | match n with |
---|
| 36 | [ O ⇒ Type[0] |
---|
| 37 | | S m ⇒ Type[0] → Types m ]. |
---|
| 38 | |
---|
| 39 | let rec record_ty0 (l: list tag) (n:nat) on n : Types n → Type[0] ≝ |
---|
| 40 | match n return λn. Types n → Type[0] with |
---|
| 41 | [ O ⇒ λr:Type[0].r |
---|
| 42 | | S m ⇒ λhd:Type[0] → Types m. |
---|
| 43 | let tag ≝ tag_of_pos m in |
---|
| 44 | if memb Tag tag l then |
---|
| 45 | record_ty0 l m (hd (type_of_tag tag)) |
---|
| 46 | else |
---|
| 47 | record_ty0 l m (hd unit)]. |
---|
| 48 | |
---|
| 49 | definition record_ty : list tag → Type[0] ≝ |
---|
| 50 | λl. record_ty0 l 3 test. |
---|
| 51 | |
---|
| 52 | coercion record_ty : ∀l:list tag. Type[0] |
---|
| 53 | ≝ record_ty on _l: list tag to Type[0]. |
---|
| 54 | |
---|
| 55 | XXX |
---|
| 56 | |
---|
| 57 | let rec mk_record_ty (l: list tag) (n:nat) on n : Type[0] ≝ |
---|
| 58 | match n with |
---|
| 59 | [ O ⇒ l |
---|
| 60 | | |
---|
| 61 | ]. |
---|
| 62 | |
---|
| 63 | let rec mk_record (l: list (Σt:tag. type_of_tag t)) (n:nat) on n : mk_record_ty n → l ≝ |
---|
| 64 | match n return with |
---|
| 65 | [ |
---|
| 66 | ]. |
---|
| 67 | |
---|
| 68 | definition tag_of_expr : ∀E:Type[0]. expr E -> tag := |
---|
| 69 | λE,e. |
---|
| 70 | match e with |
---|
| 71 | [ Num _ => num |
---|
| 72 | | Plus _ _ => plus |
---|
| 73 | | Mul _ _ => mul ]. |
---|
| 74 | |
---|
| 75 | (*definition is_a : ∀E: Type[0]. tag -> expr E -> Prop ≝ |
---|
| 76 | λE,t,e. eq_tag t (tag_of_expr \ldots e).*) |
---|
| 77 | |
---|
| 78 | definition is_in : ∀E: Type[0]. list tag -> expr E -> bool ≝ |
---|
| 79 | λE,l,e. memb Tag (tag_of_expr ? e) l. |
---|
| 80 | |
---|
| 81 | record sub_expr (l: list tag) (E: Type[0]) : Type[0] ≝ |
---|
| 82 | { |
---|
| 83 | se_el :> expr E; |
---|
| 84 | se_el_in: is_in … l se_el |
---|
| 85 | }. |
---|
| 86 | |
---|
| 87 | coercion sub_expr : ∀l:list tag. Type[0] → Type[0] |
---|
| 88 | ≝ sub_expr on _l: list tag to Type[0] → Type[0]. |
---|
| 89 | |
---|
| 90 | coercion mk_sub_expr : |
---|
| 91 | ∀l:list tag.∀E.∀e:expr E. |
---|
| 92 | ∀p:is_in ? l e.sub_expr l E |
---|
| 93 | ≝ mk_sub_expr on e:expr ? to sub_expr ? ?. |
---|
| 94 | |
---|
| 95 | let rec sublist (S:DeqSet) (l1:list S) (l2:list S) on l1 : bool ≝ |
---|
| 96 | match l1 with |
---|
| 97 | [ nil ⇒ true |
---|
| 98 | | cons hd tl ⇒ memb S hd l2 ∧ sublist S tl l2 ]. |
---|
| 99 | |
---|
| 100 | lemma sublist_hd_tl_to_memb: |
---|
| 101 | ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2. |
---|
| 102 | sublist S (hd::tl) l2 → memb S hd l2. |
---|
| 103 | #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize // |
---|
| 104 | qed. |
---|
| 105 | |
---|
| 106 | lemma sublist_hd_tl_to_sublist: |
---|
| 107 | ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2. |
---|
| 108 | sublist S (hd::tl) l2 → sublist S tl l2. |
---|
| 109 | #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize // #H cases H |
---|
| 110 | qed. |
---|
| 111 | |
---|
| 112 | lemma sublist_insert_snd_pos: |
---|
| 113 | ∀S:DeqSet. ∀x,y:S. ∀l1,l2:list S. |
---|
| 114 | sublist S l1 (x::l2) → sublist S l1 (x::y::l2). |
---|
| 115 | #S #x #y #l1 elim l1 [//] |
---|
| 116 | #hd #tl #IH #l2 #H |
---|
| 117 | lapply (sublist_hd_tl_to_sublist … H) #K |
---|
| 118 | whd in match (sublist ???); >(?:hd∈x::y::l2 = true) /2/ |
---|
| 119 | lapply (sublist_hd_tl_to_memb … H) normalize cases (hd==x) normalize // |
---|
| 120 | cases (hd==y) normalize // cases (hd∈l2) // #H cases H |
---|
| 121 | qed. |
---|
| 122 | |
---|
| 123 | lemma sublist_tl_hd_tl: |
---|
| 124 | ∀S:DeqSet. ∀hd:S. ∀tl:list S. sublist S tl (hd::tl). |
---|
| 125 | #S #hd #tl elim tl try % |
---|
| 126 | #hd' #tl' #IH whd in match (sublist ???); |
---|
| 127 | whd in match (hd' ∈ hd::?::?); cases (hd'==hd) |
---|
| 128 | whd in match (hd' ∈ ?::?); >(\b ?) try % normalize |
---|
| 129 | lapply (sublist_insert_snd_pos … hd' … IH) |
---|
| 130 | cases (sublist ???) // |
---|
| 131 | qed. |
---|
| 132 | |
---|
| 133 | lemma sublist_refl: ∀S:DeqSet. ∀l: list S. sublist S l l. |
---|
| 134 | #S #l elim l [//] #hd #tl #IH normalize >(\b ?) // |
---|
| 135 | qed. |
---|
| 136 | |
---|
| 137 | let rec sub_expr_elim_type |
---|
| 138 | (E:Type[0]) (fixed_l: list tag) (orig: fixed_l E) |
---|
| 139 | (Q: fixed_l E → Prop) |
---|
| 140 | (l: list tag) |
---|
| 141 | on l : sublist Tag l fixed_l → Prop ≝ |
---|
| 142 | match l return λl. sublist Tag l fixed_l → Prop with |
---|
| 143 | [ nil ⇒ λH. Q orig |
---|
| 144 | | cons hd tl ⇒ λH. |
---|
| 145 | let tail_call ≝ sub_expr_elim_type E fixed_l orig Q tl ? in |
---|
| 146 | match hd return λt. memb Tag t fixed_l → Prop with |
---|
| 147 | [ num ⇒ λH. (∀n. Q (Num … n)) → tail_call |
---|
| 148 | | plus ⇒ λH. (∀x,y. Q (Plus … x y)) → tail_call |
---|
| 149 | | mul ⇒ λH. (∀x,y. Q (Mul … x y)) → tail_call |
---|
| 150 | ] (sublist_hd_tl_to_memb Tag hd tl fixed_l H)]. |
---|
| 151 | /2/ qed. |
---|
| 152 | |
---|
| 153 | lemma sub_expr_elim0: |
---|
| 154 | ∀E:Type[0]. ∀l: list tag. ∀x: l E. ∀Q: l E → Prop. |
---|
| 155 | ∀l',H. |
---|
| 156 | (∀y:l E. ¬ is_in … l' y → Q y) → |
---|
| 157 | sub_expr_elim_type E l x Q l' H. |
---|
| 158 | #E #l #x #Q #l' elim l' /2/ |
---|
| 159 | #hd #tl #IH cases hd #H #INV whd #P0 @IH ** /2/ |
---|
| 160 | qed. |
---|
| 161 | |
---|
| 162 | theorem sub_expr_elim: |
---|
| 163 | ∀E:Type[0]. ∀l: list tag. ∀x: l E. ∀Q: l E → Prop. |
---|
| 164 | sub_expr_elim_type E l x Q l ?. |
---|
| 165 | [2:// |
---|
| 166 | | #E #l #x #Q @sub_expr_elim0 * #y #H #NH |
---|
| 167 | cases (?: False) cases (is_in E l y) in H NH; // |
---|
| 168 | qed. |
---|
| 169 | |
---|
| 170 | (**************************************) |
---|
| 171 | |
---|
| 172 | definition eval_additive_expr: ∀E:Type[0]. (E → nat) → [plus] E → nat ≝ |
---|
| 173 | λE,f,e. |
---|
| 174 | match e return λe. is_in … [plus] e → nat with |
---|
| 175 | [ Plus x y ⇒ λH. f x + f y |
---|
| 176 | | _ ⇒ λH:False. ? |
---|
| 177 | ] (se_el_in ?? e). |
---|
| 178 | elim H qed. |
---|
| 179 | |
---|
| 180 | definition eval_multiplicative_expr: ∀E:Type[0]. (E → nat) → [mul] E → nat ≝ |
---|
| 181 | λE,f,e. |
---|
| 182 | match e return λe. is_in … [mul] e → nat with |
---|
| 183 | [ Mul x y ⇒ λH. f x * f y |
---|
| 184 | | _ ⇒ λH:False. ? |
---|
| 185 | ] (se_el_in ?? e). |
---|
| 186 | elim H qed. |
---|
| 187 | |
---|
| 188 | definition eval_additive_multiplicative_expr: ∀E:Type[0]. (E → nat) → [plus;mul] E → nat ≝ |
---|
| 189 | λE,f,e. |
---|
| 190 | match e return λe. is_in … [plus;mul] e → nat with |
---|
| 191 | [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y) |
---|
| 192 | | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y) |
---|
| 193 | | _ ⇒ λH:False. ? |
---|
| 194 | ] (se_el_in ?? e). |
---|
| 195 | [2,3: % | elim H] |
---|
| 196 | qed. |
---|
| 197 | |
---|
| 198 | definition eval_additive_multiplicative_constant_expr: ∀E:Type[0]. (E → nat) → [plus;mul;num] E → nat ≝ |
---|
| 199 | λE,f,e. |
---|
| 200 | match e return λe. is_in … [plus;mul;num] e → nat with |
---|
| 201 | [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y) |
---|
| 202 | | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y) |
---|
| 203 | | Num n ⇒ λH. n |
---|
| 204 | ] (se_el_in ?? e). |
---|
| 205 | % qed. |
---|
| 206 | |
---|
| 207 | (*CSC: not accepted :-( |
---|
| 208 | inductive expr_no_const : Type[0] ≝ K : [plus;mul] expr_no_const → expr_no_const. |
---|
| 209 | *) |
---|
| 210 | |
---|
| 211 | inductive final_expr : Type[0] ≝ K : expr final_expr → final_expr. |
---|
| 212 | |
---|
| 213 | coercion K. |
---|
| 214 | |
---|
| 215 | let rec eval_final_expr e on e : nat ≝ |
---|
| 216 | match e with |
---|
| 217 | [ K e' ⇒ eval_additive_multiplicative_constant_expr final_expr eval_final_expr e']. |
---|
| 218 | cases e' try #x try #y % |
---|
| 219 | qed. |
---|
| 220 | |
---|
| 221 | example test: eval_final_expr (K (Mul ? (Num ? 2) (Num ? 3))) = 6. |
---|
| 222 | % qed. |
---|