matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta_ind.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/dynamic/nta_drops.ma".
  16 include "basic_2/dynamic/nta_cpcs.ma".
  17 include "basic_2/i_dynamic/ntas_cpcs.ma".
  18 include "basic_2/i_dynamic/ntas_nta.ma".
  19 include "basic_2/i_dynamic/ntas_ntas.ma".
  20
  21 (* ITERATED NATIVE TYPE ASSIGNMENT FOR TERMS ********************************)
  22
  23 (* Advanced eliminators for native type assignment **************************)
  24
  25 lemma ntas_ind_bi_nta (h) (a) (G) (L) (Q:relation3 …):
  26       (∀T1,T2. ❪G,L❫ ⊢ T1 ![h,a] → ❪G,L❫ ⊢ T2 ![h,a] → ❪G,L❫ ⊢ T1 ⬌*[h] T2 →
  27         Q 0 T1 T2
  28       ) →
  29       (∀T1,T2. ❪G,L❫ ⊢ T1 :[h,a] T2 → Q 1 T1 T2
  30       ) →
  31       (∀n1,n2,T1,T2,T0.  ❪G,L❫ ⊢ T1 :*[h,a,n1] T0 → ❪G,L❫ ⊢ T0 :*[h,a,n2] T2 →
  32         Q n1 T1 T0 → Q n2 T0 T2 → Q (n1+n2) T1 T2
  33       ) →
  34       ∀n,T1,T2. ❪G,L❫ ⊢ T1 :*[h,a,n] T2 → Q n T1 T2.
  35 #h #a #G #L #Q #IH1 #IH2 #IH3 #n
  36 @(nat_elim1 n) -n * [| * ]
  37 [ #_ #T1 #T2 #H
  38   elim (ntas_inv_zero … H) -H #HT1 #HT2 #HT12
  39   /2 width=1 by/
  40 | #_ #T1 #T2 #H
  41   /3 width=1 by ntas_inv_nta/
  42 | #n #IH #T1 #T2 <plus_SO_sn #H
  43   elim (ntas_inv_plus … H) -H #T0 #HT10 #HT02
  44   /3 width=5 by/
  45 ]
  46 qed-.
  47
  48 lemma nta_ind_cnv (h) (a) (Q:relation4 …):
  49       (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
  50       (∀G,K,V,W,U.
  51         ❪G,K❫ ⊢ V :[h,a] W → ⇧*[1] W ≘ U →
  52         Q G K V W → Q G (K.ⓓV) (#0) U
  53       ) →
  54       (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,a] → ⇧*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
  55       (∀I,G,K,W,U,i.
  56         ❪G,K❫ ⊢ #i :[h,a] W → ⇧*[1] W ≘ U →
  57         Q G K (#i) W → Q G (K.ⓘ[I]) (#↑i) U
  58       ) →
  59       (∀p,I,G,K,V,T,U.
  60         ❪G,K❫ ⊢ V ![h,a] → ❪G,K.ⓑ[I]V❫ ⊢ T :[h,a] U →
  61         Q G (K.ⓑ[I]V) T U → Q G K (ⓑ[p,I]V.T) (ⓑ[p,I]V.U)
  62       ) →
  63       (∀p,G,L,V,W,T,U0,U. (**) (* one IH is missing *)
  64         ad a 0 → ❪G,L❫ ⊢ V :[h,a] W → ❪G,L❫ ⊢ T :*[h,a,0] ⓛ[p]W.U0 → ❪G,L.ⓛW❫ ⊢ U0 :[h,a] U →
  65         Q G L V W (* → Q G (L.ⓛW) U0 U *) → Q G L (ⓐV.T) (ⓐV.ⓛ[p]W.U)
  66       ) →
  67       (∀n,p,G,L,V,W,T,U,U0.
  68         ad a (↑n) → ❪G,L❫ ⊢ V :[h,a] W → ❪G,L❫ ⊢ T :[h,a] U → ❪G,L❫ ⊢ U :*[h,a,n] ⓛ[p]W.U0 →
  69         Q G L V W → Q G L T U → Q G L (ⓐV.T) (ⓐV.U)
  70       ) →
  71       (∀G,L,T,U. ❪G,L❫ ⊢ T :[h,a] U → Q G L T U → Q G L (ⓝU.T) U
  72       ) →
  73       (∀G,L,T,U1,U2.
  74         ❪G,L❫ ⊢ T :[h,a] U1 → ❪G,L❫ ⊢ U1 ⬌*[h] U2 → ❪G,L❫ ⊢ U2 ![h,a] →
  75         Q G L T U1 → Q G L T U2
  76       ) →
  77       ∀G,L,T,U. ❪G,L❫ ⊢ T :[h,a] U → Q G L T U.
  78 #h #a #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #H9 #G #L #T
  79 @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ]
  80 [ #s #HG #HL #HT #X #H destruct -IH
  81   elim (nta_inv_sort_sn … H) -H #HUX #HX
  82   /2 width=4 by/
  83 | * [| #i ] #HG #HL #HT #X #H destruct
  84   [ elim (nta_inv_lref_sn_drops_cnv … H) -H *
  85     [ #K #V #W #U #H #HVW #HWU #HUX #HX
  86       lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
  87       /5 width=7 by nta_ldef, fqu_fqup, fqu_lref_O/
  88     | #K #W #U #H #HW #HWU #HUX #HX
  89       lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
  90       /3 width=4 by nta_ldec_cnv/
  91     ]
  92   | elim (nta_inv_lref_sn … H) -H #I #K #T #U #HT #HTU #HUX #HX #H destruct
  93     /5 width=7 by nta_lref, fqu_fqup/
  94   ]
  95 | #l #HG #HL #HT #U #H destruct -IH
  96   elim (nta_inv_gref_sn … H)
  97 | #p #I #V #T #HG #HL #HT #X #H destruct
  98   elim (nta_inv_bind_sn_cnv … H) -H #U #HV #HTU #HUX #HX
  99   /4 width=5 by nta_bind_cnv/
 100 | #V #T #HG #HL #HT #X #H destruct
 101   elim (nta_inv_appl_sn_ntas … H) -H *
 102   [ #p #W #U #U0 #Ha #HVW #HTU0 #HU0 #HUX #HX -IH7
 103     /4 width=10 by nta_appl_ntas_zero/
 104   | #n #p #W #U #U0 #Ha #HVW #HTU #HU0 #HUX #HX -IH6
 105     /4 width=13 by nta_appl_ntas_pos/
 106   ]
 107 | #U #T #HG #HL #HT #X #H destruct
 108   elim (nta_inv_cast_sn … H) -H #HTU #HUX #HX
 109   /4 width=4 by nta_cast/
 110 ]
 111 qed-.