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/grammar/term_simple.ma".
16 include "basic_2/substitution/ldrop.ma".
18 (* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************)
20 (* reducible binary items *)
21 definition ri2: item2 → Prop ≝
22 λI. I = Bind2 true Abbr ∨ I = Flat2 Cast.
24 (* irreducible binary binders *)
25 definition ib2: bool → bind2 → Prop ≝
26 λa,I. I = Abst ∨ Bind2 a I = Bind2 false Abbr.
29 inductive crf: lenv → predicate term ≝
30 | crf_delta : ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → crf L (#i)
31 | crf_appl_sn: ∀L,V,T. crf L V → crf L (ⓐV. T)
32 | crf_appl_dx: ∀L,V,T. crf L T → crf L (ⓐV. T)
33 | crf_ri2 : ∀I,L,V,T. ri2 I → crf L (②{I}V. T)
34 | crf_ib2_sn : ∀a,I,L,V,T. ib2 a I → crf L V → crf L (ⓑ{a,I}V. T)
35 | crf_ib2_dx : ∀a,I,L,V,T. ib2 a I → crf (L.ⓑ{I}V) T → crf L (ⓑ{a,I}V. T)
36 | crf_beta : ∀a,L,V,W,T. crf L (ⓐV. ⓛ{a}W. T)
37 | crf_theta : ∀a,L,V,W,T. crf L (ⓐV. ⓓ{a}W. T)
41 "context-sensitive reducibility (term)"
42 'Reducible L T = (crf L T).
44 (* Basic inversion lemmas ***************************************************)
46 fact trf_inv_atom_aux: ∀I,L,T. L ⊢ 𝐑⦃T⦄ → L = ⋆ → T = ⓪{I} → ⊥.
48 [ #L #K #V #i #HLK #H1 #H2 destruct
49 lapply (ldrop_inv_atom1 … HLK) -HLK #H destruct
50 | #L #V #T #_ #_ #H destruct
51 | #L #V #T #_ #_ #H destruct
52 | #J #L #V #T #_ #_ #H destruct
53 | #a #J #L #V #T #_ #_ #_ #H destruct
54 | #a #J #L #V #T #_ #_ #_ #H destruct
55 | #a #L #V #W #T #_ #H destruct
56 | #a #L #V #W #T #_ #H destruct
60 lemma trf_inv_atom: ∀I. ⋆ ⊢ 𝐑⦃⓪{I}⦄ → ⊥.
63 fact crf_inv_abst_aux: ∀a,L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓛ{a}W. U →
64 L ⊢ 𝐑⦃W⦄ ∨ L.ⓛW ⊢ 𝐑⦃U⦄.
66 [ #L #K #V #i #_ #H destruct
67 | #L #V #T #_ #H destruct
68 | #L #V #T #_ #H destruct
69 | #J #L #V #T #H1 #H2 destruct
70 elim H1 -H1 #H destruct
71 | #b #J #L #V #T #_ #HV #H destruct /2 width=1/
72 | #b #J #L #V #T #_ #HT #H destruct /2 width=1/
73 | #b #L #V #W #T #H destruct
74 | #b #L #V #W #T #H destruct
78 lemma crf_inv_abst: ∀a,L,W,T. L ⊢ 𝐑⦃ⓛ{a}W.T⦄ → L ⊢ 𝐑⦃W⦄ ∨ L.ⓛW ⊢ 𝐑⦃T⦄.
81 fact crf_inv_appl_aux: ∀L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓐW. U →
82 ∨∨ L ⊢ 𝐑⦃W⦄ | L ⊢ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
84 [ #L #K #V #i #_ #H destruct
85 | #L #V #T #HV #H destruct /2 width=1/
86 | #L #V #T #HT #H destruct /2 width=1/
87 | #J #L #V #T #H1 #H2 destruct
88 elim H1 -H1 #H destruct
89 | #a #I #L #V #T #_ #_ #H destruct
90 | #a #I #L #V #T #_ #_ #H destruct
91 | #a #L #V #W0 #T #H destruct
92 @or3_intro2 #H elim (simple_inv_bind … H)
93 | #a #L #V #W0 #T #H destruct
94 @or3_intro2 #H elim (simple_inv_bind … H)
98 lemma crf_inv_appl: ∀L,V,T. L ⊢ 𝐑⦃ⓐV.T⦄ → ∨∨ L ⊢ 𝐑⦃V⦄ | L ⊢ 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥).