matita/matita/contribs/lambdadelta/basic_2/etc_new/lfpr_main.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 "basic_2/rt_transition/lfpr_lfpr.ma".
  16
  17 (* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************)
  18
  19 definition lfxs_confluent_R: relation2 … ≝
  20                              λRP1,RP2.
  21                              ∀L0,T0,T1. RP1 L0 T0 T1 → ∀T2. RP2 L0 T0 T2 →
  22                              ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 →
  23                              ∃∃L. L1 ⦻*[RP2, T1] L & L2 ⦻*[RP1, T2] L.
  24
  25 (* Main properties **********************************************************)
  26
  27 fact lfpr_conf_cpr_atom_atom:
  28    ∀h,I,G,L0. (
  29       ∀L,T. ⦃G, L0, ⓪{I}⦄ ⊐+ ⦃G, L, T⦄ →
  30       ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
  31       ∀L1. ⦃G, L⦄ ⊢ ➡[h, T] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h, T] L2 →
  32       ∃∃K0. ⦃G, L1⦄ ⊢ ➡[h, T1] K0 & ⦃G, L2⦄ ⊢ ➡[h, T2] K0
  33    ) →
  34    ∀L1. ⦃G, L0⦄ ⊢ ➡[h, ⓪{I}] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h, ⓪{I}] L2 →
  35    ∃∃L. ⦃G, L1⦄ ⊢ ➡[h, ⓪{I}] L & ⦃G, L2⦄ ⊢ ➡[h, ⓪{I}] L.
  36 #h #I #G * [ | #K0 #J #V0 cases I -I [ | * | ] ]
  37 [ #_ #L1 #HL01 #L2 #HL02
  38   lapply (lfpr_inv_atom_sn … HL01) -HL01 #H destruct
  39   lapply (lfpr_inv_atom_sn … HL02) -HL02 #H destruct
  40   /2 width=3 by ex2_intro/
  41 | #s #IH #L1 #HL01 #L2 #HL02
  42   elim (lfxs_inv_sort_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #H destruct
  43   elim (lfxs_inv_sort_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #H destruct
  44   elim (IH …  HK01 … HK02) -IH -HK01 -HK02
  45   /3 width=5 by lfpr_sort, fqu_fqup, fqu_drop, ex2_intro/
  46 | #IH #L1 #HL01 #L2 #HL02
  47   elim (lfpr_inv_zero_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #HV01 #H destruct
  48   elim (lfpr_inv_zero_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #HV02 #H destruct
  49   elim (cpr_conf_lfpr … HV01 … HV02 … HK01 … HK02) #V #HV1 #HV2
  50   elim (IH … HV01 … HV02 … HK01 … HK02) -IH -HV01 -HV02 -HK01 -HK02
  51   /3 width=5 by lfpr_zero, fqu_fqup, fqu_drop, ex2_intro/
  52 | #i #IH #L1 #HL01 #L2 #HL02
  53   elim (lfxs_inv_lref_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #H destruct
  54   elim (lfxs_inv_lref_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #H destruct
  55   elim (IH …  HK01 … HK02) -IH -HK01 -HK02
  56   /3 width=5 by lfpr_lref, fqu_fqup, fqu_drop, ex2_intro/
  57 | #l #IH #L1 #HL01 #L2 #HL02
  58   elim (lfxs_inv_gref_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #H destruct
  59   elim (lfxs_inv_gref_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #H destruct
  60   elim (IH …  HK01 … HK02) -IH -HK01 -HK02
  61   /3 width=5 by lfpr_gref, fqu_fqup, fqu_drop, ex2_intro/
  62 ]
  63 qed-.
  64
  65 theorem lfpr_conf_cpr: ∀h,G. lfxs_confluent_R (cpm 0 h G) (cpm 0 h G).
  66 #h #G #L0 #T0 @(fqup_wf_ind_eq … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ]
  67 [ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
  68   elim (cpr_inv_atom1_drops … H1) -H1
  69   elim (cpr_inv_atom1_drops … H2) -H2
  70   [ #H2 #H1 destruct
  71     /3 width=7 by lfpr_conf_cpr_atom_atom/
  72   | * #K0 #V0 #V2 * [2: #i2 ] #HLK0 #HV02 #HVT2 #H2 #H1 destruct
  73
  74 (*
  75
  76 theorem lpr_conf: ∀G. confluent … (lpr G).
  77 /3 width=6 by lpx_sn_conf, cpr_conf_lpr/
  78 qed-.
  79
  80 *)