matita/matita/contribs/lambdadelta/basic_2/static/lsubf.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/lrsubeqf_4.ma".
  16 include "basic_2/static/frees.ma".
  17
  18 (* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
  19
  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
  26 .
  27
  28 interpretation
  29   "local environment refinement (context-sensitive free variables)"
  30   'LRSubEqF L1 f1 L2 f2 = (lsubf L1 f1 L2 f2).
  31
  32 (* Basic inversion lemmas ***************************************************)
  33
  34 fact lsubf_inv_atom1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L1 = ⋆ →
  35                           L2 = ⋆ ∧ f2 ⊆ f1.
  36 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  37 [ /2 width=1 by conj/
  38 | #f1 #f2 #I #L1 #L2 #V #_ #_ #H destruct
  39 | #f #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H destruct
  40 ]
  41 qed-.
  42
  43 lemma lsubf_inv_atom1: ∀f1,f2,L2. ⦃⋆, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L2 = ⋆ ∧ f2 ⊆ f1.
  44 /2 width=3 by lsubf_inv_atom1_aux/ qed-.
  45
  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/
  57 ]
  58 qed-.
  59
  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-.
  65
  66 fact lsubf_inv_atom2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L2 = ⋆ →
  67                           L1 = ⋆ ∧ f2 ⊆ f1.
  68 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  69 [ /2 width=1 by conj/
  70 | #f1 #f2 #I #L1 #L2 #V #_ #_ #H destruct
  71 | #f #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H destruct
  72 ]
  73 qed-.
  74
  75 lemma lsubf_inv_atom2: ∀f1,f2,L1. ⦃L1, f1⦄ ⫃𝐅* ⦃⋆, f2⦄ → L1 = ⋆ ∧ f2 ⊆ f1.
  76 /2 width=3 by lsubf_inv_atom2_aux/ qed-.
  77
  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/
  89 ]
  90 qed-.
  91
  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-.
  97
  98 (* Basic forward lemmas *****************************************************)
  99
 100 lemma lsubf_fwd_sle: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → f2 ⊆ f1.
 101 #f1 #f2 #L1 #L2 * //
 102 qed-.
 103
 104 (* Basic properties *********************************************************)
 105
 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.
 109
 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/
 112 qed.
 113
 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/
 118 qed-.