1 | include "infrastructure.ma". |
---|
2 | |
---|
3 | inductive expr (E: Type[0]) : Type[0] ≝ |
---|
4 | Num : nat -> expr E |
---|
5 | | Plus : E -> E -> expr E |
---|
6 | | Mul : E -> E -> expr E. |
---|
7 | |
---|
8 | inductive tag_ : Type[0] := num : tag_ | plus : tag_ | mul : tag_. |
---|
9 | |
---|
10 | definition eq_tag : tag_ -> tag_ -> bool := |
---|
11 | λt1,t2. |
---|
12 | match t1 with |
---|
13 | [ num => match t2 with [num => true | _ => false] |
---|
14 | | plus => match t2 with [plus => true | _ => false] |
---|
15 | | mul => match t2 with [mul => true | _ => false]]. |
---|
16 | |
---|
17 | definition tag : DeqSet ≝ mk_DeqSet tag_ eq_tag ?. |
---|
18 | ** normalize /2/ % #abs destruct |
---|
19 | qed. |
---|
20 | |
---|
21 | definition tag_of_expr : ∀E:Type[0]. expr E -> tag := |
---|
22 | λE,e. |
---|
23 | match e with |
---|
24 | [ Num _ => num |
---|
25 | | Plus _ _ => plus |
---|
26 | | Mul _ _ => mul ]. |
---|
27 | |
---|
28 | (* |
---|
29 | definition Q_holds_for_tag: |
---|
30 | ∀E:Type[0]. ∀l: list tag. ∀Q: ∀x: l E → Prop. ∀t:tag. memb … t l → Prop ≝ |
---|
31 | λE,l,Q,t. ?. |
---|
32 | match t return λt. memb … t l → Prop with |
---|
33 | [ num ⇒ λH. (∀n. Q (Num … n)) |
---|
34 | | plus ⇒ λH. (∀x,y. Q (Plus … x y)) |
---|
35 | | mul ⇒ λH. (∀x,y. Q (Mul … x y)) |
---|
36 | ]. |
---|
37 | |
---|
38 | |
---|
39 | definition Q_holds_for_tag: |
---|
40 | ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀t:tag. memb … t l → Prop ≝ |
---|
41 | λE,l,Q,t. ?. |
---|
42 | match t return λt. memb … t l → Prop with |
---|
43 | [ num ⇒ λH. (∀n. Q (Num … n)) |
---|
44 | | plus ⇒ λH. (∀x,y. Q (Plus … x y)) |
---|
45 | | mul ⇒ λH. (∀x,y. Q (Mul … x y)) |
---|
46 | ]. |
---|
47 | |
---|
48 | axiom Q_holds_for_tag_spec: |
---|
49 | ∀E:Type[0]. ∀fixed_l: list tag. ∀Q: fixed_l E → Prop. ∀t:tag. |
---|
50 | ∀p:memb … t fixed_l. Q_holds_for_tag … Q … p → |
---|
51 | ∀x: [t] E. Q x. |
---|
52 | *) |
---|