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

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

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

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