matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_fqu.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 "static_2/s_transition/fqu_weight.ma".
  16 include "basic_2/rt_transition/cpt.ma".
  17
  18 (* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
  19
  20 (* Basic eliminators ********************************************************)
  21
  22 lemma cpt_ind (h) (Q:relation5 …):
  23       (∀I,G,L. Q 0 G L (⓪[I]) (⓪[I])) →
  24       (∀G,L,s. Q 1 G L (⋆s) (⋆(⫯[h]s))) →
  25       (∀n,G,K,V1,V2,W2. ❪G,K❫ ⊢ V1 ⬆[h,n] V2 → Q n G K V1 V2 →
  26         ⇧*[1] V2 ≘ W2 → Q n G (K.ⓓV1) (#0) W2
  27       ) → (∀n,G,K,V1,V2,W2. ❪G,K❫ ⊢ V1 ⬆[h,n] V2 → Q n G K V1 V2 →
  28         ⇧*[1] V2 ≘ W2 → Q (↑n) G (K.ⓛV1) (#0) W2
  29       ) → (∀n,I,G,K,T,U,i. ❪G,K❫ ⊢ #i ⬆[h,n] T → Q n G K (#i) T →
  30         ⇧*[1] T ≘ U → Q n G (K.ⓘ[I]) (#↑i) (U)
  31       ) → (∀n,p,I,G,L,V1,V2,T1,T2. ❪G,L❫ ⊢ V1 ⬆[h,0] V2 → ❪G,L.ⓑ[I]V1❫ ⊢ T1 ⬆[h,n] T2 →
  32         Q 0 G L V1 V2 → Q n G (L.ⓑ[I]V1) T1 T2 → Q n G L (ⓑ[p,I]V1.T1) (ⓑ[p,I]V2.T2)
  33       ) → (∀n,G,L,V1,V2,T1,T2. ❪G,L❫ ⊢ V1 ⬆[h,0] V2 → ❪G,L❫ ⊢ T1 ⬆[h,n] T2 →
  34         Q 0 G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓐV1.T1) (ⓐV2.T2)
  35       ) → (∀n,G,L,V1,V2,T1,T2. ❪G,L❫ ⊢ V1 ⬆[h,n] V2 → ❪G,L❫ ⊢ T1 ⬆[h,n] T2 →
  36         Q n G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓝV1.T1) (ⓝV2.T2)
  37       ) → (∀n,G,L,V1,V2,T. ❪G,L❫ ⊢ V1 ⬆[h,n] V2 →
  38         Q n G L V1 V2 → Q (↑n) G L (ⓝV1.T) V2
  39       ) →
  40       ∀n,G,L,T1,T2. ❪G,L❫ ⊢ T1 ⬆[h,n] T2 → Q n G L T1 T2.
  41 #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #n #G #L #T1
  42 generalize in match n; -n
  43 @(fqu_wf_ind (Ⓣ) … G L T1) -G -L -T1 #G0 #L0 * [| * [| * ]]
  44 [ #I #IH #n #X2 #HX2 -IH6 -IH7 -IH8 -IH9
  45   elim (cpt_inv_atom_sn … HX2) -HX2 *
  46   [ #H1 #H2 destruct -IH2 -IH3 -IH4 -IH5 //
  47   | #s #H1 #H2 #H3 destruct -IH1 -IH3 -IH4 -IH5 //
  48   | #K #V1 #V2 #HV12 #HVX2 #H1 #H2 destruct -IH1 -IH2 -IH4 -IH5 /3 width=4 by/
  49   | #m #K #W1 #W2 #HW12 #HWX2 #H1 #H2 #H3 destruct -IH1 -IH2 -IH3 -IH5 /3 width=4 by/
  50   | #J #K #T2 #i #HT2 #HTX2 #H1 #H2 destruct -IH1 -IH2 -IH3 -IH4 /3 width=4 by/
  51   ]
  52 | #p #I #V1 #T1 #IH #n #X2 #HX2 -IH1 -IH2 -IH3 -IH4 -IH5 -IH7 -IH8 -IH9
  53   elim (cpt_inv_bind_sn … HX2) -HX2 #V2 #T2 #HV12 #HT12 #H destruct
  54   /4 width=1 by fqu_bind_dx/
  55 | #V1 #T1 #IH #n #X2 #HX2 -IH1 -IH2 -IH3 -IH4 -IH5 -IH6 -IH8 -IH9
  56   elim (cpt_inv_appl_sn … HX2) -HX2 #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by/
  57 | #U1 #T1 #IH #n #X2 #HX2 -IH1 -IH2 -IH3 -IH4 -IH5 -IH6 -IH7
  58   elim (cpt_inv_cast_sn … HX2) -HX2 *
  59   [ #U2 #T2 #HU12 #HT12 #H destruct -IH9 /3 width=1 by/
  60   | #m #Hm #H destruct -IH8 /3 width=1 by/
  61   ]
  62 ]
  63 qed-.