matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_fquq.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_transition/fquq.ma".
  16 include "basic_2/rt_transition/lpx.ma".
  17
  18 (* UNBOUND PARALLEL RT-TRANSITION FOR FULL LOCAL ENVIRONMENTS ***************)
  19
  20 (* Properties with extended structural successor for closures ***************)
  21
  22 lemma lpx_fqu_trans (b):
  23       ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ →
  24       ∀K1. ❪G1,K1❫ ⊢ ⬈ L1 →
  25       ∃∃K2,T. ❪G1,K1❫ ⊢ T1 ⬈ T & ❪G1,K1,T❫ ⬂[b] ❪G2,K2,T2❫ & ❪G2,K2❫ ⊢ ⬈ L2.
  26 #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
  27 [ #I #G #K #V #K1 #H
  28   elim (lpx_inv_pair_dx … H) -H #K0 #V0 #HK0 #HV0 #H destruct
  29   elim (lifts_total V (𝐔❨1❩)) #T #HVT
  30   /3 width=5 by cpx_delta, fqu_drop, ex3_2_intro/
  31 | /3 width=5 by cpx_pair_sn, fqu_pair_sn, ex3_2_intro/
  32 | /3 width=5 by lpx_bind_refl_dx, cpx_pair_sn, fqu_bind_dx, ex3_2_intro/
  33 | /3 width=5 by lpx_bind_refl_dx, cpx_pair_sn, fqu_clear, ex3_2_intro/
  34 | /3 width=5 by cpx_pair_sn, fqu_flat_dx, ex3_2_intro/
  35 | #I #G #K #T #U #HTU #K1 #H
  36   elim (lpx_inv_bind_dx … H) -H #I0 #K0 #HK0 #HI0 #H destruct
  37   /3 width=5 by fqu_drop, ex3_2_intro/
  38 ]
  39 qed-.
  40
  41 lemma fqu_lpx_trans (b):
  42       ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ →
  43       ∀K2. ❪G2,L2❫ ⊢ ⬈ K2 →
  44       ∃∃K1,T. ❪G1,L1❫ ⊢ ⬈ K1 & ❪G1,L1❫ ⊢ T1 ⬈ T & ❪G1,K1,T❫ ⬂[b] ❪G2,K2,T2❫.
  45 #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
  46 [ /3 width=5 by lpx_bind_refl_dx, fqu_lref_O, ex3_2_intro/
  47 | /3 width=5 by cpx_pair_sn, fqu_pair_sn, ex3_2_intro/
  48 | #p #I #G2 #L2 #V2 #T2 #Hb #X #H
  49   elim (lpx_inv_pair_sn … H) -H #K2 #W2 #HLK2 #HVW2 #H destruct
  50   /3 width=5 by cpx_pair_sn, fqu_bind_dx, ex3_2_intro/
  51 | #p #I #G2 #L2 #V2 #T2 #Hb #X #H
  52   elim (lpx_inv_unit_sn … H) -H #K2 #HLK2 #H destruct
  53   /3 width=5 by cpx_pair_sn, fqu_clear, ex3_2_intro/
  54 | /3 width=5 by cpx_pair_sn, fqu_flat_dx, ex3_2_intro/
  55 | /3 width=5 by lpx_bind_refl_dx, fqu_drop, ex3_2_intro/
  56 ]
  57 qed-.
  58
  59 (* Properties with extended optional structural successor for closures ******)
  60
  61 lemma lpx_fquq_trans (b):
  62       ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂⸮[b] ❪G2,L2,T2❫ →
  63       ∀K1. ❪G1,K1❫ ⊢ ⬈ L1 →
  64       ∃∃K2,T. ❪G1,K1❫ ⊢ T1 ⬈ T & ❪G1,K1,T❫ ⬂⸮[b] ❪G2,K2,T2❫ & ❪G2,K2❫ ⊢ ⬈ L2.
  65 #b #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 cases H -H
  66 [ #H12 elim (lpx_fqu_trans … H12 … HKL1) -L1 /3 width=5 by fqu_fquq, ex3_2_intro/
  67 | * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
  68 ]
  69 qed-.
  70
  71 lemma fquq_lpx_trans (b):
  72       ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂⸮[b] ❪G2,L2,T2❫ →
  73       ∀K2. ❪G2,L2❫ ⊢ ⬈ K2 →
  74       ∃∃K1,T. ❪G1,L1❫ ⊢ ⬈ K1 & ❪G1,L1❫ ⊢ T1 ⬈ T & ❪G1,K1,T❫ ⬂⸮[b] ❪G2,K2,T2❫.
  75 #b #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 cases H -H
  76 [ #H12 elim (fqu_lpx_trans … H12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/
  77 | * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
  78 ]
  79 qed-.