matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_fqus.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/relocation/drops_weight.ma".
  16 include "basic_2/s_computation/fqup_weight.ma".
  17 include "basic_2/s_computation/fqus_weight.ma".
  18 include "basic_2/static/frees.ma".
  19
  20 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
  21
  22 (* Properties with star-iterated supclosure *********************************)
  23
  24 (* Note: Restrict fqu_drop on atoms to prove frees_fqus_drops
  25          Counterex: ⦃⋆, ⋆.ⓛ#0, ⓛ#1.#0⦄ ⊐ ⦃⋆, ⋆, ⓛ#0.#0⦄ ⊐ ⦃⋆, ⋆.ⓛ#0, #0⦄
  26 *)
  27 lemma frees_fqus_drops: ∀G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
  28                         ∀L2,T2. ⦃G, L1, T1⦄ ⊐* ⦃G, L2, T2⦄ →
  29                         ∀I,n. ⬇*[n] L1 ≡ L2.ⓑ{I}T2 →
  30                         ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ ⫱*[⫯n] f1.
  31 #G #L1 #T1 @(fqup_wf_ind_eq … G L1 T1) -G -L1 -T1
  32 #G0 #L0 #T0 #IH #G #L1 * *
  33 [ #s #HG #HL #HT #f1 #Hf1 #L2 #T2 #H12 #I #n #HL12 destruct
  34   lapply (frees_inv_sort … Hf1) -Hf1 #Hf1
  35   elim (fqus_inv_sort1 … H12) -H12 * [| elim (nat_split n) ]
  36   [ -IH #H1 #H2 #H3 destruct
  37     lapply (drops_fwd_lw … HL12) -HL12 #HL12
  38     elim (lt_le_false … HL12) -HL12 //
  39   | -IH #Hn #J #L #V #H12 #H destruct
  40     lapply (drops_fwd_isid … HL12 ?) -HL12 // #H destruct
  41     <(fqus_inv_refl_atom3 … H12) -H12
  42     /3 width=3 by frees_sort_gen, sle_isid_sn, ex2_intro/
  43   | * #m #Hn #J #L #V #H12 #H destruct
  44     lapply (drops_inv_drop1 … HL12) -HL12 #HL12
  45     elim (IH … H12 … HL12) -IH -H12 -HL12
  46     /3 width=3 by frees_sort_gen, fqu_fqup, fqu_drop, lifts_sort, isid_tl, ex2_intro/
  47   ]
  48 | #i #HG #HL #HT #f1 #Hf1 #L2 #T2 #H12 #I #n #HL12 destruct
  49   elim (fqus_inv_lref1 … H12) -H12 * [|2,3: elim (nat_split n) ]
  50   [ -IH #H1 #H2 #H3 destruct
  51     lapply (drops_fwd_lw … HL12) -HL12 #HL12
  52     elim (lt_le_false … HL12) -HL12 //
  53   | -IH #Hn #J #L #V #H12 #H1 #H2 destruct
  54     elim (frees_inv_zero_pair … Hf1) -Hf1 #g1 #Hg1 #H destruct
  55     lapply (drops_fwd_isid … HL12 ?) -HL12 -H12 // #H destruct
  56     /2 width=3 by sle_refl, ex2_intro/
  57   | * #m #Hn #J #L #V #H12 #H1 #H2 destruct
  58     elim (frees_inv_zero_pair … Hf1) -Hf1 #g1 #Hg1 #H destruct
  59     lapply (drops_inv_drop1 … HL12) -HL12 #HL12
  60     elim (IH … H12 … HL12) -IH -H12 -HL12
  61     /2 width=3 by fqu_fqup, fqu_lref_O, ex2_intro/
  62   | -IH #Hn #J #L #V #j #H12 #H1 #H2 destruct
  63     elim (frees_inv_lref_pair … Hf1) -Hf1 #g1 #Hg1 #H destruct
  64     lapply (drops_fwd_isid … HL12 ?) -HL12 // #H destruct
  65     <(fqus_inv_refl_atom3 … H12) -H12 /2 width=3 by sle_refl, ex2_intro/
  66   | * #m #Hn #J #L #V #j #H12 #H1 #H2 destruct
  67     elim (frees_inv_lref_pair … Hf1) -Hf1 #g1 #Hg1 #H destruct
  68     lapply (drops_inv_drop1 … HL12) -HL12 #HL12
  69     elim (IH … H12 … HL12) -IH -H12 -HL12 /2 width=3 by fqu_fqup, ex2_intro/
  70   ]
  71 | #l #HG #HL #HT #f1 #Hf1 #L2 #T2 #H12 #I #n #HL12 destruct
  72   lapply (frees_inv_gref … Hf1) -Hf1 #Hf1
  73   elim (fqus_inv_gref1 … H12) -H12 * [| elim (nat_split n) ]
  74   [ -IH #H1 #H2 #H3 destruct
  75     lapply (drops_fwd_lw … HL12) -HL12 #HL12
  76     elim (lt_le_false … HL12) -HL12 //
  77   | -IH #Hn #J #L #V #H12 #H destruct
  78     lapply (drops_fwd_isid … HL12 ?) -HL12 // #H destruct
  79     <(fqus_inv_refl_atom3 … H12) -H12
  80     /3 width=3 by frees_gref_gen, sle_isid_sn, ex2_intro/
  81   | * #m #Hn #J #L #V #H12 #H destruct
  82     lapply (drops_inv_drop1 … HL12) -HL12 #HL12
  83     elim (IH … H12 … HL12) -IH -H12 -HL12
  84     /3 width=3 by frees_gref_gen, fqu_fqup, fqu_drop, lifts_sort, isid_tl, ex2_intro/
  85   ]
  86 | #p #I #V1 #T1 #HG #HL #HT #f1 #Hf1 #L2 #T2 #H12 #I #n #HL12 destruct
  87   elim (frees_inv_bind … Hf1) -Hf1 #f1V #f1T #Hf1V #Hf1T #Hf1
  88   elim (fqus_inv_bind1 … H12) -H12
  89   [ -IH -f1V -f1T * #H1 #H2 #H3 destruct
  90     lapply (drops_fwd_lw … HL12) -HL12 #HL12
  91     elim (lt_le_false … HL12) -HL12 //
  92   | #H12 elim (IH … H12 … HL12) -IH -H12 -HL12
  93     /4 width=6 by sor_tls, sor_inv_sle_sn_trans, ex2_intro/
  94   | #H12 elim (IH … H12 I (⫯n)) -IH -H12 [|*: /2 width=3 by drops_drop, drops_refl/ ] -HL12
  95     <tls_xn /4 width=6 by ex2_intro, sor_tls, sor_inv_sle_dx_trans/
  96   | * #J #L #V #X1 #H12 #HXT1 #H destruct
  97   ]
  98 | #I #V1 #T1 #HG #HL #HT #f1 #Hf1 #L2 #T2 #H12 #I #n #HL12 destruct
  99   elim (frees_inv_flat … Hf1) -Hf1 #f1V #f1T #Hf1V #Hf1T #Hf1
 100   elim (fqus_inv_flat1 … H12) -H12
 101   [ -IH -f1V -f1T * #H1 #H2 #H3 destruct
 102     lapply (drops_fwd_lw … HL12) -HL12 #HL12
 103     elim (lt_le_false … HL12) -HL12 //
 104   | #H12 elim (IH … H12 … HL12) -IH -H12 -HL12
 105     /4 width=6 by sor_tls, sor_inv_sle_sn_trans, ex2_intro/
 106   | #H12 elim (IH … H12 … HL12) -IH -H12 -HL12
 107     /4 width=6 by ex2_intro, sor_tls, sor_inv_sle_dx_trans/
 108   | * #J #L #V #X1 #H12 #HXT1 #H destruct
 109   ]
 110 ]
 111 qed-.