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

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

All .ma files committed: some of them are just in-progress.

File size: 1.5 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
28(*
29definition 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
39definition 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
48axiom 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*)
Note: See TracBrowser for help on using the repository browser.