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

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

Type of elimination principle generated + more lemmas.

File size: 4.2 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
70let 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
90definition 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).
96elim H qed.
97
98definition 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).
104elim H qed.
105
106definition 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]
114qed.
115
116definition 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 :-(
126inductive expr_no_const : Type[0] ≝ K : [plus;mul] expr_no_const → expr_no_const.
127*)
128
129inductive final_expr : Type[0] ≝ K : expr final_expr → final_expr.
130
131coercion K.
132
133let 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'].
136cases e' try #x try #y %
137qed.
138
139example test: eval_final_expr (K (Mul ? (Num ? 2) (Num ? 3))) = 6.
140% qed.
Note: See TracBrowser for help on using the repository browser.