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_2.ma".
16 include "basic_2/relocation/ldrop.ma".
18 (* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************)
20 (* reducible binary items *)
21 definition ri2: predicate item2 ≝
22 λI. I = Bind2 true Abbr ∨ I = Flat2 Cast.
24 (* irreducible binary binders *)
25 definition ib2: relation2 bool bind2 ≝
26 λa,I. I = Abst ∨ Bind2 a I = Bind2 false Abbr.
29 inductive crr: lenv → predicate term ≝
30 | crr_delta : ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → crr L (#i)
31 | crr_appl_sn: ∀L,V,T. crr L V → crr L (ⓐV.T)
32 | crr_appl_dx: ∀L,V,T. crr L T → crr L (ⓐV.T)
33 | crr_ri2 : ∀I,L,V,T. ri2 I → crr L (②{I}V.T)
34 | crr_ib2_sn : ∀a,I,L,V,T. ib2 a I → crr L V → crr L (ⓑ{a,I}V.T)
35 | crr_ib2_dx : ∀a,I,L,V,T. ib2 a I → crr (L.ⓑ{I}V) T → crr L (ⓑ{a,I}V.T)
36 | crr_beta : ∀a,L,V,W,T. crr L (ⓐV. ⓛ{a}W.T)
37 | crr_theta : ∀a,L,V,W,T. crr L (ⓐV. ⓓ{a}W.T)
41 "context-sensitive reducibility (term)"
42 'Reducible L T = (crr L T).
44 (* Basic inversion lemmas ***************************************************)
46 fact crr_inv_sort_aux: ∀L,T,k. L ⊢ 𝐑⦃T⦄ → T = ⋆k → ⊥.
48 [ #L #K #V #i #HLK #H destruct
49 | #L #V #T #_ #H destruct
50 | #L #V #T #_ #H destruct
51 | #I #L #V #T #_ #H destruct
52 | #a #I #L #V #T #_ #_ #H destruct
53 | #a #I #L #V #T #_ #_ #H destruct
54 | #a #L #V #W #T #H destruct
55 | #a #L #V #W #T #H destruct
59 lemma crr_inv_sort: ∀L,k. L ⊢ 𝐑⦃⋆k⦄ → ⊥.
60 /2 width=5 by crr_inv_sort_aux/ qed-.
62 fact crr_inv_lref_aux: ∀L,T,i. L ⊢ 𝐑⦃T⦄ → T = #i → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
64 [ #L #K #V #i #HLK #H destruct /2 width=3/
65 | #L #V #T #_ #H destruct
66 | #L #V #T #_ #H destruct
67 | #I #L #V #T #_ #H destruct
68 | #a #I #L #V #T #_ #_ #H destruct
69 | #a #I #L #V #T #_ #_ #H destruct
70 | #a #L #V #W #T #H destruct
71 | #a #L #V #W #T #H destruct
75 lemma crr_inv_lref: ∀L,i. L ⊢ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
76 /2 width=3 by crr_inv_lref_aux/ qed-.
78 fact crr_inv_gref_aux: ∀L,T,p. L ⊢ 𝐑⦃T⦄ → T = §p → ⊥.
80 [ #L #K #V #i #HLK #H destruct
81 | #L #V #T #_ #H destruct
82 | #L #V #T #_ #H destruct
83 | #I #L #V #T #_ #H destruct
84 | #a #I #L #V #T #_ #_ #H destruct
85 | #a #I #L #V #T #_ #_ #H destruct
86 | #a #L #V #W #T #H destruct
87 | #a #L #V #W #T #H destruct
91 lemma crr_inv_gref: ∀L,p. L ⊢ 𝐑⦃§p⦄ → ⊥.
92 /2 width=5 by crr_inv_gref_aux/ qed-.
94 lemma trr_inv_atom: ∀I. ⋆ ⊢ 𝐑⦃⓪{I}⦄ → ⊥.
96 [ elim (crr_inv_sort … H)
97 | elim (crr_inv_lref … H) -H #L #V #H
98 elim (ldrop_inv_atom1 … H) -H #H destruct
99 | elim (crr_inv_gref … H)
103 fact crr_inv_ib2_aux: ∀a,I,L,W,U,T. ib2 a I → L ⊢ 𝐑⦃T⦄ → T = ⓑ{a,I}W.U →
104 L ⊢ 𝐑⦃W⦄ ∨ L.ⓑ{I}W ⊢ 𝐑⦃U⦄.
105 #b #J #L #W0 #U #T #HI * -L -T
106 [ #L #K #V #i #_ #H destruct
107 | #L #V #T #_ #H destruct
108 | #L #V #T #_ #H destruct
109 | #I #L #V #T #H1 #H2 destruct
110 elim H1 -H1 #H destruct
111 elim HI -HI #H destruct
112 | #a #I #L #V #T #_ #HV #H destruct /2 width=1/
113 | #a #I #L #V #T #_ #HT #H destruct /2 width=1/
114 | #a #L #V #W #T #H destruct
115 | #a #L #V #W #T #H destruct
119 lemma crr_inv_ib2: ∀a,I,L,W,T. ib2 a I → L ⊢ 𝐑⦃ⓑ{a,I}W.T⦄ →
120 L ⊢ 𝐑⦃W⦄ ∨ L.ⓑ{I}W ⊢ 𝐑⦃T⦄.
121 /2 width=5 by crr_inv_ib2_aux/ qed-.
123 fact crr_inv_appl_aux: ∀L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓐW.U →
124 ∨∨ L ⊢ 𝐑⦃W⦄ | L ⊢ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
126 [ #L #K #V #i #_ #H destruct
127 | #L #V #T #HV #H destruct /2 width=1/
128 | #L #V #T #HT #H destruct /2 width=1/
129 | #I #L #V #T #H1 #H2 destruct
130 elim H1 -H1 #H destruct
131 | #a #I #L #V #T #_ #_ #H destruct
132 | #a #I #L #V #T #_ #_ #H destruct
133 | #a #L #V #W #T #H destruct
134 @or3_intro2 #H elim (simple_inv_bind … H)
135 | #a #L #V #W #T #H destruct
136 @or3_intro2 #H elim (simple_inv_bind … H)
140 lemma crr_inv_appl: ∀L,V,T. L ⊢ 𝐑⦃ⓐV.T⦄ → ∨∨ L ⊢ 𝐑⦃V⦄ | L ⊢ 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥).
141 /2 width=3 by crr_inv_appl_aux/ qed-.