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: ∀f. lsubf (⋆) f (⋆) f
  22 | lsubf_push: ∀f1,f2,I,L1,L2,V. lsubf L1 f1 L2 f2 →
  23               lsubf (L1.ⓑ{I}V) (↑f1) (L2.ⓑ{I}V) (↑f2)
  24 | lsubf_next: ∀f1,f2,I,L1,L2,V. lsubf L1 f1 L2 f2 →
  25               lsubf (L1.ⓑ{I}V) (⫯f1) (L2.ⓑ{I}V) (⫯f2)
  26 | lsubf_peta: ∀f1,f,f2,L1,L2,W,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f2 ⋓ f ≡ f1 →
  27               lsubf L1 f1 L2 f2 → lsubf (L1.ⓓⓝW.V) (↑f1) (L2.ⓛW) (↑f2)
  28 | lsubf_neta: ∀f1,f,f2,L1,L2,W,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f2 ⋓ f ≡ f1 →
  29               lsubf L1 f1 L2 f2 → lsubf (L1.ⓓⓝW.V) (⫯f1) (L2.ⓛW) (⫯f2)
  30 .
  31
  32 interpretation
  33   "local environment refinement (context-sensitive free variables)"
  34   'LRSubEqF L1 f1 L2 f2 = (lsubf L1 f1 L2 f2).
  35
  36 (* Basic inversion lemmas ***************************************************)
  37
  38 fact lsubf_inv_atom1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L1 = ⋆ →
  39                           L2 = ⋆ ∧ f1 = f2.
  40 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  41 [ /2 width=1 by conj/
  42 | #f1 #f2 #I #L1 #L2 #V #_ #H destruct
  43 | #f1 #f2 #I #L1 #L2 #V #_ #H destruct
  44 | #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
  45 | #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
  46 ]
  47 qed-.
  48
  49 lemma lsubf_inv_atom1: ∀f1,f2,L2. ⦃⋆, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  50                        L2 = ⋆ ∧ f1 = f2.
  51 /2 width=3 by lsubf_inv_atom1_aux/ qed-.
  52
  53 fact lsubf_inv_push1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  54                           ∀g1,I,K1,X. f1 = ↑g1 → L1 = K1.ⓑ{I}X →
  55                           (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ↑g2 & L2 = K2.ⓑ{I}X) ∨
  56                           ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
  57                                          ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ↑g2 & L2 = K2.ⓛW & X = ⓝW.V.
  58 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  59 [ #f #g1 #J #K1 #X #_ #H destruct
  60 | #f1 #f2 #I #L1 #L2 #V #HL12 #g1 #J #K1 #X #H1 #H2 destruct
  61   /3 width=5 by injective_push, ex3_2_intro, or_introl/
  62 | #f1 #f2 #I #L1 #L2 #V #_ #g1 #J #K1 #X #H elim (discr_next_push … H)
  63 | #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g1 #J #K1 #X #H1 #H2 destruct
  64   /3 width=11 by injective_push, ex7_5_intro, or_intror/
  65 | #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g1 #J #K1 #X #H elim (discr_next_push … H)
  66 ]
  67 qed-.
  68
  69 lemma lsubf_inv_push1: ∀g1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, ↑g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  70                        (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ↑g2 & L2 = K2.ⓑ{I}X) ∨
  71                        ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
  72                                       ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ↑g2 & L2 = K2.ⓛW & X = ⓝW.V.
  73 /2 width=5 by lsubf_inv_push1_aux/ qed-.
  74
  75 fact lsubf_inv_next1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  76                           ∀g1,I,K1,X. f1 = ⫯g1 → L1 = K1.ⓑ{I}X →
  77                           (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2 & L2 = K2.ⓑ{I}X) ∨
  78                           ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
  79                                          ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ⫯g2 & L2 = K2.ⓛW & X = ⓝW.V.
  80 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  81 [ #f #g1 #J #K1 #X #_ #H destruct
  82 | #f1 #f2 #I #L1 #L2 #V #_ #g1 #J #K1 #X #H elim (discr_push_next … H)
  83 | #f1 #f2 #I #L1 #L2 #V #HL12 #g1 #J #K1 #X #H1 #H2 destruct
  84   /3 width=5 by injective_next, ex3_2_intro, or_introl/
  85 | #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g1 #J #K1 #X #H elim (discr_push_next … H)
  86 | #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g1 #J #K1 #X #H1 #H2 destruct
  87   /3 width=11 by injective_next, ex7_5_intro, or_intror/
  88 ]
  89 qed-.
  90
  91 lemma lsubf_inv_next1: ∀g1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, ⫯g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  92                        (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2 & L2 = K2.ⓑ{I}X) ∨
  93                        ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
  94                                       ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ⫯g2 & L2 = K2.ⓛW & X = ⓝW.V.
  95 /2 width=5 by lsubf_inv_next1_aux/ qed-.
  96
  97 fact lsubf_inv_atom2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L2 = ⋆ →
  98                           L1 = ⋆ ∧ f1 = f2.
  99 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 100 [ /2 width=1 by conj/
 101 | #f1 #f2 #I #L1 #L2 #V #_ #H destruct
 102 | #f1 #f2 #I #L1 #L2 #V #_ #H destruct
 103 | #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
 104 | #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
 105 ]
 106 qed-.
 107
 108 lemma lsubf_inv_atom2: ∀f1,f2,L1. ⦃L1, f1⦄ ⫃𝐅* ⦃⋆, f2⦄ →
 109                        L1 = ⋆ ∧ f1 = f2.
 110 /2 width=3 by lsubf_inv_atom2_aux/ qed-.
 111
 112 fact lsubf_inv_push2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
 113                           ∀g2,I,K2,W. f2 = ↑g2 → L2 = K2.ⓑ{I}W →
 114                           (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ↑g1 & L1 = K1.ⓑ{I}W) ∨
 115                           ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
 116                                        ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ↑g1 & L1 = K1.ⓓⓝW.V.
 117 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 118 [ #f #g2 #J #K2 #X #_ #H destruct
 119 | #f1 #f2 #I #L1 #L2 #V #HL12 #g2 #J #K2 #X #H1 #H2 destruct
 120   /3 width=5 by injective_push, ex3_2_intro, or_introl/
 121 | #f1 #f2 #I #L1 #L2 #V #_ #g2 #J #K2 #X #H elim (discr_next_push … H)
 122 | #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g2 #J #K2 #X #H1 #H2 destruct
 123   /3 width=9 by injective_push, ex6_4_intro, or_intror/
 124 | #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g2 #J #K2 #X #H elim (discr_next_push … H)
 125 ]
 126 qed-.
 127
 128 lemma lsubf_inv_push2: ∀f1,g2,I,L1,K2,W. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓑ{I}W, ↑g2⦄ →
 129                        (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ↑g1 & L1 = K1.ⓑ{I}W) ∨
 130                        ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
 131                                     ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ↑g1 & L1 = K1.ⓓⓝW.V.
 132 /2 width=5 by lsubf_inv_push2_aux/ qed-.
 133
 134 fact lsubf_inv_next2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
 135                           ∀g2,I,K2,W. f2 = ⫯g2 → L2 = K2.ⓑ{I}W →
 136                           (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ⫯g1 & L1 = K1.ⓑ{I}W) ∨
 137                           ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
 138                                        ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ⫯g1 & L1 = K1.ⓓⓝW.V.
 139 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 140 [ #f #g2 #J #K2 #X #_ #H destruct
 141 | #f1 #f2 #I #L1 #L2 #V #_ #g2 #J #K2 #X #H elim (discr_push_next … H)
 142 | #f1 #f2 #I #L1 #L2 #V #HL12 #g2 #J #K2 #X #H1 #H2 destruct
 143   /3 width=5 by injective_next, ex3_2_intro, or_introl/
 144 | #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g2 #J #K2 #X #H elim (discr_push_next … H)
 145 | #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g2 #J #K2 #X #H1 #H2 destruct
 146   /3 width=9 by injective_next, ex6_4_intro, or_intror/
 147 ]
 148 qed-.
 149
 150 lemma lsubf_inv_next2: ∀f1,g2,I,L1,K2,W. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓑ{I}W, ⫯g2⦄ →
 151                        (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ⫯g1 & L1 = K1.ⓑ{I}W) ∨
 152                        ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
 153                                     ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ⫯g1 & L1 = K1.ⓓⓝW.V.
 154 /2 width=5 by lsubf_inv_next2_aux/ qed-.
 155
 156 (* Basic properties *********************************************************)
 157
 158 lemma lsubf_refl: bi_reflexive … lsubf.
 159 #L elim L -L //
 160 #L #I #V #IH #f elim (pn_split f) * /2 width=1 by lsubf_push, lsubf_next/
 161 qed.