matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lex.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 "basic_2/relocation/lex.ma".
  16 include "basic_2/relocation/drops_cext2.ma".
  17 include "basic_2/relocation/drops_sex.ma".
  18
  19 (* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
  20
  21 definition dedropable_sn: predicate … ≝
  22                           λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≘ K1 → ∀K2. K1 ⪤[R] K2 →
  23                           ∃∃L2. L1 ⪤[R] L2 & ⬇*[b, f] L2 ≘ K2 & L1 ≡[f] L2.
  24
  25 definition dropable_sn: predicate … ≝
  26                         λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≘ K1 → 𝐔⦃f⦄ → ∀L2. L1 ⪤[R] L2 →
  27                         ∃∃K2. K1 ⪤[R] K2 & ⬇*[b, f] L2 ≘ K2.
  28
  29 definition dropable_dx: predicate … ≝
  30                         λR. ∀L1,L2. L1 ⪤[R] L2 → ∀b,f,K2. ⬇*[b, f] L2 ≘ K2 → 𝐔⦃f⦄ →
  31                         ∃∃K1. ⬇*[b, f] L1 ≘ K1 & K1 ⪤[R] K2.
  32
  33 (* Properties with generic extension ****************************************)
  34
  35 (* Basic_2A1: was: lpx_sn_liftable_dedropable *)
  36 lemma lex_liftable_dedropable_sn (R): c_reflexive … R →
  37                                       d_liftable2_sn … lifts R → dedropable_sn R.
  38 #R #H1R #H2R #b #f #L1 #K1 #HLK1 #K2 * #f1 #Hf1 #HK12
  39 elim (sex_liftable_co_dedropable_sn … HLK1 … HK12) -K1
  40 /3 width=6 by cext2_d_liftable2_sn, cfull_lift_sn, ext2_refl, coafter_isid_dx, ex3_intro, ex2_intro/
  41 qed-.
  42
  43 (* Inversion lemmas with generic extension **********************************)
  44
  45 (* Basic_2A1: was: lpx_sn_deliftable_dropable *)
  46 lemma lex_dropable_sn (R): dropable_sn R.
  47 #R #b #f #L1 #K1 #HLK1 #H1f #L2 * #f2 #Hf2 #HL12
  48 elim (sex_co_dropable_sn … HLK1 … HL12) -L1
  49 /3 width=3 by coafter_isid_dx, ex2_intro/
  50 qed-.
  51
  52 (* Basic_2A1: was: lpx_sn_dropable *)
  53 lemma lex_dropable_dx (R): dropable_dx R.
  54 #R #L1 #L2 * #f2 #Hf2 #HL12 #b #f #K2 #HLK2 #Hf
  55 elim (sex_co_dropable_dx … HL12 … HLK2) -L2
  56 /3 width=5 by coafter_isid_dx, ex2_intro/
  57 qed-.
  58
  59 (* Basic_2A1: includes: lpx_sn_drop_conf *)
  60 lemma lex_drops_conf_pair (R): ∀L1,L2. L1 ⪤[R] L2 →
  61                                ∀b,f,I,K1,V1. ⬇*[b, f] L1 ≘ K1.ⓑ{I}V1 → 𝐔⦃f⦄ →
  62                                ∃∃K2,V2. ⬇*[b, f] L2 ≘ K2.ⓑ{I}V2 & K1 ⪤[R] K2 & R K1 V1 V2.
  63 #R #L1 #L2 * #f2 #Hf2 #HL12 #b #f #I #K1 #V1 #HLK1 #Hf
  64 elim (sex_drops_conf_push … HL12 … HLK1 Hf f2) -L1 -Hf
  65 [ #Z2 #K2 #HLK2 #HK12 #H
  66   elim (ext2_inv_pair_sn … H) -H #V2 #HV12 #H destruct
  67   /3 width=5 by ex3_2_intro, ex2_intro/
  68 | /3 width=3 by coafter_isid_dx, isid_push/
  69 ]
  70 qed-.
  71
  72 (* Basic_2A1: includes: lpx_sn_drop_trans *)
  73 lemma lex_drops_trans_pair (R): ∀L1,L2. L1 ⪤[R] L2 →
  74                                 ∀b,f,I,K2,V2. ⬇*[b, f] L2 ≘ K2.ⓑ{I}V2 → 𝐔⦃f⦄ →
  75                                 ∃∃K1,V1. ⬇*[b, f] L1 ≘ K1.ⓑ{I}V1 & K1 ⪤[R] K2 & R K1 V1 V2.
  76 #R #L1 #L2 * #f2 #Hf2 #HL12 #b #f #I #K2 #V2 #HLK2 #Hf
  77 elim (sex_drops_trans_push … HL12 … HLK2 Hf f2) -L2 -Hf
  78 [ #Z1 #K1 #HLK1 #HK12 #H
  79   elim (ext2_inv_pair_dx … H) -H #V1 #HV12 #H destruct
  80   /3 width=5 by ex3_2_intro, ex2_intro/
  81 | /3 width=3 by coafter_isid_dx, isid_push/
  82 ]
  83 qed-.