matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.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 "static_2/s_computation/fqup_weight.ma".
  16 include "static_2/static/lsubf_lsubr.ma".
  17
  18 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
  19
  20 (* Advanced properties ******************************************************)
  21
  22 (* Note: this replaces lemma 1400 concluding the "big tree" theorem *)
  23 lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅*⦃T⦄ ≘ f.
  24 #L #T @(fqup_wf_ind_eq (Ⓣ) … (⋆) L T) -L -T
  25 #G0 #L0 #T0 #IH #G #L * *
  26 [ /3 width=2 by frees_sort, ex_intro/
  27 | cases L -L /3 width=2 by frees_atom, ex_intro/
  28   #L #I *
  29   [ cases I -I #I [2: #V ] #HG #HL #HT destruct
  30     [ elim (IH G L V) -IH
  31       /3 width=2 by frees_pair, fqu_fqup, fqu_lref_O, ex_intro/
  32     | -IH /3 width=2 by frees_unit, ex_intro/
  33     ]
  34   | #i #HG #HL #HT destruct
  35     elim (IH G L (#i)) -IH
  36     /3 width=2 by frees_lref, fqu_fqup, fqu_drop, ex_intro/
  37   ]
  38 | /3 width=2 by frees_gref, ex_intro/
  39 | #p #I #V #T #HG #HL #HT destruct
  40   elim (IH G L V) // #f1 #HV
  41   elim (IH G (L.ⓑ{I}V) T) -IH // #f2 #HT
  42   elim (sor_isfin_ex f1 (⫱f2))
  43   /3 width=6 by frees_fwd_isfin, frees_bind, isfin_tl, ex_intro/
  44 | #I #V #T #HG #HL #HT destruct
  45   elim (IH G L V) // #f1 #HV
  46   elim (IH G L T) -IH // #f2 #HT
  47   elim (sor_isfin_ex f1 f2)
  48   /3 width=6 by frees_fwd_isfin, frees_flat, ex_intro/
  49 ]
  50 qed-.
  51
  52 (* Advanced main properties *************************************************)
  53
  54 theorem frees_bind_void: ∀f1,L,V. L ⊢ 𝐅*⦃V⦄ ≘ f1 → ∀f2,T. L.ⓧ ⊢ 𝐅*⦃T⦄ ≘ f2 →
  55                          ∀f. f1 ⋓ ⫱f2 ≘ f → ∀p,I. L ⊢ 𝐅*⦃ⓑ{p,I}V.T⦄ ≘ f.
  56 #f1 #L #V #Hf1 #f2 #T #Hf2 #f #Hf #p #I
  57 elim (frees_total (L.ⓑ{I}V) T) #f0 #Hf0
  58 lapply (lsubr_lsubf … Hf2 … Hf0) -Hf2 /2 width=5 by lsubr_unit/ #H02
  59 elim (pn_split f2) * #g2 #H destruct
  60 [ elim (lsubf_inv_push2 … H02) -H02 #g0 #Z #Y #H02 #H0 #H destruct
  61   lapply (lsubf_inv_refl … H02) -H02 #H02
  62   lapply (sor_eq_repl_fwd2 … Hf … H02) -g2 #Hf
  63   /2 width=5 by frees_bind/
  64 | elim (lsubf_inv_unit2 … H02) -H02 * [ #g0 #Y #_ #_ #H destruct ]
  65   #z1 #g0 #z #Z #Y #X #H02 #Hz1 #Hz #H0 #H destruct
  66   lapply (lsubf_inv_refl … H02) -H02 #H02
  67   lapply (frees_mono … Hz1 … Hf1) -Hz1 #H1
  68   lapply (sor_eq_repl_back1 … Hz … H02) -g0 #Hz
  69   lapply (sor_eq_repl_back2 … Hz … H1) -z1 #Hz
  70   lapply (sor_comm … Hz) -Hz #Hz
  71   lapply (sor_mono … f Hz ?) // -Hz #H
  72   lapply (sor_inv_sle_sn … Hf) -Hf #Hf
  73   lapply (frees_eq_repl_back … Hf0 (↑f) ?) /2 width=5 by eq_next/ -z #Hf0
  74   @(frees_bind … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
  75   /2 width=1 by sor_sle_dx/
  76 ]
  77 qed-.
  78
  79 (* Advanced inversion lemmas ************************************************)
  80
  81 lemma frees_inv_bind_void: ∀f,p,I,L,V,T. L ⊢ 𝐅*⦃ⓑ{p,I}V.T⦄ ≘ f →
  82                            ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≘ f1 & L.ⓧ ⊢ 𝐅*⦃T⦄ ≘ f2 & f1 ⋓ ⫱f2 ≘ f.
  83 #f #p #I #L #V #T #H
  84 elim (frees_inv_bind … H) -H #f1 #f2 #Hf1 #Hf2 #Hf
  85 elim (frees_total (L.ⓧ) T) #f0 #Hf0
  86 lapply (lsubr_lsubf … Hf0 … Hf2) -Hf2 /2 width=5 by lsubr_unit/ #H20
  87 elim (pn_split f0) * #g0 #H destruct
  88 [ elim (lsubf_inv_push2 … H20) -H20 #g2 #I #Y #H20 #H2 #H destruct
  89   lapply (lsubf_inv_refl … H20) -H20 #H20
  90   lapply (sor_eq_repl_back2 … Hf … H20) -g2 #Hf
  91   /2 width=5 by ex3_2_intro/
  92 | elim (lsubf_inv_unit2 … H20) -H20 * [ #g2 #Y #_ #_ #H destruct ]
  93   #z1 #z0 #g2 #Z #Y #X #H20 #Hz1 #Hg2 #H2 #H destruct
  94   lapply (lsubf_inv_refl … H20) -H20 #H0
  95   lapply (frees_mono … Hz1 … Hf1) -Hz1 #H1
  96   lapply (sor_eq_repl_back1 … Hg2 … H0) -z0 #Hg2
  97   lapply (sor_eq_repl_back2 … Hg2 … H1) -z1 #Hg2
  98   @(ex3_2_intro … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
  99   /2 width=3 by sor_comm_23_idem/
 100 ]
 101 qed-.
 102
 103 lemma frees_ind_void: ∀Q:relation3 ….
 104                       (
 105                          ∀f,L,s. 𝐈⦃f⦄ →  Q L (⋆s) f
 106                       ) → (
 107                          ∀f,i. 𝐈⦃f⦄ →  Q (⋆) (#i) (⫯*[i]↑f)
 108                       ) → (
 109                          ∀f,I,L,V.
 110                          L ⊢ 𝐅*⦃V⦄ ≘ f →  Q L V f→ Q (L.ⓑ{I}V) (#O) (↑f)
 111                       ) → (
 112                          ∀f,I,L. 𝐈⦃f⦄ →  Q (L.ⓤ{I}) (#O) (↑f)
 113                       ) → (
 114                          ∀f,I,L,i.
 115                          L ⊢ 𝐅*⦃#i⦄ ≘ f →  Q L (#i) f → Q (L.ⓘ{I}) (#(↑i)) (⫯f)
 116                       ) → (
 117                          ∀f,L,l. 𝐈⦃f⦄ →  Q L (§l) f
 118                       ) → (
 119                          ∀f1,f2,f,p,I,L,V,T.
 120                          L ⊢ 𝐅*⦃V⦄ ≘ f1 → L.ⓧ ⊢𝐅*⦃T⦄≘ f2 → f1 ⋓ ⫱f2 ≘ f →
 121                          Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ{p,I}V.T) f
 122                       ) → (
 123                          ∀f1,f2,f,I,L,V,T.
 124                          L ⊢ 𝐅*⦃V⦄ ≘ f1 → L ⊢𝐅*⦃T⦄ ≘ f2 → f1 ⋓ f2 ≘ f →
 125                          Q L V f1 → Q L T f2 → Q L (ⓕ{I}V.T) f
 126                       ) →
 127                       ∀L,T,f. L ⊢ 𝐅*⦃T⦄ ≘ f →  Q L T f.
 128 #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #L #T
 129 @(fqup_wf_ind_eq (Ⓕ) … (⋆) L T) -L -T #G0 #L0 #T0 #IH #G #L * *
 130 [ #s #HG #HL #HT #f #H destruct -IH
 131   lapply (frees_inv_sort … H) -H /2 width=1 by/
 132 | cases L -L
 133   [ #i #HG #HL #HT #f #H destruct -IH
 134     elim (frees_inv_atom … H) -H #g #Hg #H destruct /2 width=1 by/
 135   | #L #I * [ cases I -I #I [ | #V ] | #i ] #HG #HL #HT #f #H destruct
 136     [ elim (frees_inv_unit … H) -H #g #Hg #H destruct /2 width=1 by/
 137     | elim (frees_inv_pair … H) -H #g #Hg #H destruct
 138       /4 width=2 by fqu_fqup, fqu_lref_O/
 139     | elim (frees_inv_lref … H) -H #g #Hg #H destruct
 140       /4 width=2 by fqu_fqup/
 141     ]
 142   ]
 143 | #l #HG #HL #HT #f #H destruct -IH
 144   lapply (frees_inv_gref … H) -H /2 width=1 by/
 145 | #p #I #V #T #HG #HL #HT #f #H destruct
 146   elim (frees_inv_bind_void … H) -H /3 width=7 by/
 147 | #I #V #T #HG #HL #HT #f #H destruct
 148   elim (frees_inv_flat … H) -H /3 width=7 by/
 149 ]
 150 qed-.