matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.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/rt_computation/fpbg_fpbs.ma".
  16 include "basic_2/rt_computation/fsb_feqx.ma".
  17
  18 (* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************)
  19
  20 (* Properties with parallel rst-computation for closures ********************)
  21
  22 lemma fsb_fpbs_trans:
  23       ∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
  24       ∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫.
  25 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
  26 #G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
  27 elim (fpbs_inv_fpbg … H12) -H12
  28 [ -IH /2 width=5 by fsb_feqx_trans/
  29 | -H1 * /2 width=5 by/
  30 ]
  31 qed-.
  32
  33 (* Properties with proper parallel rst-computation for closures *************)
  34
  35 lemma fsb_intro_fpbg:
  36       ∀G1,L1,T1.
  37       (∀G2,L2,T2. ❪G1,L1,T1❫ > ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫) →
  38       ≥𝐒 ❪G1,L1,T1❫.
  39 /4 width=1 by fsb_intro, fpb_fpbg/ qed.
  40
  41 (* Eliminators with proper parallel rst-computation for closures ************)
  42
  43 lemma fsb_ind_fpbg_fpbs (Q:relation3 …):
  44       (∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
  45         (∀G2,L2,T2. ❪G1,L1,T1❫ > ❪G2,L2,T2❫ → Q G2 L2 T2) →
  46         Q G1 L1 T1
  47       ) →
  48       ∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
  49       ∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → Q G2 L2 T2.
  50 #Q #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
  51 #G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
  52 @IH1 -IH1
  53 [ -IH /2 width=5 by fsb_fpbs_trans/
  54 | -H1 #G0 #L0 #T0 #H10
  55   elim (fpbs_fpbg_trans … H12 … H10) -G2 -L2 -T2
  56   /2 width=5 by/
  57 ]
  58 qed-.
  59
  60 lemma fsb_ind_fpbg (Q:relation3 …):
  61       (∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
  62         (∀G2,L2,T2. ❪G1,L1,T1❫ > ❪G2,L2,T2❫ → Q G2 L2 T2) →
  63         Q G1 L1 T1
  64       ) →
  65       ∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →  Q G1 L1 T1.
  66 #Q #IH #G1 #L1 #T1 #H @(fsb_ind_fpbg_fpbs … H) -H
  67 /3 width=1 by/
  68 qed-.
  69
  70 (* Inversion lemmas with proper parallel rst-computation for closures *******)
  71
  72 lemma fsb_fpbg_refl_false (G) (L) (T):
  73       ≥𝐒 ❪G,L,T❫ → ❪G,L,T❫ > ❪G,L,T❫ → ⊥.
  74 #G #L #T #H
  75 @(fsb_ind_fpbg … H) -G -L -T #G1 #L1 #T1 #_ #IH #H
  76 /2 width=5 by/
  77 qed-.