matita/matita/contribs/lambdadelta/static_2/static/rdeq_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/rdeq_drops.ma".
  17 include "static_2/static/rdeq_fqup.ma".
  18 include "static_2/static/rdeq_rdeq.ma".
  19
  20 (* SORT-IRRELEVANT EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***)
  21
  22 (* Properties with extended structural successor for closures ***************)
  23
  24 lemma fqu_tdeq_conf: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, T1⦄ →
  25                      ∀U2. U1 ≛ U2 →
  26                      ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐[b] ⦃G2, L, T2⦄ & L2 ≛[T1] L & T1 ≛ T2.
  27 #b #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -G1 -G2 -L1 -L2 -U1 -T1
  28 [ #I #G #L #W #X #H >(tdeq_inv_lref1 … H) -X
  29   /2 width=5 by fqu_lref_O, ex3_2_intro/
  30 | #I #G #L #W1 #U1 #X #H
  31   elim (tdeq_inv_pair1 … H) -H #W2 #U2 #HW12 #_ #H destruct
  32   /2 width=5 by fqu_pair_sn, ex3_2_intro/
  33 | #p #I #G #L #W1 #U1 #X #H
  34   elim (tdeq_inv_pair1 … H) -H #W2 #U2 #HW12 #HU12 #H destruct
  35   /3 width=5 by rdeq_pair_refl, fqu_bind_dx, ex3_2_intro/
  36 | #p #I #G #L #W1 #U1 #Hb #X #H
  37   elim (tdeq_inv_pair1 … H) -H #W2 #U2 #HW12 #HU12 #H destruct
  38   /3 width=5 by fqu_clear, ex3_2_intro/
  39 | #I #G #L #W1 #U1 #X #H
  40   elim (tdeq_inv_pair1 … H) -H #W2 #U2 #_ #HU12 #H destruct
  41   /2 width=5 by fqu_flat_dx, ex3_2_intro/
  42 | #I #G #L #T1 #U1 #HTU1 #U2 #HU12
  43   elim (tdeq_inv_lifts_sn … HU12 … HTU1) -U1
  44   /3 width=5 by fqu_drop, ex3_2_intro/
  45 ]
  46 qed-.
  47
  48 lemma tdeq_fqu_trans: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, T1⦄ →
  49                       ∀U2. U2 ≛ U1 →
  50                       ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐[b] ⦃G2, L, T2⦄ & T2 ≛ T1 & L ≛[T1] L2.
  51 #b #G1 #G2 #L1 #L2 #U1 #T1 #H12 #U2 #HU21
  52 elim (fqu_tdeq_conf … H12 U2) -H12
  53 /3 width=5 by rdeq_sym, tdeq_sym, ex3_2_intro/
  54 qed-.
  55
  56 (* Basic_2A1: uses: lleq_fqu_trans *)
  57 lemma rdeq_fqu_trans: ∀b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐[b] ⦃G2, K2, U⦄ →
  58                       ∀L1. L1 ≛[T] L2 →
  59                       ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐[b] ⦃G2, K1, U0⦄ & U0 ≛ U & K1 ≛[U] K2.
  60 #b #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
  61 [ #I #G #L2 #V2 #L1 #H elim (rdeq_inv_zero_pair_dx … H) -H
  62   #K1 #V1 #HV1 #HV12 #H destruct
  63   /3 width=7 by tdeq_rdeq_conf, fqu_lref_O, ex3_2_intro/
  64 | * [ #p ] #I #G #L2 #V #T #L1 #H
  65   [ elim (rdeq_inv_bind … H)
  66   | elim (rdeq_inv_flat … H)
  67   ] -H
  68   /2 width=5 by fqu_pair_sn, ex3_2_intro/
  69 | #p #I #G #L2 #V #T #L1 #H elim (rdeq_inv_bind … H) -H
  70   /2 width=5 by fqu_bind_dx, ex3_2_intro/
  71 | #p #I #G #L2 #V #T #Hb #L1 #H elim (rdeq_inv_bind_void … H) -H
  72   /3 width=5 by fqu_clear, ex3_2_intro/
  73 | #I #G #L2 #V #T #L1 #H elim (rdeq_inv_flat … H) -H
  74   /2 width=5 by fqu_flat_dx, ex3_2_intro/
  75 | #I #G #L2 #T #U #HTU #Y #HU
  76   elim (rdeq_fwd_dx … HU) #L1 #V1 #H destruct
  77   /5 width=14 by rdeq_inv_lifts_bi, fqu_drop, drops_refl, drops_drop, ex3_2_intro/
  78 ]
  79 qed-.
  80
  81 (* Properties with optional structural successor for closures ***************)
  82
  83 lemma tdeq_fquq_trans: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, T1⦄ →
  84                        ∀U2. U2 ≛ U1 →
  85                        ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐⸮[b] ⦃G2, L, T2⦄ & T2 ≛ T1 & L ≛[T1] L2.
  86 #b #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -H
  87 [ #H #U2 #HU21 elim (tdeq_fqu_trans … H … HU21) -U1
  88   /3 width=5 by fqu_fquq, ex3_2_intro/
  89 | * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/
  90 ]
  91 qed-.
  92
  93 (* Basic_2A1: was just: lleq_fquq_trans *)
  94 lemma rdeq_fquq_trans: ∀b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐⸮[b] ⦃G2, K2, U⦄ →
  95                        ∀L1. L1 ≛[T] L2 →
  96                        ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐⸮[b] ⦃G2, K1, U0⦄ & U0 ≛ U & K1 ≛[U] K2.
  97 #b #G1 #G2 #L2 #K2 #T #U #H elim H -H
  98 [ #H #L1 #HL12 elim (rdeq_fqu_trans … H … HL12) -L2 /3 width=5 by fqu_fquq, ex3_2_intro/
  99 | * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/
 100 ]
 101 qed-.
 102
 103 (* Properties with plus-iterated structural successor for closures **********)
 104
 105 (* Basic_2A1: was just: lleq_fqup_trans *)
 106 lemma rdeq_fqup_trans: ∀b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+[b] ⦃G2, K2, U⦄ →
 107                        ∀L1. L1 ≛[T] L2 →
 108                        ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐+[b] ⦃G2, K1, U0⦄ & U0 ≛ U & K1 ≛[U] K2.
 109 #b #G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U
 110 [ #G2 #K2 #U #HTU #L1 #HL12 elim (rdeq_fqu_trans … HTU … HL12) -L2
 111   /3 width=5 by fqu_fqup, ex3_2_intro/
 112 | #G #G2 #K #K2 #U #U2 #_ #HU2 #IHTU #L1 #HL12
 113   elim (IHTU … HL12) -L2 #K0 #U0 #HTU #HU0 #HK0
 114   elim (rdeq_fqu_trans … HU2 … HK0) -K #K1 #U1 #HU1 #HU12 #HK12
 115   elim (tdeq_fqu_trans … HU1 … HU0) -U #K3 #U3 #HU03 #HU31 #HK31
 116   @(ex3_2_intro … K3 U3) (**) (* full auto too slow *)
 117   /3 width=5 by rdeq_trans, tdeq_rdeq_conf, fqup_strap1, tdeq_trans/
 118 ]
 119 qed-.
 120
 121 lemma tdeq_fqup_trans: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, T1⦄ →
 122                        ∀U2. U2 ≛ U1 →
 123                        ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐+[b] ⦃G2, L, T2⦄ & T2 ≛ T1 & L ≛[T1] L2.
 124 #b #G1 #G2 #L1 #L2 #U1 #T1 #H @(fqup_ind_dx … H) -G1 -L1 -U1
 125 [ #G1 #L1 #U1 #H #U2 #HU21 elim (tdeq_fqu_trans … H … HU21) -U1
 126   /3 width=5 by fqu_fqup, ex3_2_intro/
 127 | #G1 #G #L1 #L #U1 #U #H #_ #IH #U2 #HU21
 128   elim (tdeq_fqu_trans … H … HU21) -U1 #L0 #T #H1 #HTU #HL0
 129   lapply (tdeq_rdeq_div … HTU … HL0) -HL0 #HL0
 130   elim (IH … HTU) -U #K2 #U1 #H2 #HUT1 #HKL2
 131   elim (rdeq_fqup_trans … H2 … HL0) -L #K #U #H2 #HU1 #HK2
 132   lapply (tdeq_rdeq_conf … HUT1 … HK2) -HK2 #HK2
 133   /3 width=7 by rdeq_trans, fqup_strap2, tdeq_trans, ex3_2_intro/
 134 ]
 135 qed-.
 136
 137 (* Properties with star-iterated structural successor for closures **********)
 138
 139 lemma tdeq_fqus_trans: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, T1⦄ →
 140                        ∀U2. U2 ≛ U1 →
 141                        ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐*[b] ⦃G2, L, T2⦄ & T2 ≛ T1 & L ≛[T1] L2.
 142 #b #G1 #G2 #L1 #L2 #U1 #T1 #H #U2 #HU21 elim(fqus_inv_fqup … H) -H
 143 [ #H elim (tdeq_fqup_trans … H … HU21) -U1 /3 width=5 by fqup_fqus, ex3_2_intro/
 144 | * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/
 145 ]
 146 qed-.
 147
 148 (* Basic_2A1: was just: lleq_fqus_trans *)
 149 lemma rdeq_fqus_trans: ∀b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐*[b] ⦃G2, K2, U⦄ →
 150                        ∀L1. L1 ≛[T] L2 →
 151                        ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐*[b] ⦃G2, K1, U0⦄ & U0 ≛ U & K1 ≛[U] K2.
 152 #b #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_fqup … H) -H
 153 [ #H elim (rdeq_fqup_trans … H … HL12) -L2 /3 width=5 by fqup_fqus, ex3_2_intro/
 154 | * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/
 155 ]
 156 qed-.