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

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

Generic stuff moved to infrastructure.

File size: 3.4 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 Q_of_Q_ok':
42 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀x:l E.
43  Q_of_Q' E l Q x→Q x.
44 #E #l #Q #x normalize
45 @(dep_bool_match_elim (tag_of_expr E x ∈ l)) [2: #_ *]
46 cases x #y #prf' #prf'' #H @H
47qed.
48 
49definition Q_holds_for_tag':
50 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀t:tag. memb … t l → Prop ≝
51 λE,l,Q',t,p.
52  Q_holds_for_tag E (Q_of_Q' … l Q') t.
53
54theorem Q_holds_for_tag_spec':
55 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀t:tag.
56  ∀p:memb … t l. Q_holds_for_tag' … Q … p →
57   ∀x: [t] E. Q x.
58[2: cases x #y #H @(memb_to_sublist_to_memb … H) whd in match (sublist ???);
59    cases (memb ???) in p; //
60| #E #l #Q #t #p whd in match Q_holds_for_tag'; normalize nodelta #H #x
61  cut (t = tag_of_expr … x)
62  [ cases x -x #x #EQ whd in EQ; inversion (is_in E [t] x) in EQ;
63    normalize nodelta
64    [2: #_ #abs cases abs] whd in ⊢ (??%? → ? → ?);
65    inversion (tag_of_expr E x == t) [2: #_ normalize #abs destruct]
66    #EQ #_ #_ <(\P EQ) %
67  | #EQ2 lapply H >EQ2 in ⊢ (% → ?); #K lapply(Q_holds_for_tag_spec … K)
68    cut (tag_of_expr E x ∈ l) // #K1 #K2 @(Q_of_Q_ok' E l Q x)
69    cases x in K2; // ]]
70qed.
71
72let rec sub_expr_elim_type
73 (E:Type[0]) (fixed_l: list tag) (orig: fixed_l E)
74 (Q: fixed_l E → Prop)
75 (l: list tag)
76 on l : sublist … l fixed_l → Prop ≝
77 match l return λl. sublist … l fixed_l → Prop with
78 [ nil ⇒ λH. Q orig
79 | cons hd tl ⇒ λH.
80    let tail_call ≝ sub_expr_elim_type E fixed_l orig Q tl ? in
81     Q_holds_for_tag' … fixed_l Q hd (sublist_hd_tl_to_memb … hd tl fixed_l H) →
82      tail_call ].
83/2/ qed.
84
85lemma sub_expr_elim0:
86 ∀E:Type[0]. ∀l: list tag. ∀x: l E. ∀Q: l E → Prop.
87  ∀l',H.
88   (∀y:l E. ¬ is_in … l' y → Q y) →
89    sub_expr_elim_type E l x Q l' H.
90 #E #l #x #Q #l' elim l' /2/
91 #hd #tl #IH (*cases hd*) #H #INV whd #P0 @IH #y
92 whd in match (is_in ???) in INV:%;
93 lapply (Q_holds_for_tag_spec' … P0) #K1 #K2
94 inversion (tag_of_expr … y == hd) #K3
95 [ lapply (K1 y)
96   [ whd in match (is_in ???); >K3 %
97   | cases y in K3; // ]
98 | @INV whd in match (is_in ???); >K3 // ]
99qed.
100
101theorem sub_expr_elim:
102 ∀E:Type[0]. ∀l: list tag. ∀x: l E. ∀Q: l E → Prop.
103  sub_expr_elim_type E l x Q l ?.
104[2://
105| #E #l #x #Q @sub_expr_elim0 * #y #H #NH
106  cases (?: False) cases (is_in E l y) in H NH; //
107qed.
Note: See TracBrowser for help on using the repository browser.