Changeset 2514 for Papers/polymorphicvariants2012/test.ma
 Timestamp:
 Dec 2, 2012, 4:40:41 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/polymorphicvariants2012/test.ma
r2406 r2514 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]. 1 include "infrastructure.ma". 7 2 8 3 inductive expr (E: Type[0]) : Type[0] ≝ … … 11 6  Mul : E > E > expr E. 12 7 13 inductive tag : Type[0] := num : tag  plus : tag  mul : tag.8 inductive tag_ : Type[0] := num : tag_  plus : tag_  mul : tag_. 14 9 15 definition eq_tag : tag > tag> bool :=10 definition eq_tag : tag_ > tag_ > bool := 16 11 λt1,t2. 17 12 match t1 with … … 20 15  mul => match t2 with [mul => true  _ => false]]. 21 16 22 definition Tag : DeqSet ≝ mk_DeqSet tageq_tag ?.17 definition tag : DeqSet ≝ mk_DeqSet tag_ eq_tag ?. 23 18 ** normalize /2/ % #abs destruct 24 19 qed. … … 31 26  Mul _ _ => mul ]. 32 27 33 (*definition is_a : ∀E: Type[0]. tag > expr E > Prop ≝ 34 λE,t,e. eq_tag t (tag_of_expr \ldots e).*) 28 (* 29 definition Q_holds_for_tag: 30 ∀E:Type[0]. ∀l: list tag. ∀Q: ∀x: l E → Prop. ∀t:tag. memb … t l → Prop ≝ 31 λE,l,Q,t. ?. 32 match t return λt. memb … t l → Prop with 33 [ num ⇒ λH. (∀n. Q (Num … n)) 34  plus ⇒ λH. (∀x,y. Q (Plus … x y)) 35  mul ⇒ λH. (∀x,y. Q (Mul … x y)) 36 ]. 35 37 36 definition is_in : ∀E: Type[0]. list tag > expr E > bool ≝37 λE,l,e. memb Tag (tag_of_expr ? e) l.38 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 }. 39 definition Q_holds_for_tag: 40 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀t:tag. memb … t l → Prop ≝ 41 λE,l,Q,t. ?. 42 match t return λt. memb … t l → Prop with 43 [ num ⇒ λH. (∀n. Q (Num … n)) 44  plus ⇒ λH. (∀x,y. Q (Plus … x y)) 45  mul ⇒ λH. (∀x,y. Q (Mul … x y)) 46 ]. 44 47 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 lemma sublist_insert_snd_pos: 71 ∀S:DeqSet. ∀x,y:S. ∀l1,l2:list S. 72 sublist S l1 (x::l2) → sublist S l1 (x::y::l2). 73 #S #x #y #l1 elim l1 [//] 74 #hd #tl #IH #l2 #H 75 lapply (sublist_hd_tl_to_sublist … H) #K 76 whd in match (sublist ???); >(?:hd∈x::y::l2 = true) /2/ 77 lapply (sublist_hd_tl_to_memb … H) normalize cases (hd==x) normalize // 78 cases (hd==y) normalize // cases (hd∈l2) // #H cases H 79 qed. 80 81 lemma sublist_tl_hd_tl: 82 ∀S:DeqSet. ∀hd:S. ∀tl:list S. sublist S tl (hd::tl). 83 #S #hd #tl elim tl try % 84 #hd' #tl' #IH whd in match (sublist ???); 85 whd in match (hd' ∈ hd::?::?); cases (hd'==hd) 86 whd in match (hd' ∈ ?::?); >(\b ?) try % normalize 87 lapply (sublist_insert_snd_pos … hd' … IH) 88 cases (sublist ???) // 89 qed. 90 91 lemma sublist_refl: ∀S:DeqSet. ∀l: list S. sublist S l l. 92 #S #l elim l [//] #hd #tl #IH normalize >(\b ?) // 93 qed. 94 95 let rec sub_expr_elim_type 96 (E:Type[0]) (fixed_l: list tag) (orig: fixed_l E) 97 (Q: fixed_l E → Prop) 98 (l: list tag) 99 on l : sublist Tag l fixed_l → Prop ≝ 100 match l return λl. sublist Tag l fixed_l → Prop with 101 [ nil ⇒ λH. Q orig 102  cons hd tl ⇒ λH. 103 let tail_call ≝ sub_expr_elim_type E fixed_l orig Q tl ? in 104 match hd return λt. memb Tag t fixed_l → Prop with 105 [ num ⇒ λH. (∀n. Q (Num … n)) → tail_call 106  plus ⇒ λH. (∀x,y. Q (Plus … x y)) → tail_call 107  mul ⇒ λH. (∀x,y. Q (Mul … x y)) → tail_call 108 ] (sublist_hd_tl_to_memb Tag hd tl fixed_l H)]. 109 /2/ qed. 110 111 lemma sub_expr_elim0: 112 ∀E:Type[0]. ∀l: list tag. ∀x: l E. ∀Q: l E → Prop. 113 ∀l',H. 114 (∀y:l E. ¬ is_in … l' y → Q y) → 115 sub_expr_elim_type E l x Q l' H. 116 #E #l #x #Q #l' elim l' /2/ 117 #hd #tl #IH cases hd #H #INV whd #P0 @IH ** /2/ 118 qed. 119 120 theorem sub_expr_elim: 121 ∀E:Type[0]. ∀l: list tag. ∀x: l E. ∀Q: l E → Prop. 122 sub_expr_elim_type E l x Q l ?. 123 [2:// 124  #E #l #x #Q @sub_expr_elim0 * #y #H #NH 125 cases (?: False) cases (is_in E l y) in H NH; // 126 qed. 127 128 (**************************************) 129 130 definition eval_additive_expr: ∀E:Type[0]. (E → nat) → [plus] E → nat ≝ 131 λE,f,e. 132 match e return λe. is_in … [plus] e → nat with 133 [ Plus x y ⇒ λH. f x + f y 134  _ ⇒ λH:False. ? 135 ] (se_el_in ?? e). 136 elim H qed. 137 138 definition eval_multiplicative_expr: ∀E:Type[0]. (E → nat) → [mul] E → nat ≝ 139 λE,f,e. 140 match e return λe. is_in … [mul] e → nat with 141 [ Mul x y ⇒ λH. f x * f y 142  _ ⇒ λH:False. ? 143 ] (se_el_in ?? e). 144 elim H qed. 145 146 definition eval_additive_multiplicative_expr: ∀E:Type[0]. (E → nat) → [plus;mul] E → nat ≝ 147 λE,f,e. 148 match e return λe. is_in … [plus;mul] e → nat with 149 [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y) 150  Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y) 151  _ ⇒ λH:False. ? 152 ] (se_el_in ?? e). 153 [2,3: %  elim H] 154 qed. 155 156 definition eval_additive_multiplicative_constant_expr: ∀E:Type[0]. (E → nat) → [plus;mul;num] E → nat ≝ 157 λE,f,e. 158 match e return λe. is_in … [plus;mul;num] e → nat with 159 [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y) 160  Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y) 161  Num n ⇒ λH. n 162 ] (se_el_in ?? e). 163 % qed. 164 165 (*CSC: not accepted :( 166 inductive expr_no_const : Type[0] ≝ K : [plus;mul] expr_no_const → expr_no_const. 48 axiom Q_holds_for_tag_spec: 49 ∀E:Type[0]. ∀fixed_l: list tag. ∀Q: fixed_l E → Prop. ∀t:tag. 50 ∀p:memb … t fixed_l. Q_holds_for_tag … Q … p → 51 ∀x: [t] E. Q x. 167 52 *) 168 169 inductive final_expr : Type[0] ≝ K : expr final_expr → final_expr.170 171 coercion K.172 173 let rec eval_final_expr e on e : nat ≝174 match e with175 [ K e' ⇒ eval_additive_multiplicative_constant_expr final_expr eval_final_expr e'].176 cases e' try #x try #y %177 qed.178 179 example test: eval_final_expr (K (Mul ? (Num ? 2) (Num ? 3))) = 6.180 % qed.
Note: See TracChangeset
for help on using the changeset viewer.