matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.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 "ground_2/lib/star.ma".
  16 include "static_2/notation/relations/suptermplus_6.ma".
  17 include "static_2/notation/relations/suptermplus_7.ma".
  18 include "static_2/s_transition/fqu.ma".
  19
  20 (* PLUS-ITERATED SUPCLOSURE *************************************************)
  21
  22 definition fqup: bool → tri_relation genv lenv term ≝
  23                  λb. tri_TC … (fqu b).
  24
  25 interpretation "extended plus-iterated structural successor (closure)"
  26    'SupTermPlus b G1 L1 T1 G2 L2 T2 = (fqup b G1 L1 T1 G2 L2 T2).
  27
  28 interpretation "plus-iterated structural successor (closure)"
  29    'SupTermPlus G1 L1 T1 G2 L2 T2 = (fqup true G1 L1 T1 G2 L2 T2).
  30
  31 (* Basic properties *********************************************************)
  32
  33 lemma fqu_fqup: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ →
  34                 ⦃G1,L1,T1⦄ ⬂+[b] ⦃G2,L2,T2⦄.
  35 /2 width=1 by tri_inj/ qed.
  36
  37 lemma fqup_strap1: ∀b,G1,G,G2,L1,L,L2,T1,T,T2.
  38                    ⦃G1,L1,T1⦄ ⬂+[b] ⦃G,L,T⦄ → ⦃G,L,T⦄ ⬂[b] ⦃G2,L2,T2⦄ →
  39                    ⦃G1,L1,T1⦄ ⬂+[b] ⦃G2,L2,T2⦄.
  40 /2 width=5 by tri_step/ qed.
  41
  42 lemma fqup_strap2: ∀b,G1,G,G2,L1,L,L2,T1,T,T2.
  43                    ⦃G1,L1,T1⦄ ⬂[b] ⦃G,L,T⦄ → ⦃G,L,T⦄ ⬂+[b] ⦃G2,L2,T2⦄ →
  44                    ⦃G1,L1,T1⦄ ⬂+[b] ⦃G2,L2,T2⦄.
  45 /2 width=5 by tri_TC_strap/ qed.
  46
  47 lemma fqup_pair_sn: ∀b,I,G,L,V,T. ⦃G,L,②{I}V.T⦄ ⬂+[b] ⦃G,L,V⦄.
  48 /2 width=1 by fqu_pair_sn, fqu_fqup/ qed.
  49
  50 lemma fqup_bind_dx: ∀p,I,G,L,V,T. ⦃G,L,ⓑ{p,I}V.T⦄ ⬂+[Ⓣ] ⦃G,L.ⓑ{I}V,T⦄.
  51 /3 width=1 by fqu_bind_dx, fqu_fqup/ qed.
  52
  53 lemma fqup_clear: ∀p,I,G,L,V,T. ⦃G,L,ⓑ{p,I}V.T⦄ ⬂+[Ⓕ] ⦃G,L.ⓧ,T⦄.
  54 /3 width=1 by fqu_clear, fqu_fqup/ qed.
  55
  56 lemma fqup_flat_dx: ∀b,I,G,L,V,T. ⦃G,L,ⓕ{I}V.T⦄ ⬂+[b] ⦃G,L,T⦄.
  57 /2 width=1 by fqu_flat_dx, fqu_fqup/ qed.
  58
  59 lemma fqup_flat_dx_pair_sn: ∀b,I1,I2,G,L,V1,V2,T. ⦃G,L,ⓕ{I1}V1.②{I2}V2.T⦄ ⬂+[b] ⦃G,L,V2⦄.
  60 /2 width=5 by fqu_pair_sn, fqup_strap1/ qed.
  61
  62 lemma fqup_bind_dx_flat_dx: ∀p,G,I1,I2,L,V1,V2,T. ⦃G,L,ⓑ{p,I1}V1.ⓕ{I2}V2.T⦄ ⬂+[Ⓣ] ⦃G,L.ⓑ{I1}V1,T⦄.
  63 /2 width=5 by fqu_flat_dx, fqup_strap1/ qed.
  64
  65 lemma fqup_flat_dx_bind_dx: ∀p,I1,I2,G,L,V1,V2,T. ⦃G,L,ⓕ{I1}V1.ⓑ{p,I2}V2.T⦄ ⬂+[Ⓣ] ⦃G,L.ⓑ{I2}V2,T⦄.
  66 /3 width=5 by fqu_bind_dx, fqup_strap1/ qed.
  67
  68 (* Basic eliminators ********************************************************)
  69
  70 lemma fqup_ind: ∀b,G1,L1,T1. ∀Q:relation3 ….
  71                 (∀G2,L2,T2. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ → Q G2 L2 T2) →
  72                 (∀G,G2,L,L2,T,T2. ⦃G1,L1,T1⦄ ⬂+[b] ⦃G,L,T⦄ → ⦃G,L,T⦄ ⬂[b] ⦃G2,L2,T2⦄ → Q G L T → Q G2 L2 T2) →
  73                 ∀G2,L2,T2. ⦃G1,L1,T1⦄ ⬂+[b] ⦃G2,L2,T2⦄ → Q G2 L2 T2.
  74 #b #G1 #L1 #T1 #Q #IH1 #IH2 #G2 #L2 #T2 #H
  75 @(tri_TC_ind … IH1 IH2 G2 L2 T2 H)
  76 qed-.
  77
  78 lemma fqup_ind_dx: ∀b,G2,L2,T2. ∀Q:relation3 ….
  79                    (∀G1,L1,T1. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ → Q G1 L1 T1) →
  80                    (∀G1,G,L1,L,T1,T. ⦃G1,L1,T1⦄ ⬂[b] ⦃G,L,T⦄ → ⦃G,L,T⦄ ⬂+[b] ⦃G2,L2,T2⦄ → Q G L T → Q G1 L1 T1) →
  81                    ∀G1,L1,T1. ⦃G1,L1,T1⦄ ⬂+[b] ⦃G2,L2,T2⦄ → Q G1 L1 T1.
  82 #b #G2 #L2 #T2 #Q #IH1 #IH2 #G1 #L1 #T1 #H
  83 @(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H)
  84 qed-.
  85
  86 (* Advanced properties ******************************************************)
  87
  88 lemma fqup_zeta (b) (p) (I) (G) (K) (V):
  89                 ∀T1,T2. ⇧*[1]T2 ≘ T1 → ⦃G,K,ⓑ{p,I}V.T1⦄ ⬂+[b] ⦃G,K,T2⦄.
  90 * /4 width=5 by fqup_strap2, fqu_fqup, fqu_drop, fqu_clear, fqu_bind_dx/ qed.
  91
  92 (* Basic_2A1: removed theorems 1: fqup_drop *)