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

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

Extensible records implemented via option type.
One axiom left.

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