source: Papers/polymorphic-variants-2012/variants.ma @ 2520

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

Now it is nice!

File size: 3.7 KB
Line 
1(*
2include "infrastructure.ma".
3axiom tag: DeqSet.
4axiom expr: Type[0] → Type[0].
5axiom tag_of_expr: ∀E:Type[0]. expr E → tag.
6axiom Q_holds_for_tag: ∀E:Type[0]. ∀Q: expr E → Prop. ∀t:tag. Prop.
7axiom Q_holds_for_tag_spec:
8 ∀E:Type[0]. ∀Q: expr E → Prop.
9  ∀x: expr E. Q_holds_for_tag … Q … (tag_of_expr … x) → Q x.
10*)
11
12include "test.ma".
13
14definition is_in : ∀E: Type[0]. list tag -> expr E -> bool ≝
15 λE,l,e. memb … (tag_of_expr ? e) l.
16
17record sub_expr (l: list tag) (E: Type[0]) : Type[0] ≝
18{
19  se_el :> expr E;
20  se_el_in: is_in … l se_el
21}.
22
23coercion sub_expr : ∀l:list tag. Type[0] → Type[0]
24 ≝ sub_expr on _l: list tag to Type[0] → Type[0].
25
26coercion mk_sub_expr :
27 ∀l:list tag.∀E.∀e:expr E.
28  ∀p:is_in ? l e.sub_expr l E
29 ≝ mk_sub_expr on e:expr ? to sub_expr ? ?.
30
31definition Q_of_Q':
32 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. expr E → Prop ≝
33 λE,l,Q,e.
34  match memb … (tag_of_expr … e) l return λx. memb … (tag_of_expr … e) l = x → Prop with
35  [ true ⇒ λH. Q e
36  | false ⇒ λH. False
37  ] (refl …).
38whd in match (is_in ???); >H //
39qed.
40
41lemma dep_bool_match_elim :
42∀b.∀B : Type[0].∀P : B → Prop.∀Q : bool → Prop.
43∀c1,c2.
44(∀prf : Q true.P (c1 prf)) →
45(∀prf : Q false.P (c2 prf)) →
46∀prf : Q b.
47P (match b return λx.Q x → B with [ true ⇒ λprf.c1 prf | false ⇒ λprf.c2 prf ] prf).
48* // qed.
49
50lemma Q_of_Q_ok':
51 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀x:l E.
52  Q_of_Q' E l Q x→Q x.
53 #E #l #Q #x normalize
54 @(dep_bool_match_elim (tag_of_expr E x ∈ l)) [2: #_ *]
55 cases x #y #prf' #prf'' #H @H
56qed.
57 
58definition Q_holds_for_tag':
59 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀t:tag. memb … t l → Prop ≝
60 λE,l,Q',t,p.
61  Q_holds_for_tag E (Q_of_Q' … l Q') t.
62
63theorem Q_holds_for_tag_spec':
64 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀t:tag.
65  ∀p:memb … t l. Q_holds_for_tag' … Q … p →
66   ∀x: [t] E. Q x.
67[2: cases x #y #H @(memb_to_sublist_to_memb … H) whd in match (sublist ???);
68    cases (memb ???) in p; //
69| #E #l #Q #t #p whd in match Q_holds_for_tag'; normalize nodelta #H #x
70  cut (t = tag_of_expr … x)
71  [ cases x -x #x #EQ whd in EQ; inversion (is_in E [t] x) in EQ;
72    normalize nodelta
73    [2: #_ #abs cases abs] whd in ⊢ (??%? → ? → ?);
74    inversion (tag_of_expr E x == t) [2: #_ normalize #abs destruct]
75    #EQ #_ #_ <(\P EQ) %
76  | #EQ2 lapply H >EQ2 in ⊢ (% → ?); #K lapply(Q_holds_for_tag_spec … K)
77    cut (tag_of_expr E x ∈ l) // #K1 #K2 @(Q_of_Q_ok' E l Q x)
78    cases x in K2; // ]]
79qed.
80
81let rec sub_expr_elim_type
82 (E:Type[0]) (fixed_l: list tag) (orig: fixed_l E)
83 (Q: fixed_l E → Prop)
84 (l: list tag)
85 on l : sublist … l fixed_l → Prop ≝
86 match l return λl. sublist … l fixed_l → Prop with
87 [ nil ⇒ λH. Q orig
88 | cons hd tl ⇒ λH.
89    let tail_call ≝ sub_expr_elim_type E fixed_l orig Q tl ? in
90     Q_holds_for_tag' … fixed_l Q hd (sublist_hd_tl_to_memb … hd tl fixed_l H) →
91      tail_call ].
92/2/ qed.
93
94lemma sub_expr_elim0:
95 ∀E:Type[0]. ∀l: list tag. ∀x: l E. ∀Q: l E → Prop.
96  ∀l',H.
97   (∀y:l E. ¬ is_in … l' y → Q y) →
98    sub_expr_elim_type E l x Q l' H.
99 #E #l #x #Q #l' elim l' /2/
100 #hd #tl #IH (*cases hd*) #H #INV whd #P0 @IH #y
101 whd in match (is_in ???) in INV:%;
102 lapply (Q_holds_for_tag_spec' … P0) #K1 #K2
103 inversion (tag_of_expr … y == hd) #K3
104 [ lapply (K1 y)
105   [ whd in match (is_in ???); >K3 %
106   | cases y in K3; // ]
107 | @INV whd in match (is_in ???); >K3 // ]
108qed.
109
110theorem sub_expr_elim:
111 ∀E:Type[0]. ∀l: list tag. ∀x: l E. ∀Q: l E → Prop.
112  sub_expr_elim_type E l x Q l ?.
113[2://
114| #E #l #x #Q @sub_expr_elim0 * #y #H #NH
115  cases (?: False) cases (is_in E l y) in H NH; //
116qed.
Note: See TracBrowser for help on using the repository browser.