source: Papers/polymorphic-variants-2012/test3.ma @ 3454

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

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

File size: 4.1 KB
Line 
1include "infrastructure.ma".
2
3inductive tag : Type[0] := a : tag | b : tag | c : tag.
4
5definition tags : list tag ≝ [a;b;c].
6
7definition type_of_tag : ∀T:Type[0]. tag → Type[0] ≝
8 λT,t. match t with [ a ⇒ T | b ⇒ nat | c ⇒ bool ].
9
10record test (T:Type[0]) : Type[0] ≝
11 { A_:option (type_of_tag T a); B_: option (type_of_tag T b); C_: option (type_of_tag T c) }.
12
13definition mk_test ≝ mk_test.
14
15definition proj_of_tag: ∀t:tag. ∀T:Type[0]. test T → option (type_of_tag T t) ≝
16 λt. match t with [ a ⇒ A_ | b ⇒ B_ | c ⇒ C_ ].
17
18definition eq_tag : tag → tag → bool ≝
19 λt1,t2.
20  match t1 with
21  [ a ⇒ match t2 with [a => true | _ => false]
22  | b ⇒ match t2 with [b => true | _ => false]
23  | c ⇒ match t2 with [c => true | _ => false]].
24
25definition Tag : DeqSet ≝ mk_DeqSet tag eq_tag ?.
26 ** normalize /2/ % #abs destruct
27qed.
28
29record sub_test (l: list tag) (T: Type[0]) : Type[0] ≝
30{
31  st_el :> test T;
32  st_el_in: for_each ? (λt. defined … (proj_of_tag t … st_el)) l
33}.
34
35coercion sub_test : ∀l:list tag. Type[0] → Type[0]
36 ≝ sub_test on _l: list tag to Type[0] → Type[0].
37
38(*
39coercion mk_sub_expr :
40 ∀l:list tag.∀E.∀e:expr E.
41  ∀p:is_in ? l e.sub_expr l E
42 ≝ mk_sub_expr on e:expr ? to sub_expr ? ?.
43*)
44
45definition proj:
46 ∀t:tag. ∀l:list tag. memb Tag t l → ∀T:Type[0]. l T → type_of_tag T t
47
48 λt,l,H,T,r.
49  match proj_of_tag t … r return λr. defined ? r → type_of_tag T t with
50  [ None ⇒ λH:False.?
51  | Some v ⇒ λH:True.v] ?.
52[2: cases H
53| lapply (st_el_in …r) inversion (for_each ???) [2: #_ #abs cases abs]
54  #K #_ lapply (for_each_to_memb_to_true ???? H K) #X >X %]
55qed.
56
57definition A: ∀l:list tag. memb Tag a l → ∀T:Type[0]. l T → T ≝ proj a.
58definition B: ∀l:list tag. memb Tag b l → ∀T:Type[0]. l T → nat ≝ proj b.
59definition C: ∀l:list tag. memb Tag c l → ∀T:Type[0]. l T → bool ≝ proj c.
60
61let rec type_of_build_test0 (tags: list tag) (l:list tag) (T:Type[0]) on tags: Type[0] ≝
62 match tags with
63 [ nil ⇒ l T
64 | cons hd tl ⇒
65    if memb Tag hd l then
66     (type_of_tag T hd → type_of_build_test0 tl l T)
67    else
68     type_of_build_test0 tl l T ].
69
70definition type_of_build_test: list tag → Type[0] → Type[0] ≝
71 type_of_build_test0 tags.
72
73let rec type_of_mk_test0 (tags: list tag) (T:Type[0]) on tags: Type[0] ≝
74 match tags with
75 [ nil ⇒ test T
76 | cons hd tl ⇒ option (type_of_tag T hd) → type_of_mk_test0 tl T].
77
78let rec mk_test0_ok (tags: list tag) (l:list tag) (T:Type[0]) on tags :
79 type_of_mk_test0 tags T → Prop ≝
80 match tags return λtags.type_of_mk_test0 tags T → Prop with
81 [ nil ⇒ λr:test T. bool_to_Prop (for_each ? (λt. defined … (proj_of_tag t … r)) l)
82 | cons hd tl ⇒ λr:option (type_of_tag T hd) → type_of_mk_test0 tl T.
83    if memb Tag hd l then
84     ∀x:type_of_tag T hd. mk_test0_ok tl l T (r (Some … x))
85    else
86     mk_test0_ok tl l T (r (None …))
87 ].
88
89let rec build_test0 (tags: list tag) (l:list tag) (T:Type[0]) on tags :
90 ∀mk_record:type_of_mk_test0 tags T.
91  mk_test0_ok tags l T mk_record → type_of_build_test0 tags l T
92
93 match tags
94  return λtags.
95   ∀mk_record:type_of_mk_test0 tags T.
96    mk_test0_ok tags l T mk_record → type_of_build_test0 tags l T
97 with
98 [ nil ⇒ λr,r_ok.?
99 | cons hd tl ⇒ λmk_record,mk_record_ok.
100    match memb Tag hd l return λb. b=memb Tag hd l → if b then ? else ? with
101    [ true ⇒ λH.λv. build_test0 tl l T (mk_record (Some ? v)) ?
102    | false ⇒ λH.build_test0 tl l T (mk_record (None …)) ?] (refl … (memb Tag hd l))].
103[ %{r} @r_ok
104|2,3: whd in mk_record_ok; <H in mk_record_ok; // ]
105qed.
106
107 (*CSC: This needs to be proved every time :-( *)
108axiom mk_test_ok: ∀l: list tag. ∀T:Type[0]. mk_test0_ok tags l T (mk_test T).
109
110definition build_test: ∀l:list tag. ∀T:Type[0]. type_of_build_test l T ≝
111 λl,T. build_test0 tags l T (mk_test …) ?.
112// qed.
113
114example xxx: [a; c] True ≝ build_test [a;c] … I true.
115example xxx_c: C … xxx = true. // qed.
116(*CSC: here we need a lemma! *)
117example xxx_sub: [a;b] True → [a] True.
118 #x %{x} cases x #y whd in ⊢ (% → %); whd in match (for_each ???);
119 cases (for_each ???) [#X @X | #X cases X]
120qed.
Note: See TracBrowser for help on using the repository browser.