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

Last change on this file since 2403 was 2403, checked in by sacerdot, 9 years ago

More work, example almost finished up to recursive type.

File size: 2.3 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
53(**************************************)
54
55definition eval_additive_expr: ∀E:Type[0]. (E → nat) → [plus] E → nat ≝
56 λE,f,e.
57  match e return λe. is_in … [plus] e → nat with
58  [ Plus x y ⇒ λH. f x + f y
59  | _ ⇒ λH:False. ?
60  ] (se_el_in ?? e).
61elim H qed.
62
63definition eval_multiplicative_expr: ∀E:Type[0]. (E → nat) → [mul] E → nat ≝
64 λE,f,e.
65  match e return λe. is_in … [mul] e → nat with
66  [ Mul x y ⇒ λH. f x + f y
67  | _ ⇒ λH:False. ?
68  ] (se_el_in ?? e).
69elim H qed.
70
71definition eval_additive_multiplicative_expr: ∀E:Type[0]. (E → nat) → [plus;mul] E → nat ≝
72 λE,f,e.
73  match e return λe. is_in … [plus;mul] e → nat with
74  [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y)
75  | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y)
76  | _ ⇒ λH:False. ?
77  ] (se_el_in ?? e).
78[2,3: % | elim H]
79qed.
Note: See TracBrowser for help on using the repository browser.