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 | inductive expr (E: Type[0]) : Type[0] ≝ |
---|
7 | Num : nat -> expr E |
---|
8 | | Plus : expr E -> expr E -> expr E |
---|
9 | | Mul : expr E -> expr E -> expr E. |
---|
10 | |
---|
11 | inductive tag : Type[0] := num : tag | plus : tag | mul : tag. |
---|
12 | |
---|
13 | definition eq_tag : tag -> tag -> bool := |
---|
14 | λt1,t2. |
---|
15 | match t1 with |
---|
16 | [ num => match t2 with [num => true | _ => false] |
---|
17 | | plus => match t2 with [plus => true | _ => false] |
---|
18 | | mul => match t2 with [mul => true | _ => false]]. |
---|
19 | |
---|
20 | definition Tag : DeqSet ≝ mk_DeqSet tag eq_tag ?. |
---|
21 | ** normalize /2/ % #abs destruct |
---|
22 | qed. |
---|
23 | |
---|
24 | definition tag_of_expr : ∀E:Type[0]. expr E -> tag := |
---|
25 | λE,e. |
---|
26 | match e with |
---|
27 | [ Num _ => num |
---|
28 | | Plus _ _ => plus |
---|
29 | | Mul _ _ => mul ]. |
---|
30 | |
---|
31 | (*definition is_a : ∀E: Type[0]. tag -> expr E -> Prop ≝ |
---|
32 | λE,t,e. eq_tag t (tag_of_expr \ldots e).*) |
---|
33 | |
---|
34 | definition is_in : ∀E: Type[0]. list tag -> expr E -> bool ≝ |
---|
35 | λE,l,e. memb Tag (tag_of_expr ? e) l. |
---|
36 | |
---|
37 | record sub_expr (l: list tag) (E: Type[0]) : Type[0] ≝ |
---|
38 | { |
---|
39 | se_el :> expr E; |
---|
40 | se_el_in: bool_to_Prop (is_in … l se_el) |
---|
41 | }. |
---|
42 | |
---|
43 | coercion sub_expr : ∀l:list tag. Type[0] → Type[0] |
---|
44 | ≝ sub_expr on _l: list tag to Type[0] → Type[0]. |
---|
45 | |
---|
46 | coercion mk_sub_expr : |
---|
47 | ∀l:list tag.∀E.∀e:expr E. |
---|
48 | ∀p:bool_to_Prop (is_in ? l e).sub_expr l E |
---|
49 | ≝ mk_sub_expr on e:expr E to sub_expr ? ?. |
---|
50 | |
---|
51 | (**************************************) |
---|
52 | |
---|
53 | definition additive_expr : Type[0] → Type[0] ≝ λE. [plus] E. |
---|