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/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 *)