matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpx_reqx.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 "static_2/static/reqx_req.ma".
  16 include "basic_2/rt_transition/rpx_reqx.ma".
  17 include "basic_2/rt_transition/rpx_lpx.ma".
  18
  19 (* EXTENDED PARALLEL RT-TRANSITION FOR FULL LOCAL ENVIRONMENTS **************)
  20
  21 (* Properties with sort-irrelevant equivalence for local environments *******)
  22
  23 lemma reqx_lpx_trans_rpx (G) (L) (T:term):
  24       ∀L1. L1 ≛[T] L → ∀L2. ❪G,L❫ ⊢ ⬈ L2 → ❪G,L❫ ⊢ ⬈[T] L2.
  25 /3 width=1 by lpx_rpx, reqx_rpx_trans/ qed.
  26
  27 (* Basic_2A1: uses: lleq_lpx_trans *)
  28 lemma reqx_lpx_trans (G):
  29       ∀L2,K2. ❪G,L2❫ ⊢ ⬈ K2 → ∀L1. ∀T:term. L1 ≛[T] L2 →
  30       ∃∃K1. ❪G,L1❫ ⊢ ⬈ K1 & K1 ≛[T] K2.
  31 #G #L2 #K2 #HLK2 #L1 #T #HL12
  32 lapply (lpx_rpx … T … HLK2) -HLK2 #HLK2
  33 lapply (reqx_rpx_trans … HL12 … HLK2) -L2 #H
  34 elim (rpx_fwd_lpx_req … H) -H #K1 #HLK1 #HK12
  35 /3 width=3 by req_reqx, ex2_intro/
  36 qed-.
  37
  38 (* Inversion lemmas with sort-irrelevant equivalence for local environments *)
  39
  40 lemma rpx_inv_reqx_lpx (G) (T):
  41       ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 →
  42       ∃∃L. L1 ≛[T] L & ❪G,L❫ ⊢ ⬈ L2.
  43 #G #T #L1 #L2 #H
  44 elim (rpx_inv_req_lpx … H) -H #L #HL1 #HL2
  45 /3 width=3 by req_reqx, ex2_intro/
  46 qed-.
  47
  48 (* Forward lemmas with sort-irrelevant equivalence for local environments ***)
  49
  50 lemma rpx_fwd_lpx_reqx (G) (T):
  51       ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 →
  52       ∃∃L. ❪G,L1❫ ⊢ ⬈ L & L ≛[T] L2.
  53 #G #T #L1 #L2 #H
  54 elim (rpx_fwd_lpx_req … H) -H #L #HL1 #HL2
  55 /3 width=3 by req_reqx, ex2_intro/
  56 qed-.