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