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

Last change on this file since 2400 was 2400, checked in by sacerdot, 8 years ago

Some tests.

File size: 1.4 KB
Line 
1include "basics/lists/listb.ma".
2
3definition bool_to_Prop : bool → Prop ≝
4 λb. match b with [ true ⇒ True | false ⇒ False ].
5
6inductive expr (E: Type[0]) : Type[0] ≝
7   Num : nat -> expr E
8 | Plus : expr E -> expr E -> expr E
9 | Mul : expr E -> expr E -> expr E.
10
11inductive tag : Type[0] := num : tag | plus : tag | mul : tag.
12
13definition eq_tag : tag -> tag -> bool :=
14 λt1,t2.
15  match t1 with
16  [ num => match t2 with [num => true | _ => false]
17  | plus => match t2 with [plus => true | _ => false]
18  | mul => match t2 with [mul => true | _ => false]].
19
20definition Tag : DeqSet ≝ mk_DeqSet tag eq_tag ?.
21 ** normalize /2/ % #abs destruct
22qed.
23
24definition tag_of_expr : ∀E:Type[0]. expr E -> tag :=
25 λE,e.
26   match e with
27   [ Num _ => num
28   | Plus _ _ => plus
29   | Mul _ _ => mul ].
30
31(*definition is_a : ∀E: Type[0]. tag -> expr E -> Prop ≝
32 λE,t,e. eq_tag t (tag_of_expr \ldots e).*)
33
34definition is_in : ∀E: Type[0]. list tag -> expr E -> bool ≝
35 λE,l,e. memb Tag (tag_of_expr ? e) l.
36
37record sub_expr (E: Type[0]) (l: list tag) : Type[0] ≝
38{
39  se_el :> expr E;
40  se_el_in: bool_to_Prop (is_in … l se_el)
41}.
42
43coercion sub_expr : ∀E:Type[0].∀l:list tag .Type[0]
44 ≝ sub_expr on _l: list tag to Type[0].
45
46coercion mk_sub_expr :
47 ∀E.∀l:list tag.∀e:expr E.
48  ∀p:bool_to_Prop (is_in ? l e).sub_expr E l
49 ≝ mk_sub_expr on e:expr E to sub_expr ? ?.
50
51(**************************************)
52
53definition additive_expr : Type[0] ≝ [plus].
Note: See TracBrowser for help on using the repository browser.