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 | *) |
---|