matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basic_2/notation/relations/cofreestar_4.ma".
  16 include "basic_2/relocation/lift_neg.ma".
  17 include "basic_2/substitution/cpys.ma".
  18
  19 (* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
  20
  21 definition cofrees: relation4 ynat nat lenv term ≝
  22                     λd,i,L,U1. ∀U2. ⦃⋆, L⦄ ⊢ U1 ▶*[d, ∞] U2 → ∃T2. ⇧[i, 1] T2 ≡ U2.
  23
  24 interpretation
  25    "context-sensitive exclusion from free variables (term)"
  26    'CoFreeStar L i d T = (cofrees d i L T).
  27
  28 (* Basic inversion lemmas ***************************************************)
  29
  30 lemma cofrees_inv_gen: ∀L,U,U0,d,i. ⦃⋆, L⦄ ⊢ U ▶*[d, ∞] U0 → (∀T. ⇧[i, 1] T ≡ U0 → ⊥) →
  31                        L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥.
  32 #L #U #U0 #d #i #HU0 #HnU0 #HU elim (HU … HU0) -L -U -d /2 width=2 by/
  33 qed-.
  34
  35 lemma cofrees_inv_lref_eq: ∀L,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃#i⦄ → ⊥.
  36 #L #d #i #H elim (H (#i)) -H //
  37 #X #H elim (lift_inv_lref2_be … H) -H //
  38 qed-.
  39
  40 (* Basic forward lemmas *****************************************************)
  41
  42 lemma cofrees_fwd_lift: ∀L,U,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ∃T. ⇧[i, 1] T ≡ U.
  43 /2 width=1 by/ qed-.
  44
  45 lemma cofrees_fwd_nlift: ∀L,U,d,i. (∀T. ⇧[i, 1] T ≡ U → ⊥) → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥).
  46 #L #U #d #i #HnTU #H elim (cofrees_fwd_lift … H) -H /2 width=2 by/
  47 qed-.
  48
  49 (* Basic Properties *********************************************************)
  50
  51 lemma cofrees_sort: ∀L,d,i,k. L ⊢ i ~ϵ 𝐅*[d]⦃⋆k⦄.
  52 #L #d #i #k #X #H >(cpys_inv_sort1 … H) -X /2 width=2 by ex_intro/
  53 qed.
  54
  55 lemma cofrees_gref: ∀L,d,i,p. L ⊢ i ~ϵ 𝐅*[d]⦃§p⦄.
  56 #L #d #i #p #X #H >(cpys_inv_gref1 … H) -X /2 width=2 by ex_intro/
  57 qed.
  58
  59 lemma cofrees_bind: ∀L,V,d,i. L ⊢ i ~ϵ 𝐅*[d] ⦃V⦄ →
  60                     ∀I,T. L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃T⦄ →
  61                     ∀a. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}V.T⦄.
  62 #L #W1 #d #i #HW1 #I #U1 #HU1 #a #X #H elim (cpys_inv_bind1 … H) -H
  63 #W2 #U2 #HW12 #HU12 #H destruct
  64 elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_bind, ex_intro/
  65 qed.
  66
  67 lemma cofrees_flat: ∀L,V,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ∀T. L ⊢ i ~ϵ 𝐅*[d]⦃T⦄ →
  68                     ∀I. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}V.T⦄.
  69 #L #W1 #d #i #HW1 #U1 #HU1 #I #X #H elim (cpys_inv_flat1 … H) -H
  70 #W2 #U2 #HW12 #HU12 #H destruct
  71 elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_flat, ex_intro/
  72 qed.
  73
  74 axiom cofrees_dec: ∀L,T,d,i. Decidable (L ⊢ i ~ϵ 𝐅*[d]⦃T⦄).
  75
  76 (* Negated inversion lemmas *************************************************)
  77
  78 lemma frees_inv_bind: ∀a,I,L,V,T,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}V.T⦄ → ⊥) →
  79                       (L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ⊥) ∨ (L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃T⦄ → ⊥).
  80 #a #I #L #W #U #d #i #H elim (cofrees_dec L W d i)
  81 /4 width=9 by cofrees_bind, or_intror, or_introl/
  82 qed-.
  83
  84 lemma frees_inv_flat: ∀I,L,V,T,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}V.T⦄ → ⊥) →
  85                       (L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ⊥) ∨ (L ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥).
  86 #I #L #W #U #d #H elim (cofrees_dec L W d)
  87 /4 width=8 by cofrees_flat, or_intror, or_introl/
  88 qed-.