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/notation/relations/reducible_5.ma".
16 include "basic_2/static/sd.ma".
17 include "basic_2/reduction/crr.ma".
19 (* CONTEXT-SENSITIVE EXTENDED REDUCIBLE TERMS *******************************)
22 (* extended reducible terms *)
23 inductive crx (h) (g) (G:genv): relation2 lenv term ≝
24 | crx_sort : ∀L,k,l. deg h g k (l+1) → crx h g G L (⋆k)
25 | crx_delta : ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → crx h g G L (#i)
26 | crx_appl_sn: ∀L,V,T. crx h g G L V → crx h g G L (ⓐV.T)
27 | crx_appl_dx: ∀L,V,T. crx h g G L T → crx h g G L (ⓐV.T)
28 | crx_ri2 : ∀I,L,V,T. ri2 I → crx h g G L (②{I}V.T)
29 | crx_ib2_sn : ∀a,I,L,V,T. ib2 a I → crx h g G L V → crx h g G L (ⓑ{a,I}V.T)
30 | crx_ib2_dx : ∀a,I,L,V,T. ib2 a I → crx h g G (L.ⓑ{I}V) T → crx h g G L (ⓑ{a,I}V.T)
31 | crx_beta : ∀a,L,V,W,T. crx h g G L (ⓐV. ⓛ{a}W.T)
32 | crx_theta : ∀a,L,V,W,T. crx h g G L (ⓐV. ⓓ{a}W.T)
36 "context-sensitive extended reducibility (term)"
37 'Reducible h g G L T = (crx h g G L T).
39 (* Basic properties *********************************************************)
41 lemma crr_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄.
42 #h #g #G #L #T #H elim H -L -T // /2 width=1/ /2 width=4/
45 (* Basic inversion lemmas ***************************************************)
47 fact crx_inv_sort_aux: ∀h,g,G,L,T,k. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ⋆k →
49 #h #g #G #L #T #k0 * -L -T
50 [ #L #k #l #Hkl #H destruct /2 width=2/
51 | #I #L #K #V #i #HLK #H destruct
52 | #L #V #T #_ #H destruct
53 | #L #V #T #_ #H destruct
54 | #I #L #V #T #_ #H destruct
55 | #a #I #L #V #T #_ #_ #H destruct
56 | #a #I #L #V #T #_ #_ #H destruct
57 | #a #L #V #W #T #H destruct
58 | #a #L #V #W #T #H destruct
62 lemma crx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃⋆k⦄ → ∃l. deg h g k (l+1).
63 /2 width=5 by crx_inv_sort_aux/ qed-.
65 fact crx_inv_lref_aux: ∀h,g,G,L,T,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = #i →
66 ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
67 #h #g #G #L #T #j * -L -T
68 [ #L #k #l #_ #H destruct
69 | #I #L #K #V #i #HLK #H destruct /2 width=4/
70 | #L #V #T #_ #H destruct
71 | #L #V #T #_ #H destruct
72 | #I #L #V #T #_ #H destruct
73 | #a #I #L #V #T #_ #_ #H destruct
74 | #a #I #L #V #T #_ #_ #H destruct
75 | #a #L #V #W #T #H destruct
76 | #a #L #V #W #T #H destruct
80 lemma crx_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃#i⦄ → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
81 /2 width=6 by crx_inv_lref_aux/ qed-.
83 fact crx_inv_gref_aux: ∀h,g,G,L,T,p. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = §p → ⊥.
84 #h #g #G #L #T #q * -L -T
85 [ #L #k #l #_ #H destruct
86 | #I #L #K #V #i #HLK #H destruct
87 | #L #V #T #_ #H destruct
88 | #L #V #T #_ #H destruct
89 | #I #L #V #T #_ #H destruct
90 | #a #I #L #V #T #_ #_ #H destruct
91 | #a #I #L #V #T #_ #_ #H destruct
92 | #a #L #V #W #T #H destruct
93 | #a #L #V #W #T #H destruct
97 lemma crx_inv_gref: ∀h,g,G,L,p. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃§p⦄ → ⊥.
98 /2 width=8 by crx_inv_gref_aux/ qed-.
100 lemma trx_inv_atom: ∀h,g,I,G. ⦃G, ⋆⦄ ⊢ 𝐑[h, g]⦃⓪{I}⦄ →
101 ∃∃k,l. deg h g k (l+1) & I = Sort k.
103 [ elim (crx_inv_sort … H) -H /2 width=4/
104 | elim (crx_inv_lref … H) -H #I #L #V #H
105 elim (ldrop_inv_atom1 … H) -H #H destruct
106 | elim (crx_inv_gref … H)
110 fact crx_inv_ib2_aux: ∀h,g,a,I,G,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ →
111 T = ⓑ{a,I}W.U → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ 𝐑[h, g]⦃U⦄.
112 #h #g #b #J #G #L #W0 #U #T #HI * -L -T
113 [ #L #k #l #_ #H destruct
114 | #I #L #K #V #i #_ #H destruct
115 | #L #V #T #_ #H destruct
116 | #L #V #T #_ #H destruct
117 | #I #L #V #T #H1 #H2 destruct
118 elim H1 -H1 #H destruct
119 elim HI -HI #H destruct
120 | #a #I #L #V #T #_ #HV #H destruct /2 width=1/
121 | #a #I #L #V #T #_ #HT #H destruct /2 width=1/
122 | #a #L #V #W #T #H destruct
123 | #a #L #V #W #T #H destruct
127 lemma crx_inv_ib2: ∀h,g,a,I,G,L,W,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃ⓑ{a,I}W.T⦄ →
128 ⦃G, L⦄ ⊢ 𝐑[h, g]⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ 𝐑[h, g]⦃T⦄.
129 /2 width=5 by crx_inv_ib2_aux/ qed-.
131 fact crx_inv_appl_aux: ∀h,g,G,L,W,U,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ⓐW.U →
132 ∨∨ ⦃G, L⦄ ⊢ 𝐑[h, g]⦃W⦄ | ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄ | (𝐒⦃U⦄ → ⊥).
133 #h #g #G #L #W0 #U #T * -L -T
134 [ #L #k #l #_ #H destruct
135 | #I #L #K #V #i #_ #H destruct
136 | #L #V #T #HV #H destruct /2 width=1/
137 | #L #V #T #HT #H destruct /2 width=1/
138 | #I #L #V #T #H1 #H2 destruct
139 elim H1 -H1 #H destruct
140 | #a #I #L #V #T #_ #_ #H destruct
141 | #a #I #L #V #T #_ #_ #H destruct
142 | #a #L #V #W #T #H destruct
143 @or3_intro2 #H elim (simple_inv_bind … H)
144 | #a #L #V #W #T #H destruct
145 @or3_intro2 #H elim (simple_inv_bind … H)
149 lemma crx_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃ⓐV.T⦄ →
150 ∨∨ ⦃G, L⦄ ⊢ 𝐑[h, g]⦃V⦄ | ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ | (𝐒⦃T⦄ → ⊥).
151 /2 width=3 by crx_inv_appl_aux/ qed-.