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/lrsubeqf_4.ma".
16 include "basic_2/static/frees.ma".
18 (* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
20 inductive lsubf: relation4 lenv rtmap lenv rtmap ≝
21 | lsubf_atom: ∀f1,f2. f2 ⊆ f1 → lsubf (⋆) f1 (⋆) f2
22 | lsubf_pair: ∀f1,f2,I,L1,L2,V. f2 ⊆ f1 → lsubf L1 (⫱f1) L2 (⫱f2) →
23 lsubf (L1.ⓑ{I}V) f1 (L2.ⓑ{I}V) f2
24 | lsubf_beta: ∀f,f1,f2,L1,L2,W,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f ⊆ ⫱f1 → f2 ⊆ f1 →
25 lsubf L1 (⫱f1) L2 (⫱f2) → lsubf (L1.ⓓⓝW.V) f1 (L2.ⓛW) f2
29 "local environment refinement (context-sensitive free variables)"
30 'LRSubEqF L1 f1 L2 f2 = (lsubf L1 f1 L2 f2).
32 (* Basic inversion lemmas ***************************************************)
34 fact lsubf_inv_atom1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L1 = ⋆ →
36 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
38 | #f1 #f2 #I #L1 #L2 #V #_ #_ #H destruct
39 | #f #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H destruct
43 lemma lsubf_inv_atom1: ∀f1,f2,L2. ⦃⋆, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L2 = ⋆ ∧ f2 ⊆ f1.
44 /2 width=3 by lsubf_inv_atom1_aux/ qed-.
46 fact lsubf_inv_pair1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
47 ∀I,K1,X. L1 = K1.ⓑ{I}X →
48 (∃∃K2. f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L2 = K2.ⓑ{I}X) ∨
49 ∃∃f,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⊆ ⫱f1 &
50 f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
51 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
52 [ #f1 #f2 #_ #J #K1 #X #H destruct
53 | #f1 #f2 #I #L1 #L2 #V #H21 #HL12 #J #K1 #X #H destruct
54 /3 width=3 by ex3_intro, or_introl/
55 | #f #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H21 #HL12 #J #K1 #X #H destruct
56 /3 width=11 by ex7_4_intro, or_intror/
60 lemma lsubf_inv_pair1: ∀f1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
61 (∃∃K2. f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L2 = K2.ⓑ{I}X) ∨
62 ∃∃f,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⊆ ⫱f1 &
63 f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
64 /2 width=3 by lsubf_inv_pair1_aux/ qed-.
66 fact lsubf_inv_atom2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L2 = ⋆ →
68 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
70 | #f1 #f2 #I #L1 #L2 #V #_ #_ #H destruct
71 | #f #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H destruct
75 lemma lsubf_inv_atom2: ∀f1,f2,L1. ⦃L1, f1⦄ ⫃𝐅* ⦃⋆, f2⦄ → L1 = ⋆ ∧ f2 ⊆ f1.
76 /2 width=3 by lsubf_inv_atom2_aux/ qed-.
78 fact lsubf_inv_pair2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
79 ∀I,K2,W. L2 = K2.ⓑ{I}W →
80 (∃∃K1.f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L1 = K1.ⓑ{I}W) ∨
81 ∃∃f,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⊆ ⫱f1 &
82 f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abst & L1 = K1.ⓓⓝW.V.
83 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
84 [ #f1 #f2 #_ #J #K2 #X #H destruct
85 | #f1 #f2 #I #L1 #L2 #V #H21 #HL12 #J #K2 #X #H destruct
86 /3 width=3 by ex3_intro, or_introl/
87 | #f #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H21 #HL12 #J #K2 #X #H destruct
88 /3 width=7 by ex6_3_intro, or_intror/
92 lemma lsubf_inv_pair2: ∀f1,f2,I,L1,K2,W. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓑ{I}W, f2⦄ →
93 (∃∃K1.f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L1 = K1.ⓑ{I}W) ∨
94 ∃∃f,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⊆ ⫱f1 &
95 f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abst & L1 = K1.ⓓⓝW.V.
96 /2 width=5 by lsubf_inv_pair2_aux/ qed-.
98 (* Basic forward lemmas *****************************************************)
100 lemma lsubf_fwd_sle: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → f2 ⊆ f1.
104 (* Basic properties *********************************************************)
106 lemma lsubf_pair_nn: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
107 ∀I,V. ⦃L1.ⓑ{I}V, ⫯f1⦄ ⫃𝐅* ⦃L2.ⓑ{I}V, ⫯f2⦄.
108 /4 width=5 by lsubf_fwd_sle, lsubf_pair, sle_next/ qed.
110 lemma lsubf_refl: ∀L,f1,f2. f2 ⊆ f1 → ⦃L, f1⦄ ⫃𝐅* ⦃L, f2⦄.
111 #L elim L -L /4 width=1 by lsubf_atom, lsubf_pair, sle_tl/
114 lemma lsubf_sle_div: ∀f,f2,L1,L2. ⦃L1, f⦄ ⫃ 𝐅* ⦃L2, f2⦄ →
115 ∀f1. f1 ⊆ f2 → ⦃L1, f⦄ ⫃ 𝐅* ⦃L2, f1⦄.
116 #f #f2 #L1 #L2 #H elim H -f -f2 -L1 -L2
117 /4 width=3 by lsubf_beta, lsubf_pair, lsubf_atom, sle_tl, sle_trans/