Line | |
---|

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 | definition Q_holds_for_tag: |
---|

29 | ∀E:Type[0]. ∀Q: expr E → Prop. ∀t:tag. Prop ≝ |
---|

30 | λE,Q,t. |
---|

31 | match t with |
---|

32 | [ num ⇒ ∀n. Q (Num … n) |
---|

33 | | plus ⇒ ∀x,y. Q (Plus … x y) |
---|

34 | | mul ⇒ ∀x,y. Q (Mul … x y) |
---|

35 | ]. |
---|

36 | |
---|

37 | theorem Q_holds_for_tag_spec: |
---|

38 | ∀E:Type[0]. ∀Q: expr E → Prop. |
---|

39 | ∀x: expr E. Q_holds_for_tag … Q … (tag_of_expr … x) → Q x. |
---|

40 | #E #Q * normalize // |
---|

41 | qed. |
---|

**Note:** See

TracBrowser
for help on using the repository browser.