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/cofreestar_3.ma".
16 include "basic_2/relocation/lift_neg.ma".
17 include "basic_2/substitution/cpys.ma".
19 (* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
21 definition cofrees: relation3 lenv nat term ≝
22 λL,i,U1. ∀U2. ⦃⋆, L⦄ ⊢ U1 ▶* U2 → ∃T2. ⇧[i, 1] T2 ≡ U2.
25 "context-sensitive exclusion from free variables (term)"
26 'CoFreeStar L i U = (cofrees L i U).
28 (* Basic forward lemmas *****************************************************)
30 lemma cofrees_fwd_lift: ∀L,U,i. L ⊢ i ~ϵ 𝐅*⦃U⦄ → ∃T. ⇧[i, 1] T ≡ U.
33 lemma cofrees_fwd_bind_sn: ∀a,I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}W.U⦄ →
35 #a #I #L #W1 #U #i #H #W2 #HW12 elim (H (ⓑ{a,I}W2.U)) /2 width=1 by cpys_bind/ -W1
36 #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by ex_intro/
39 lemma cofrees_fwd_bind_dx: ∀a,I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}W.U⦄ →
40 L.ⓑ{I}W ⊢ i+1 ~ϵ 𝐅*⦃U⦄.
41 #a #I #L #W #U1 #i #H #U2 #HU12 elim (H (ⓑ{a,I}W.U2)) /2 width=1 by cpys_bind/ -U1
42 #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by ex_intro/
45 lemma cofrees_fwd_flat_sn: ∀I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}W.U⦄ →
47 #I #L #W1 #U #i #H #W2 #HW12 elim (H (ⓕ{I}W2.U)) /2 width=1 by cpys_flat/ -W1
48 #X #H elim (lift_inv_flat2 … H) -H /2 width=2 by ex_intro/
51 lemma cofrees_fwd_flat_dx: ∀I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}W.U⦄ →
53 #I #L #W #U1 #i #H #U2 #HU12 elim (H (ⓕ{I}W.U2)) /2 width=1 by cpys_flat/ -U1
54 #X #H elim (lift_inv_flat2 … H) -H /2 width=2 by ex_intro/
57 (* Basic inversion lemmas ***************************************************)
59 lemma cofrees_inv_gen: ∀L,U,U0,i. ⦃⋆, L⦄ ⊢ U ▶* U0 → (∀T. ⇧[i, 1] T ≡ U0 → ⊥) →
61 #L #U #U0 #i #HU0 #HnU0 #HU elim (HU … HU0) -L -U /2 width=2 by/
64 lemma cofrees_inv_lref_eq: ∀L,i. L ⊢ i ~ϵ 𝐅*⦃#i⦄ → ⊥.
65 #L #i #H elim (H (#i)) -H //
66 #X #H elim (lift_inv_lref2_be … H) -H //
69 lemma cofrees_inv_bind: ∀a,I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}W.U⦄ →
70 L ⊢ i ~ϵ 𝐅*⦃W⦄ ∧ L.ⓑ{I}W ⊢ i+1 ~ϵ 𝐅*⦃U⦄.
71 /3 width=7 by cofrees_fwd_bind_sn, cofrees_fwd_bind_dx, conj/ qed-.
73 lemma cofrees_inv_flat: ∀I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}W.U⦄ →
74 L ⊢ i ~ϵ 𝐅*⦃W⦄ ∧ L ⊢ i ~ϵ 𝐅*⦃U⦄.
75 /3 width=6 by cofrees_fwd_flat_sn, cofrees_fwd_flat_dx, conj/ qed-.
77 (* Basic Properties *********************************************************)
79 lemma cofrees_sort: ∀L,i,k. L ⊢ i ~ϵ 𝐅*⦃⋆k⦄.
80 #L #i #k #X #H >(cpys_inv_sort1 … H) -X /2 width=2 by ex_intro/
83 lemma cofrees_gref: ∀L,i,p. L ⊢ i ~ϵ 𝐅*⦃§p⦄.
84 #L #i #p #X #H >(cpys_inv_gref1 … H) -X /2 width=2 by ex_intro/
87 lemma cofrees_bind: ∀L,V,i. L ⊢ i ~ϵ 𝐅*⦃V⦄ →
88 ∀I,T. L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*⦃T⦄ →
89 ∀a. L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}V.T⦄.
90 #L #W1 #i #HW1 #I #U1 #HU1 #a #X #H elim (cpys_inv_bind1 … H) -H
91 #W2 #U2 #HW12 #HU12 #H destruct
92 elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_bind, ex_intro/
95 lemma cofrees_flat: ∀L,V,i. L ⊢ i ~ϵ 𝐅*⦃V⦄ → ∀T. L ⊢ i ~ϵ 𝐅*⦃T⦄ →
96 ∀I. L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}V.T⦄.
97 #L #W1 #i #HW1 #U1 #HU1 #I #X #H elim (cpys_inv_flat1 … H) -H
98 #W2 #U2 #HW12 #HU12 #H destruct
99 elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_flat, ex_intro/
102 axiom cofrees_dec: ∀L,T,i. Decidable (L ⊢ i ~ϵ 𝐅*⦃T⦄).
104 (* Basic negated inversion lemmas *******************************************)
106 lemma frees_inv_bind: ∀a,I,L,V,T,i. (L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}V.T⦄ → ⊥) →
107 (L ⊢ i ~ϵ 𝐅*⦃V⦄ → ⊥) ∨ (L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*⦃T⦄ → ⊥).
108 #a #I #L #W #U #i #H elim (cofrees_dec L W i)
109 /4 width=8 by cofrees_bind, or_intror, or_introl/
112 lemma frees_inv_flat: ∀I,L,V,T,i. (L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}V.T⦄ → ⊥) →
113 (L ⊢ i ~ϵ 𝐅*⦃V⦄ → ⊥) ∨ (L ⊢ i ~ϵ 𝐅*⦃T⦄ → ⊥).
114 #I #L #W #U #i #H elim (cofrees_dec L W i)
115 /4 width=7 by cofrees_flat, or_intror, or_introl/