matita/matita/contribs/lambdadelta/basic_2/dynamic/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_cpms.ma".
  17 include "basic_2/dynamic/nta_cpcs.ma".
  18 include "basic_2/dynamic/nta_preserve.ma".
  19
  20 (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
  21
  22 (* Advanced eliminators *****************************************************)
  23
  24 lemma nta_ind_rest_cnv (h) (Q:relation4 …):
  25       (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
  26       (∀G,K,V,W,U.
  27         ❪G,K❫ ⊢ V :[h,𝟐] W → ⇧*[1] W ≘ U →
  28         Q G K V W → Q G (K.ⓓV) (#0) U
  29       ) →
  30       (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,𝟐] → ⇧*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
  31       (∀I,G,K,W,U,i.
  32         ❪G,K❫ ⊢ #i :[h,𝟐] W → ⇧*[1] W ≘ U →
  33         Q G K (#i) W → Q G (K.ⓘ[I]) (#↑i) U
  34       ) →
  35       (∀p,I,G,K,V,T,U.
  36         ❪G,K❫ ⊢ V ![h,𝟐] → ❪G,K.ⓑ[I]V❫ ⊢ T :[h,𝟐] U →
  37         Q G (K.ⓑ[I]V) T U → Q G K (ⓑ[p,I]V.T) (ⓑ[p,I]V.U)
  38       ) →
  39       (∀p,G,L,V,W,T,U.
  40         ❪G,L❫ ⊢ V :[h,𝟐] W → ❪G,L❫ ⊢ T :[h,𝟐] ⓛ[p]W.U →
  41         Q G L V W → Q G L T (ⓛ[p]W.U) → Q G L (ⓐV.T) (ⓐV.ⓛ[p]W.U)
  42       ) →
  43       (∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝟐] U → Q G L T U → Q G L (ⓝU.T) U
  44       ) →
  45       (∀G,L,T,U1,U2.
  46         ❪G,L❫ ⊢ T :[h,𝟐] U1 → ❪G,L❫ ⊢ U1 ⬌*[h] U2 → ❪G,L❫ ⊢ U2 ![h,𝟐] →
  47         Q G L T U1 → Q G L T U2
  48       ) →
  49       ∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝟐] U → Q G L T U.
  50 #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #G #L #T
  51 @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ]
  52 [ #s #HG #HL #HT #X #H destruct -IH
  53   elim (nta_inv_sort_sn … H) -H #HUX #HX
  54   /2 width=4 by/
  55 | * [| #i ] #HG #HL #HT #X #H destruct
  56   [ elim (nta_inv_lref_sn_drops_cnv … H) -H *
  57     [ #K #V #W #U #H #HVW #HWU #HUX #HX
  58       lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
  59       /5 width=7 by nta_ldef, fqu_fqup, fqu_lref_O/
  60     | #K #W #U #H #HW #HWU #HUX #HX
  61       lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
  62       /3 width=4 by nta_ldec_cnv/
  63     ]
  64   | elim (nta_inv_lref_sn … H) -H #I #K #T #U #HT #HTU #HUX #HX #H destruct
  65     /5 width=7 by nta_lref, fqu_fqup/
  66   ]
  67 | #l #HG #HL #HT #U #H destruct -IH
  68   elim (nta_inv_gref_sn … H)
  69 | #p #I #V #T #HG #HL #HT #X #H destruct
  70   elim (nta_inv_bind_sn_cnv … H) -H #U #HV #HTU #HUX #HX
  71   /4 width=5 by nta_bind_cnv/
  72 | #V #T #HG #HL #HT #X #H destruct
  73   elim (nta_inv_appl_sn … H) -H #p #W #U #HVW #HTU #HUX #HX
  74   /4 width=9 by nta_appl/
  75 | #U #T #HG #HL #HT #X #H destruct
  76   elim (nta_inv_cast_sn … H) -H #HTU #HUX #HX
  77   /4 width=4 by nta_cast/
  78 ]
  79 qed-.
  80
  81 lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …):
  82       (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
  83       (∀G,K,V,W,U.
  84         ❪G,K❫ ⊢ V :[h,𝛚] W → ⇧*[1] W ≘ U →
  85         Q G K V W → Q G (K.ⓓV) (#0) U
  86       ) →
  87       (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,𝛚] → ⇧*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
  88       (∀I,G,K,W,U,i.
  89         ❪G,K❫ ⊢ #i :[h,𝛚] W → ⇧*[1] W ≘ U →
  90         Q G K (#i) W → Q G (K.ⓘ[I]) (#↑i) U
  91       ) →
  92       (∀p,I,G,K,V,T,U.
  93         ❪G,K❫ ⊢ V ![h,𝛚] → ❪G,K.ⓑ[I]V❫ ⊢ T :[h,𝛚] U →
  94         Q G (K.ⓑ[I]V) T U → Q G K (ⓑ[p,I]V.T) (ⓑ[p,I]V.U)
  95       ) →
  96       (∀p,G,L,V,W,T,U.
  97         ❪G,L❫ ⊢ V :[h,𝛚] W → ❪G,L❫ ⊢ T :[h,𝛚] ⓛ[p]W.U →
  98         Q G L V W → Q G L T (ⓛ[p]W.U) → Q G L (ⓐV.T) (ⓐV.ⓛ[p]W.U)
  99       ) →
 100       (∀G,L,V,T,U.
 101         ❪G,L❫ ⊢ T :[h,𝛚] U → ❪G,L❫ ⊢ ⓐV.U ![h,𝛚] →
 102         Q G L T U → Q G L (ⓐV.T) (ⓐV.U)
 103       ) →
 104       (∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝛚] U → Q G L T U → Q G L (ⓝU.T) U
 105       ) →
 106       (∀G,L,T,U1,U2.
 107         ❪G,L❫ ⊢ T :[h,𝛚] U1 → ❪G,L❫ ⊢ U1 ⬌*[h] U2 → ❪G,L❫ ⊢ U2 ![h,𝛚] →
 108         Q G L T U1 → Q G L T U2
 109       ) →
 110       ∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝛚] U → Q G L T U.
 111 #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T
 112 @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ]
 113 [ #s #HG #HL #HT #X #H destruct -IH
 114   elim (nta_inv_sort_sn … H) -H #HUX #HX
 115   /2 width=4 by/
 116 | * [| #i ] #HG #HL #HT #X #H destruct
 117   [ elim (nta_inv_lref_sn_drops_cnv … H) -H *
 118     [ #K #V #W #U #H #HVW #HWU #HUX #HX
 119       lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
 120       /5 width=7 by nta_ldef, fqu_fqup, fqu_lref_O/
 121     | #K #W #U #H #HW #HWU #HUX #HX
 122       lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
 123       /3 width=4 by nta_ldec_cnv/
 124     ]
 125   | elim (nta_inv_lref_sn … H) -H #I #K #T #U #HT #HTU #HUX #HX #H destruct
 126     /5 width=7 by nta_lref, fqu_fqup/
 127   ]
 128 | #l #HG #HL #HT #U #H destruct -IH
 129   elim (nta_inv_gref_sn … H)
 130 | #p #I #V #T #HG #HL #HT #X #H destruct
 131   elim (nta_inv_bind_sn_cnv … H) -H #U #HV #HTU #HUX #HX
 132   /4 width=5 by nta_bind_cnv/
 133 | #V #T #HG #HL #HT #X #H destruct
 134   elim (nta_inv_pure_sn_cnv … H) -H *
 135   [ #p #W #U #HVW #HTU #HUX #HX
 136     /4 width=9 by nta_appl/
 137   | #U #HTU #HVU #HUX #HX
 138     /4 width=6 by nta_pure_cnv/
 139   ]
 140 | #U #T #HG #HL #HT #X #H destruct
 141   elim (nta_inv_cast_sn … H) -H #HTU #HUX #HX
 142   /4 width=4 by nta_cast/
 143 ]
 144 qed-.
 145
 146 lemma nta_ind_ext_cnv (h) (Q:relation4 …):
 147       (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
 148       (∀G,K,V,W,U.
 149         ❪G,K❫ ⊢ V :[h,𝛚] W → ⇧*[1] W ≘ U →
 150         Q G K V W → Q G (K.ⓓV) (#0) U
 151       ) →
 152       (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,𝛚] → ⇧*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
 153       (∀I,G,K,W,U,i.
 154         ❪G,K❫ ⊢ #i :[h,𝛚] W → ⇧*[1] W ≘ U →
 155         Q G K (#i) W → Q G (K.ⓘ[I]) (#↑i) U
 156       ) →
 157       (∀p,I,G,K,V,T,U.
 158         ❪G,K❫ ⊢ V ![h,𝛚] → ❪G,K.ⓑ[I]V❫ ⊢ T :[h,𝛚] U →
 159         Q G (K.ⓑ[I]V) T U → Q G K (ⓑ[p,I]V.T) (ⓑ[p,I]V.U)
 160       ) →
 161       (∀p,G,K,V,W,T,U.
 162         ❪G,K❫ ⊢ V :[h,𝛚] W → ❪G,K.ⓛW❫ ⊢ T :[h,𝛚] U →
 163         Q G K V W → Q G (K.ⓛW) T U → Q G K (ⓐV.ⓛ[p]W.T) (ⓐV.ⓛ[p]W.U)
 164       ) →
 165       (∀G,L,V,T,U.
 166         ❪G,L❫ ⊢ T :[h,𝛚] U → ❪G,L❫ ⊢ ⓐV.U ![h,𝛚] →
 167         Q G L T U → Q G L (ⓐV.T) (ⓐV.U)
 168       ) →
 169       (∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝛚] U → Q G L T U → Q G L (ⓝU.T) U
 170       ) →
 171       (∀G,L,T,U1,U2.
 172         ❪G,L❫ ⊢ T :[h,𝛚] U1 → ❪G,L❫ ⊢ U1 ⬌*[h] U2 → ❪G,L❫ ⊢ U2 ![h,𝛚] →
 173         Q G L T U1 → Q G L T U2
 174       ) →
 175       ∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝛚] U → Q G L T U.
 176 #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T #U #H
 177 @(nta_ind_ext_cnv_mixed … IH1 IH2 IH3 IH4 IH5 … IH7 IH8 IH9 … H) -G -L -T -U -IH1 -IH2 -IH3 -IH4 -IH5 -IH6 -IH8 -IH9
 178 #p #G #L #V #W #T #U #HVW #HTU #_ #IHTU
 179 lapply (nta_fwd_cnv_dx … HTU) #H
 180 elim (cnv_inv_bind … H) -H #_ #HU
 181 elim (cnv_nta_sn … HU) -HU #X #HUX
 182 /4 width=2 by nta_appl_abst, nta_fwd_cnv_sn/
 183 qed-.