matita/matita/contribs/lambdadelta/static_2/static/reqg_fqus.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/fqus_fqup.ma".
  16 include "static_2/static/reqg_drops.ma".
  17 include "static_2/static/reqg_fqup.ma".
  18 include "static_2/static/reqg_reqg.ma".
  19
  20 (* GENERIC  EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES **********)
  21
  22 (* Properties with extended structural successor for closures ***************)
  23
  24 lemma fqu_teqg_conf (S) (b):
  25       reflexive … S →
  26       ∀G1,G2,L1,L2,U1,T1. ❨G1,L1,U1❩ ⬂[b] ❨G2,L2,T1❩ →
  27       ∀U2. U1 ≛[S] U2 →
  28       ∃∃L,T2. ❨G1,L1,U2❩ ⬂[b] ❨G2,L,T2❩ & L2 ≛[S,T1] L & T1 ≛[S] T2.
  29 #S #b #HS #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -G1 -G2 -L1 -L2 -U1 -T1
  30 [ #I #G #L #W #X #H >(teqg_inv_lref1 … H) -X
  31   /3 width=5 by reqg_refl, fqu_lref_O, teqg_refl, ex3_2_intro/
  32 | #I #G #L #W1 #U1 #X #H
  33   elim (teqg_inv_pair1 … H) -H #W2 #U2 #HW12 #_ #H destruct
  34   /3 width=5 by reqg_refl, fqu_pair_sn, ex3_2_intro/
  35 | #p #I #G #L #W1 #U1 #Hb #X #H
  36   elim (teqg_inv_pair1 … H) -H #W2 #U2 #HW12 #HU12 #H destruct
  37   /3 width=5 by reqg_pair_refl, fqu_bind_dx, ex3_2_intro/
  38 | #p #I #G #L #W1 #U1 #Hb #X #H
  39   elim (teqg_inv_pair1 … H) -H #W2 #U2 #HW12 #HU12 #H destruct
  40   /3 width=5 by reqg_refl, fqu_clear, ex3_2_intro/
  41 | #I #G #L #W1 #U1 #X #H
  42   elim (teqg_inv_pair1 … H) -H #W2 #U2 #_ #HU12 #H destruct
  43   /3 width=5 by reqg_refl, fqu_flat_dx, ex3_2_intro/
  44 | #I #G #L #T1 #U1 #HTU1 #U2 #HU12
  45   elim (teqg_inv_lifts_sn … HU12 … HTU1) -U1
  46   /3 width=5 by reqg_refl, fqu_drop, ex3_2_intro/
  47 ]
  48 qed-.
  49
  50 lemma teqg_fqu_trans (S) (b):
  51       reflexive … S → symmetric … S →
  52       ∀G1,G2,L1,L2,U1,T1. ❨G1,L1,U1❩ ⬂[b] ❨G2,L2,T1❩ →
  53       ∀U2. U2 ≛[S] U1 →
  54       ∃∃L,T2. ❨G1,L1,U2❩ ⬂[b] ❨G2,L,T2❩ & T2 ≛[S] T1 & L ≛[S,T1] L2.
  55 #S #b #H1S #H2S #G1 #G2 #L1 #L2 #U1 #T1 #H12 #U2 #HU21
  56 elim (fqu_teqg_conf … H12 U2) -H12
  57 /3 width=5 by reqg_sym, teqg_sym, ex3_2_intro/
  58 qed-.
  59
  60 (* Basic_2A1: uses: lleq_fqu_trans *)
  61 lemma reqg_fqu_trans (S) (b):
  62       reflexive … S →
  63       ∀G1,G2,L2,K2,T,U. ❨G1,L2,T❩ ⬂[b] ❨G2,K2,U❩ →
  64       ∀L1. L1 ≛[S,T] L2 →
  65       ∃∃K1,U0. ❨G1,L1,T❩ ⬂[b] ❨G2,K1,U0❩ & U0 ≛[S] U & K1 ≛[S,U] K2.
  66 #S #b #HS #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
  67 [ #I #G #L2 #V2 #L1 #H elim (reqg_inv_zero_pair_dx … H) -H
  68   #K1 #V1 #HV1 #HV12 #H destruct
  69   /3 width=9 by teqg_reqg_conf_sn, fqu_lref_O, ex3_2_intro/
  70 | * [ #p ] #I #G #L2 #V #T #L1 #H
  71   [ elim (reqg_inv_bind_refl … H)
  72   | elim (reqg_inv_flat … H)
  73   ] -H
  74   /3 width=5 by fqu_pair_sn, teqg_refl, ex3_2_intro/
  75 | #p #I #G #L2 #V #T #Hb #L1 #H elim (reqg_inv_bind_refl … H) -H
  76   /3 width=5 by fqu_bind_dx, teqg_refl, ex3_2_intro/
  77 | #p #I #G #L2 #V #T #Hb #L1 #H elim (reqg_inv_bind_void … H) -H
  78   /3 width=5 by fqu_clear, teqg_refl, ex3_2_intro/
  79 | #I #G #L2 #V #T #L1 #H elim (reqg_inv_flat … H) -H
  80   /3 width=5 by fqu_flat_dx, teqg_refl, ex3_2_intro/
  81 | #I #G #L2 #T #U #HTU #Y #HU
  82   elim (reqg_fwd_dx … HU) #L1 #V1 #H destruct
  83   /5 width=14 by reqg_inv_lifts_bi, fqu_drop, teqg_refl, drops_refl, drops_drop, ex3_2_intro/
  84 ]
  85 qed-.
  86
  87 (* Properties with optional structural successor for closures ***************)
  88
  89 lemma teqg_fquq_trans (S) (b):
  90       reflexive … S → symmetric … S →
  91       ∀G1,G2,L1,L2,U1,T1. ❨G1,L1,U1❩ ⬂⸮[b] ❨G2,L2,T1❩ →
  92       ∀U2. U2 ≛[S] U1 →
  93       ∃∃L,T2. ❨G1,L1,U2❩ ⬂⸮[b] ❨G2,L,T2❩ & T2 ≛[S] T1 & L ≛[S,T1] L2.
  94 #S #b #H1S #H2S #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -H
  95 [ #H #U2 #HU21 elim (teqg_fqu_trans … H … HU21) -U1
  96   /3 width=5 by fqu_fquq, ex3_2_intro/
  97 | * #HG #HL #HT destruct /3 width=5 by reqg_refl, ex3_2_intro/
  98 ]
  99 qed-.
 100
 101 (* Basic_2A1: was just: lleq_fquq_trans *)
 102 lemma reqg_fquq_trans (S) (b):
 103       reflexive … S →
 104       ∀G1,G2,L2,K2,T,U. ❨G1,L2,T❩ ⬂⸮[b] ❨G2,K2,U❩ →
 105       ∀L1. L1 ≛[S,T] L2 →
 106       ∃∃K1,U0. ❨G1,L1,T❩ ⬂⸮[b] ❨G2,K1,U0❩ & U0 ≛[S] U & K1 ≛[S,U] K2.
 107 #S #b #HS #G1 #G2 #L2 #K2 #T #U #H elim H -H
 108 [ #H #L1 #HL12 elim (reqg_fqu_trans … H … HL12) -L2 /3 width=5 by fqu_fquq, ex3_2_intro/
 109 | * #HG #HL #HT destruct /3 width=5 by teqg_refl, ex3_2_intro/
 110 ]
 111 qed-.
 112
 113 (* Properties with plus-iterated structural successor for closures **********)
 114
 115 (* Basic_2A1: was just: lleq_fqup_trans *)
 116 lemma reqg_fqup_trans (S) (b):
 117       reflexive … S → symmetric … S → Transitive … S →
 118       ∀G1,G2,L2,K2,T,U. ❨G1,L2,T❩ ⬂+[b] ❨G2,K2,U❩ →
 119       ∀L1. L1 ≛[S,T] L2 →
 120       ∃∃K1,U0. ❨G1,L1,T❩ ⬂+[b] ❨G2,K1,U0❩ & U0 ≛[S] U & K1 ≛[S,U] K2.
 121 #S #b #H1S #H2S #H3S #G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U
 122 [ #G2 #K2 #U #HTU #L1 #HL12 elim (reqg_fqu_trans … HTU … HL12) -L2
 123   /3 width=5 by fqu_fqup, ex3_2_intro/
 124 | #G #G2 #K #K2 #U #U2 #_ #HU2 #IHTU #L1 #HL12
 125   elim (IHTU … HL12) -L2 #K0 #U0 #HTU #HU0 #HK0
 126   elim (reqg_fqu_trans … HU2 … HK0) -K // #K1 #U1 #HU1 #HU12 #HK12
 127   elim (teqg_fqu_trans … HU1 … HU0) -U // #K3 #U3 #HU03 #HU31 #HK31
 128   @(ex3_2_intro … K3 U3) (**) (* full auto too slow *)
 129   /3 width=5 by reqg_trans, teqg_reqg_conf_sn, fqup_strap1, teqg_trans/
 130 ]
 131 qed-.
 132
 133 lemma teqg_fqup_trans (S) (b):
 134       reflexive … S → symmetric … S → Transitive … S →
 135       ∀G1,G2,L1,L2,U1,T1. ❨G1,L1,U1❩ ⬂+[b] ❨G2,L2,T1❩ →
 136       ∀U2. U2 ≛[S] U1 →
 137       ∃∃L,T2. ❨G1,L1,U2❩ ⬂+[b] ❨G2,L,T2❩ & T2 ≛[S] T1 & L ≛[S,T1] L2.
 138 #S #b #H1S #H2S #H3S #G1 #G2 #L1 #L2 #U1 #T1 #H @(fqup_ind_dx … H) -G1 -L1 -U1
 139 [ #G1 #L1 #U1 #H #U2 #HU21 elim (teqg_fqu_trans … H … HU21) -U1 //
 140   /3 width=5 by fqu_fqup, ex3_2_intro/
 141 | #G1 #G #L1 #L #U1 #U #H #_ #IH #U2 #HU21
 142   elim (teqg_fqu_trans … H … HU21) -U1 // #L0 #T #H1 #HTU #HL0
 143   lapply (teqg_reqg_div … HTU … HL0) -HL0 // #HL0
 144   elim (IH … HTU) -U #K2 #U1 #H2 #HUT1 #HKL2
 145   elim (reqg_fqup_trans … H2 … HL0) -L // #K #U #H2 #HU1 #HK2
 146   lapply (teqg_reqg_conf_sn … HUT1 … HK2) -HK2 // #HK2
 147   /3 width=7 by reqg_trans, fqup_strap2, teqg_trans, ex3_2_intro/
 148 ]
 149 qed-.
 150
 151 (* Properties with star-iterated structural successor for closures **********)
 152
 153 lemma teqg_fqus_trans (S) (b):
 154       reflexive … S → symmetric … S → Transitive … S →
 155       ∀G1,G2,L1,L2,U1,T1. ❨G1,L1,U1❩ ⬂*[b] ❨G2,L2,T1❩ →
 156       ∀U2. U2 ≛[S] U1 →
 157       ∃∃L,T2. ❨G1,L1,U2❩ ⬂*[b] ❨G2,L,T2❩ & T2 ≛[S] T1 & L ≛[S,T1] L2.
 158 #S #b #H1S #H2S #H3S #G1 #G2 #L1 #L2 #U1 #T1 #H #U2 #HU21 elim(fqus_inv_fqup … H) -H
 159 [ #H elim (teqg_fqup_trans … H … HU21) -U1 /3 width=5 by fqup_fqus, ex3_2_intro/
 160 | * #HG #HL #HT destruct /3 width=5 by reqg_refl, ex3_2_intro/
 161 ]
 162 qed-.
 163
 164 (* Basic_2A1: was just: lleq_fqus_trans *)
 165 lemma reqg_fqus_trans (S) (b):
 166       reflexive … S → symmetric … S → Transitive … S →
 167       ∀G1,G2,L2,K2,T,U. ❨G1,L2,T❩ ⬂*[b] ❨G2,K2,U❩ →
 168       ∀L1. L1 ≛[S,T] L2 →
 169       ∃∃K1,U0. ❨G1,L1,T❩ ⬂*[b] ❨G2,K1,U0❩ & U0 ≛[S] U & K1 ≛[S,U] K2.
 170 #S #b #H1S #H2S #H3S #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_fqup … H) -H
 171 [ #H elim (reqg_fqup_trans … H … HL12) -L2 /3 width=5 by fqup_fqus, ex3_2_intro/
 172 | * #HG #HL #HT destruct /3 width=5 by teqg_refl, ex3_2_intro/
 173 ]
 174 qed-.