matita/matita/contribs/lambdadelta/basic_2/etc_new/frees_etc.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_fqup.ma".
  18 include "basic_2/static/frees.ma".
  19
  20 corec lemma sle_refl: ∀f. f ⊆ f.
  21 #f cases (pn_split f) * #g #H
  22 [ @(sle_push … H H) | @(sle_next … H H) ] -H //
  23 qed.
  24
  25 lemma sle_inv_tl1: ∀f1,f2. ⫱f1 ⊆ f2 → f1 ⊆ ⫯f2.
  26 #f1 elim (pn_split f1) * #g #H destruct
  27 /2 width=5 by sle_next, sle_weak/
  28 qed-.
  29
  30 axiom sor_tls: ∀f1,f2,f. f1 ⋓ f2 ≡ f →
  31                ∀n. ⫱*[n]f1 ⋓ ⫱*[n]f2 ≡ ⫱*[n]f.
  32
  33 axiom sor_sle1: ∀f1,f2,f. f1 ⋓ f2 ≡ f →
  34                 ∀g. g ⊆ f1 → g ⊆ f.
  35
  36 axiom sor_sle2: ∀f1,f2,f. f1 ⋓ f2 ≡ f →
  37                 ∀g. g ⊆ f2 → g ⊆ f.
  38
  39 lemma fqus_inv_refl_atom3: ∀I,G,L,X. ⦃G, L, ⓪{I}⦄ ⊐* ⦃G, L, X⦄ → ⓪{I} = X.
  40 #I #G #L #X #H elim (fqus_inv_fqup … H) -H [2: * // ]
  41 #H lapply (fqup_fwd_fw … H) -H
  42 #H elim (lt_le_false … H) -H /2 width=1 by monotonic_le_plus_r/
  43 qed-.
  44
  45 axiom drops_T_isuni_inv_refl: ∀n,L. ⬇*[n] L ≡ L → n = 0.
  46
  47 axiom fqus_split_fqu: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
  48                       (∧∧ G1 = G2 & L1 = L2 & T1 = T2) ∨
  49                       ∃∃G,L,T. ⦃G1, L1, T1⦄ ⊐ ⦃G, L, T⦄ & ⦃G, L, T⦄ ⊐* ⦃G2, L2, T2⦄.
  50
  51 axiom fqus_inv_atom1: ∀I,G1,G2,L2,T2. ⦃G1, ⋆, ⓪{I}⦄ ⊐* ⦃G2, L2, T2⦄ →
  52                       ∧∧ G1 = G2 & ⋆ = L2 & ⓪{I} = T2.
  53
  54 axiom fqus_inv_sort1: ∀G1,G2,L1,L2,T2,s. ⦃G1, L1, ⋆s⦄ ⊐* ⦃G2, L2, T2⦄ →
  55                       ∧∧ G1 = G2 & L1 = L2 & ⋆s = T2.
  56
  57 axiom fqus_inv_zero1: ∀I,G1,G2,L1,L2,V1,T2. ⦃G1, L1.ⓑ{I}V1, #0⦄ ⊐* ⦃G2, L2, T2⦄ →
  58                       (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & #0 = T2) ∨ ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄.
  59
  60 axiom fqus_inv_lref1: ∀I,G1,G2,L1,L2,V1,T2,i. ⦃G1, L1.ⓑ{I}V1, #⫯i⦄ ⊐* ⦃G2, L2, T2⦄ →
  61                       (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & #(⫯i) = T2) ∨ ⦃G1, L1, #i⦄ ⊐* ⦃G2, L2, T2⦄.
  62
  63 axiom fqus_inv_gref1: ∀G1,G2,L1,L2,T2,l. ⦃G1, L1, §l⦄ ⊐* ⦃G2, L2, T2⦄ →
  64                       ∧∧ G1 = G2 & L1 = L2 & §l = T2.
  65
  66 axiom fqus_inv_bind1: ∀p,I,G1,G2,L1,L2,V1,T1,T2. ⦃G1, L1, ⓑ{p,I}V1.T1⦄ ⊐* ⦃G2, L2, T2⦄ →
  67                       ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ{p,I}V1.T1 = T2
  68                        | ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄
  69                        | ⦃G1, L1.ⓑ{I}V1, T1⦄ ⊐* ⦃G2, L2, T2⦄.
  70
  71 axiom fqus_inv_flat1: ∀I,G1,G2,L1,L2,V1,T1,T2. ⦃G1, L1, ⓕ{I}V1.T1⦄ ⊐* ⦃G2, L2, T2⦄ →
  72                       ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓕ{I}V1.T1 = T2
  73                        | ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄
  74                        | ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄.
  75
  76 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
  77
  78 lemma frees_drops_sle: ∀f1,G,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
  79                        ∀L2,T2. ⦃G, L1, T1⦄ ⊐* ⦃G, L2, T2⦄ →
  80                        ∀I,n. ⬇*[n] L1 ≡ L2.ⓑ{I}T2 →
  81                        ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ ⫱*[⫯n] f1.
  82 #f1 #G #L1 #T1 #H elim H -f1 -L1 -T1
  83 [ #f1 #J #Hf1 #L2 #T2 #H12 #I #n #HL12
  84   elim (fqus_inv_atom1 … H12) -H12 #H1 #H2 #H3 destruct
  85   lapply (drops_fwd_lw … HL12) -HL12 #HL12
  86   elim (lt_le_false … HL12) -HL12 //
  87 | #f1 #J #L1 #V1 #s #_ #_ #L2 #T2 #H12 #I #n #HL12
  88   elim (fqus_inv_sort1 … H12) -H12 #H1 #H2 #H3 destruct
  89   lapply (drops_fwd_lw … HL12) -HL12 #HL12
  90   elim (lt_le_false … HL12) -HL12 //
  91 | #f1 #J #L1 #V1 #Hf1 #IH #L2 #T2 #H12
  92   elim (fqus_inv_zero1 … H12) -H12 [ * | #H12 #I * ]
  93   [ -IH -Hf1 #H1 #H2 #H3 #I #n #HL12 destruct
  94     lapply (drops_fwd_lw … HL12) -HL12 #HL12
  95     elim (lt_le_false … HL12) -HL12 //
  96   | -IH -H12 #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 //
  97      #H destruct /3 width=3 by sle_refl, ex2_intro/
  98   | -Hf1 #n #HL12 lapply (drops_inv_drop1 … HL12) -HL12
  99     #HL12 elim (IH … H12 … HL12) -IH -H12 -HL12 /3 width=3 by ex2_intro/
 100   ]
 101 | #f1 #J #L1 #V1 #i #Hf1 #IH #L2 #T2 #H12
 102   elim (fqus_inv_lref1 … H12) -H12 [ * | #H12 #I * ]
 103   [ -IH -Hf1 #H1 #H2 #H3 #I #n #HL12 destruct
 104     lapply (drops_fwd_lw … HL12) -HL12 #HL12
 105     elim (lt_le_false … HL12) -HL12 //
 106   | -IH #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 //
 107     #H destruct <(fqus_inv_refl_atom3 … H12) -H12 /2 width=3 by sle_refl, ex2_intro/
 108   | -Hf1 #I #HL12 lapply (drops_inv_drop1 … HL12) -HL12
 109     #HL12 elim (IH … H12 … HL12) -IH -H12 -HL12 /3 width=3 by ex2_intro/
 110   ]
 111 | #f1 #J #L1 #V1 #l #_ #_ #L2 #T2 #H12 #I #n #HL12
 112   elim (fqus_inv_gref1 … H12) -H12 #H1 #H2 #H3 destruct
 113   lapply (drops_fwd_lw … HL12) -HL12 #HL12
 114   elim (lt_le_false … HL12) -HL12 //
 115 | #f1V #f1T #f1 #p #J #L1 #V #T #_ #_ #Hf1 #IHV #IHT #L2 #T2 #H12 #I #n #HL12
 116   elim (fqus_inv_bind1 … H12) -H12 [ * |*: #H12 ]
 117   [ -IHV -IHT -Hf1 #H1 #H2 #H3 destruct
 118     lapply (drops_fwd_lw … HL12) -HL12 #HL12
 119     elim (lt_le_false … HL12) -HL12 //
 120   | -IHT elim (IHV … H12 … HL12) -IHV -H12 -HL12
 121     /4 width=6 by sor_tls, sor_sle1, ex2_intro/
 122   | -IHV elim (IHT … H12 I (⫯n)) -IHT -H12 /2 width=1 by drops_drop/ -HL12
 123     <tls_xn /4 width=6 by ex2_intro, sor_tls, sor_sle2/
 124   ]
 125 | #f1V #f1T #f1 #J #L1 #V #T #_ #_ #Hf1 #IHV #IHT #L2 #T2 #H12 #I #n #HL12
 126   elim (fqus_inv_flat1 … H12) -H12 [ * |*: #H12 ]
 127   [ -IHV -IHT -Hf1 #H1 #H2 #H3 destruct
 128     lapply (drops_fwd_lw … HL12) -HL12 #HL12
 129     elim (lt_le_false … HL12) -HL12 //
 130   | -IHT elim (IHV … H12 … HL12) -IHV -H12 -HL12
 131     /4 width=6 by sor_tls, sor_sle1, ex2_intro/
 132   | -IHV elim (IHT … H12 … HL12) -IHT -H12 -HL12
 133     /4 width=6 by ex2_intro, sor_tls, sor_sle2/
 134   ]
 135 ]
 136 qed-.