1 | (* |
---|
2 | include "infrastructure.ma". |
---|
3 | axiom tag: DeqSet. |
---|
4 | axiom expr: Type[0] → Type[0]. |
---|
5 | axiom tag_of_expr: ∀E:Type[0]. expr E → tag. |
---|
6 | axiom Q_holds_for_tag: ∀E:Type[0]. ∀Q: expr E → Prop. ∀t:tag. Prop. |
---|
7 | axiom 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 | |
---|
12 | include "test.ma". |
---|
13 | |
---|
14 | definition is_in : ∀E: Type[0]. list tag -> expr E -> bool ≝ |
---|
15 | λE,l,e. memb … (tag_of_expr ? e) l. |
---|
16 | |
---|
17 | record 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 | |
---|
23 | coercion sub_expr : ∀l:list tag. Type[0] → Type[0] |
---|
24 | ≝ sub_expr on _l: list tag to Type[0] → Type[0]. |
---|
25 | |
---|
26 | coercion 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 | |
---|
31 | definition 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 …). |
---|
38 | whd in match (is_in ???); >H // |
---|
39 | qed. |
---|
40 | |
---|
41 | lemma 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. |
---|
47 | P (match b return λx.Q x → B with [ true ⇒ λprf.c1 prf | false ⇒ λprf.c2 prf ] prf). |
---|
48 | * // qed. |
---|
49 | |
---|
50 | lemma 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 |
---|
56 | qed. |
---|
57 | |
---|
58 | definition 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 | |
---|
63 | theorem 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; // ]] |
---|
79 | qed. |
---|
80 | |
---|
81 | let 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 | |
---|
94 | lemma 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 // ] |
---|
108 | qed. |
---|
109 | |
---|
110 | theorem 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; // |
---|
116 | qed. |
---|