1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/rt_computation/rdsx.ma".
17 (* STRONGLY NORMALIZING SELECTED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******)
19 (* Basic_2A1: uses: lcosx *)
20 inductive sdsx (h) (G): rtmap → predicate lenv ≝
21 | sdsx_atom: ∀f. sdsx h G f (⋆)
22 | sdsx_push: ∀f,I,K. sdsx h G f K → sdsx h G (⫯f) (K.ⓘ{I})
23 | sdsx_unit: ∀f,I,K. sdsx h G f K → sdsx h G (↑f) (K.ⓤ{I})
24 | sdsx_pair: ∀f,I,K,V. G ⊢ ⬈*[h,V] 𝐒⦃K⦄ →
25 sdsx h G f K → sdsx h G (↑f) (K.ⓑ{I}V)
29 "strong normalization for unbound context-sensitive parallel rt-transition on selected entries (local environment)"
30 'PRedTySNStrong h f G L = (sdsx h G f L).
32 (* Basic inversion lemmas ***************************************************)
34 fact sdsx_inv_push_aux (h) (G):
35 ∀g,L. G ⊢ ⬈*[h,g] 𝐒⦃L⦄ →
36 ∀f,I,K. g = ⫯f → L = K.ⓘ{I} → G ⊢ ⬈*[h,f] 𝐒⦃K⦄.
38 [ #f #g #J #L #_ #H destruct
39 | #f #I #K #HK #g #J #L #H1 #H2 destruct //
40 | #f #I #K #_ #g #J #L #H #_
41 elim (discr_next_push … H)
42 | #f #I #K #V #_ #_ #g #J #L #H #_
43 elim (discr_next_push … H)
47 lemma sdsx_inv_push (h) (G):
48 ∀f,I,K. G ⊢ ⬈*[h,⫯f] 𝐒⦃K.ⓘ{I}⦄ → G ⊢ ⬈*[h,f] 𝐒⦃K⦄.
49 /2 width=6 by sdsx_inv_push_aux/ qed-.
51 fact sdsx_inv_unit_aux (h) (G):
52 ∀g,L. G ⊢ ⬈*[h,g] 𝐒⦃L⦄ →
53 ∀f,I,K. g = ↑f → L = K.ⓤ{I} → G ⊢ ⬈*[h,f] 𝐒⦃K⦄.
55 [ #f #g #J #L #_ #H destruct
56 | #f #I #K #_ #g #J #L #H #_
57 elim (discr_push_next … H)
58 | #f #I #K #HK #g #J #L #H1 #H2 destruct //
59 | #f #I #K #V #_ #_ #g #J #L #_ #H destruct
63 lemma sdsx_inv_unit (h) (G):
64 ∀f,I,K. G ⊢ ⬈*[h,↑f] 𝐒⦃K.ⓤ{I}⦄ → G ⊢ ⬈*[h,f] 𝐒⦃K⦄.
65 /2 width=6 by sdsx_inv_unit_aux/ qed-.
67 fact sdsx_inv_pair_aux (h) (G):
68 ∀g,L. G ⊢ ⬈*[h,g] 𝐒⦃L⦄ →
69 ∀f,I,K,V. g = ↑f → L = K.ⓑ{I}V →
70 ∧∧ G ⊢ ⬈*[h,V] 𝐒⦃K⦄ & G ⊢ ⬈*[h,f] 𝐒⦃K⦄.
72 [ #f #g #J #L #W #_ #H destruct
73 | #f #I #K #_ #g #J #L #W #H #_
74 elim (discr_push_next … H)
75 | #f #I #K #_ #g #J #L #W #_ #H destruct
76 | #f #I #K #V #HV #HK #g #J #L #W #H1 #H2 destruct
81 (* Basic_2A1: uses: lcosx_inv_pair *)
82 lemma sdsx_inv_pair (h) (G):
83 ∀f,I,K,V. G ⊢ ⬈*[h,↑f] 𝐒⦃K.ⓑ{I}V⦄ →
84 ∧∧ G ⊢ ⬈*[h,V] 𝐒⦃K⦄ & G ⊢ ⬈*[h,f] 𝐒⦃K⦄.
85 /2 width=6 by sdsx_inv_pair_aux/ qed-.
87 (* Advanced inversion lemmas ************************************************)
89 lemma sdsx_inv_pair_gen (h) (G):
90 ∀g,I,K,V. G ⊢ ⬈*[h,g] 𝐒⦃K.ⓑ{I}V⦄ →
91 ∨∨ ∃∃f. G ⊢ ⬈*[h,f] 𝐒⦃K⦄ & g = ⫯f
92 | ∃∃f. G ⊢ ⬈*[h,V] 𝐒⦃K⦄ & G ⊢ ⬈*[h,f] 𝐒⦃K⦄ & g = ↑f.
94 elim (pn_split g) * #f #Hf destruct
95 [ lapply (sdsx_inv_push … H) -H /3 width=3 by ex2_intro, or_introl/
96 | elim (sdsx_inv_pair … H) -H /3 width=3 by ex3_intro, or_intror/
100 (* Advanced forward lemmas **************************************************)
102 lemma sdsx_fwd_bind (h) (G):
103 ∀g,I,K. G ⊢ ⬈*[h,g] 𝐒⦃K.ⓘ{I}⦄ → G ⊢ ⬈*[h,⫱g] 𝐒⦃K⦄.
105 elim (pn_split g) * #f #Hf destruct
106 [ #H lapply (sdsx_inv_push … H) -H //
108 [ #H lapply (sdsx_inv_unit … H) -H //
109 | #V #H elim (sdsx_inv_pair … H) -H //
114 (* Basic properties *********************************************************)
116 lemma sdsx_eq_repl_back (h) (G):
117 ∀L. eq_repl_back … (λf. G ⊢ ⬈*[h,f] 𝐒⦃L⦄).
118 #h #G #L #f1 #H elim H -L -f1
120 | #f1 #I #L #_ #IH #x2 #H
121 elim (eq_inv_px … H) -H /3 width=3 by sdsx_push/
122 | #f1 #I #L #_ #IH #x2 #H
123 elim (eq_inv_nx … H) -H /3 width=3 by sdsx_unit/
124 | #f1 #I #L #V #HV #_ #IH #x2 #H
125 elim (eq_inv_nx … H) -H /3 width=3 by sdsx_pair/
129 lemma sdsx_eq_repl_fwd (h) (G):
130 ∀L. eq_repl_fwd … (λf. G ⊢ ⬈*[h,f] 𝐒⦃L⦄).
131 #h #G #L @eq_repl_sym /2 width=3 by sdsx_eq_repl_back/
134 (* Advanced properties ******************************************************)
136 (* Basic_2A1: uses: lcosx_O *)
137 lemma sdsx_isid (h) (G):
138 ∀f. 𝐈⦃f⦄ → ∀L. G ⊢ ⬈*[h,f] 𝐒⦃L⦄.
139 #h #G #f #Hf #L elim L -L
140 /3 width=3 by sdsx_eq_repl_back, sdsx_push, eq_push_inv_isid/
143 (* Basic_2A1: removed theorems 2:
144 lcosx_drop_trans_lt lcosx_inv_succ