matita/matita/contribs/lambdadelta/static_2/static/aaa_dec.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/static/aaa_drops.ma".
  16 include "static_2/static/aaa_aaa.ma".
  17
  18 (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
  19
  20 (* Main properties **********************************************************)
  21
  22 theorem aaa_dec (G) (L) (T): Decidable (∃A. ⦃G,L⦄ ⊢ T ⁝ A).
  23 #G #L #T @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T
  24 #G0 #L0 #T0 #IH #G #L * * [||| #p * | * ]
  25 [ #s #HG #HL #HT destruct -IH
  26   /3 width=2 by aaa_sort, ex_intro, or_introl/
  27 | #i #HG #HL #HT destruct
  28   elim (drops_F_uni L i) [| * * #I [| #V ] #K ] #HLK
  29   [1,2: -IH
  30     @or_intror * #A #H
  31     elim (aaa_inv_lref_drops … H) -H #J #Y #X #HLY #_ -G -A
  32     lapply (drops_mono … HLY … HLK) -L -i #H destruct
  33   | elim (IH G K V) -IH [3: /2 width=2 by fqup_lref/ ]
  34     [ * /4 width=6 by aaa_lref_drops, ex_intro, or_introl/
  35     | #H0 @or_intror * #A #H
  36       lapply (aaa_pair_inv_lref … H … HLK) -I -L -i
  37       /3 width=2 by ex_intro/
  38     ]
  39   ]
  40 | #l #HG #HL #HT destruct -IH
  41   @or_intror * #A #H
  42   @(aaa_inv_gref … H)
  43 | #V #T #HG #HL #HT destruct
  44   elim (IH G L V) [ * #B #HB | #HnB | // ]
  45   [ elim (IH G (L.ⓓV) T) [ * #A #HA | #HnA | // ] ] -IH
  46   [ /4 width=2 by aaa_abbr, ex_intro, or_introl/ ]
  47   @or_intror * #A #H
  48   elim (aaa_inv_abbr … H) -H #B0 #HB0 #HA0
  49   /3 width=2 by ex_intro/
  50 | #W #T #HG #HL #HT destruct
  51   elim (IH G L W) [ * #B #HB | #HnB | // ]
  52   [ elim (IH G (L.ⓛW) T) [ * #A #HA | #HnA | // ] ] -IH
  53   [ /4 width=2 by aaa_abst, ex_intro, or_introl/ ]
  54   @or_intror * #A #H
  55   elim (aaa_inv_abst … H) -H #B0 #A0 #HB0 #HA0 #H destruct
  56   /3 width=2 by ex_intro/
  57 | #V #T #HG #HL #HT destruct
  58   elim (IH G L V) [ * #B #HB | #HnB | // ]
  59   [ elim (IH G L T) [ * #X #HX | #HnX | // ] ] -IH
  60   [ elim (is_apear_dec B X) [ * #A #H destruct | #HnX ]
  61     [ /4 width=4 by aaa_appl, ex_intro, or_introl/ ]
  62   ]
  63   @or_intror * #A #H
  64   [ lapply (aaa_aaa_inv_appl … H HB HX) -G -L -V -T
  65   |*: elim (aaa_inv_appl … H) -H #B0 #HB0 #HA0
  66   ]
  67   /3 width=2 by ex_intro/
  68 | #U #T #HG #HL #HT destruct
  69   elim (IH G L U) [ * #B #HB | #HnB | // ]
  70   [ elim (IH G L T) [ * #A #HA | #HnA | // ] ] -IH
  71   [ elim (eq_aarity_dec B A) [ #H destruct | #HnA ]
  72     [ /4 width=3 by aaa_cast, ex_intro, or_introl/ ]
  73   ]
  74   @or_intror * #X #H
  75   [ elim (aaa_aaa_inv_cast … H HB HA) -G -L -U -T
  76   |*: elim (aaa_inv_cast … H) -H #HU #HT
  77   ]
  78   /3 width=2 by ex_intro/
  79 ]
  80 qed-.