matita/matita/contribs/lambdadelta/basic_2/etc/frees/frees_bind.etc

   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/syntax/bind.ma".
  16 include "basic_2/static/frees.ma".
  17
  18 (* CONTEXT-SENSITIVE FREE VARIABLES FOR BINDERS *****************************)
  19
  20 inductive freesb (L): relation2 … ≝
  21 | freesb_pair: ∀I,V,f. L ⊢ 𝐅*⦃V⦄ ≡ f → freesb L (BPair I V) f
  22 | freesb_unit: ∀I,f. 𝐈⦃f⦄ → freesb L (BUnit I) f
  23 .
  24
  25 interpretation
  26    "context-sensitive free variables (binder)"
  27    'FreeStar L I f = (freesb L I f).
  28
  29 (* Basic inversion lemmas ***************************************************)
  30
  31 fact frees_inv_pair_aux: ∀L,Z,f. L ⊢ 𝐅*⦃Z⦄ ≡ f →
  32                          ∀I,V. Z = BPair I V → L ⊢ 𝐅*⦃V⦄ ≡ f.
  33 #L #Z #f * -Z -f
  34 [ #I #V #f #Hf #Z #X #H destruct //
  35 | #I #f #_ #Z #X #H destruct
  36 ]
  37 qed-.
  38
  39 lemma frees_inv_pair: ∀L,I,V,f. L ⊢ 𝐅*⦃BPair I V⦄ ≡ f → L ⊢ 𝐅*⦃V⦄ ≡ f.
  40 /2 width=4 by frees_inv_pair_aux/ qed-.
  41
  42 fact frees_inv_unit_aux: ∀L,Z,f. L ⊢ 𝐅*⦃Z⦄ ≡ f →
  43                          ∀I. Z = BUnit I → 𝐈⦃f⦄.
  44 #L #Z #f * -Z -f
  45 [ #I #V #f #_ #Z #H destruct
  46 | #I #f #Hf #Z #H destruct //
  47 ]
  48 qed-.
  49
  50 lemma frees_inv_unit: ∀L,I,f. L ⊢ 𝐅*⦃BUnit I⦄ ≡ f → 𝐈⦃f⦄.
  51 /2 width=5 by frees_inv_unit_aux/ qed-.