source: Papers/polymorphic-variants-2012/test.ma @ 2410

Last change on this file since 2410 was 2406, checked in by sacerdot, 7 years ago

Elimination principle committed.

File size: 5.5 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
8inductive expr (E: Type[0]) : Type[0] ≝
9   Num : nat -> expr E
10 | Plus : E -> E -> expr E
11 | Mul : E -> E -> expr E.
12
13inductive tag : Type[0] := num : tag | plus : tag | mul : tag.
14
15definition 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
22definition Tag : DeqSet ≝ mk_DeqSet tag eq_tag ?.
23 ** normalize /2/ % #abs destruct
24qed.
25
26definition 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
36definition is_in : ∀E: Type[0]. list tag -> expr E -> bool ≝
37 λE,l,e. memb Tag (tag_of_expr ? e) l.
38
39record 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
45coercion sub_expr : ∀l:list tag. Type[0] → Type[0]
46 ≝ sub_expr on _l: list tag to Type[0] → Type[0].
47
48coercion 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
53let 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 
58lemma 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 //
62qed.
63
64lemma 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
68qed.
69
70lemma 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
79qed.
80
81lemma 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 ???) //
89qed.
90
91lemma sublist_refl: ∀S:DeqSet. ∀l: list S. sublist S l l.
92 #S #l elim l [//] #hd #tl #IH normalize >(\b ?) //
93qed.
94
95let 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
111lemma 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/
118qed.
119
120theorem 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; //
126qed.
127
128(**************************************)
129
130definition 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).
136elim H qed.
137
138definition 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).
144elim H qed.
145
146definition 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]
154qed.
155
156definition 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 :-(
166inductive expr_no_const : Type[0] ≝ K : [plus;mul] expr_no_const → expr_no_const.
167*)
168
169inductive final_expr : Type[0] ≝ K : expr final_expr → final_expr.
170
171coercion K.
172
173let rec eval_final_expr e on e : nat ≝
174 match e with
175 [ K e' ⇒ eval_additive_multiplicative_constant_expr final_expr eval_final_expr e'].
176cases e' try #x try #y %
177qed.
178
179example test: eval_final_expr (K (Mul ? (Num ? 2) (Num ? 3))) = 6.
180% qed.
Note: See TracBrowser for help on using the repository browser.