source: Papers/polymorphic-variants-2012/test2.ma @ 3418

Last change on this file since 3418 was 2514, checked in by sacerdot, 7 years ago

All .ma files committed: some of them are just in-progress.

File size: 6.4 KB
Line 
1include "basics/lists/listb.ma".
2
3definition bool_to_Prop : bool → Prop ≝
4 λb. match b with [ true ⇒ True | false ⇒ False ].
5
6coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
7
8record test (A:Type[0]) (B:Type[0]) (C:Type[0]) : Type[0] ≝
9 { a:A; b:B; c:C }.
10
11inductive tag : Type[0] := a : tag | b : tag | c : tag.
12
13definition tag_of_pos : nat → tag ≝
14 λn. if eqb n 0 then a else if eqb n 1 then b else c.
15
16definition type_of_tag : tag → Type[0] ≝
17 λt.
18  match t with
19  [ a ⇒ nat
20  | b ⇒ bool
21  | c ⇒ nat ].
22
23definition 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
30definition Tag : DeqSet ≝ mk_DeqSet tag eq_tag ?.
31 ** normalize /2/ % #abs destruct
32qed.
33
34let rec Types (n:nat) on n : Type[1] ≝
35 match n with
36 [ O ⇒ Type[0]
37 | S m ⇒ Type[0] → Types m ].
38
39let 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
49definition record_ty : list tag → Type[0] ≝
50 λl. record_ty0 l 3 test.
51
52coercion record_ty : ∀l:list tag. Type[0]
53 ≝ record_ty on _l: list tag to Type[0].
54 
55XXX
56
57let rec mk_record_ty (l: list tag) (n:nat) on n : Type[0] ≝
58 match n with
59 [ O ⇒ l
60 |
61 ].
62
63let 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
68definition 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
78definition is_in : ∀E: Type[0]. list tag -> expr E -> bool ≝
79 λE,l,e. memb Tag (tag_of_expr ? e) l.
80
81record 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
87coercion sub_expr : ∀l:list tag. Type[0] → Type[0]
88 ≝ sub_expr on _l: list tag to Type[0] → Type[0].
89
90coercion 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
95let 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 
100lemma 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 //
104qed.
105
106lemma 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
110qed.
111
112lemma 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
121qed.
122
123lemma 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 ???) //
131qed.
132
133lemma sublist_refl: ∀S:DeqSet. ∀l: list S. sublist S l l.
134 #S #l elim l [//] #hd #tl #IH normalize >(\b ?) //
135qed.
136
137let 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
153lemma 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/
160qed.
161
162theorem 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; //
168qed.
169
170(**************************************)
171
172definition 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).
178elim H qed.
179
180definition 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).
186elim H qed.
187
188definition 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]
196qed.
197
198definition 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 :-(
208inductive expr_no_const : Type[0] ≝ K : [plus;mul] expr_no_const → expr_no_const.
209*)
210
211inductive final_expr : Type[0] ≝ K : expr final_expr → final_expr.
212
213coercion K.
214
215let 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'].
218cases e' try #x try #y %
219qed.
220
221example test: eval_final_expr (K (Mul ? (Num ? 2) (Num ? 3))) = 6.
222% qed.
Note: See TracBrowser for help on using the repository browser.