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

Last change on this file since 2552 was 2520, checked in by sacerdot, 7 years ago

Now it is nice!

File size: 1.1 KB
Line 
1include "infrastructure.ma".
2
3inductive expr (E: Type[0]) : Type[0] ≝
4   Num : nat -> expr E
5 | Plus : E -> E -> expr E
6 | Mul : E -> E -> expr E.
7
8inductive tag_ : Type[0] := num : tag_ | plus : tag_ | mul : tag_.
9
10definition 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
17definition tag : DeqSet ≝ mk_DeqSet tag_ eq_tag ?.
18 ** normalize /2/ % #abs destruct
19qed.
20
21definition 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
28definition 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
37theorem 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 //
41qed.
Note: See TracBrowser for help on using the repository browser.