matita/matita/lib/lambdaN/thinning.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "lambdaN/types.ma".
  13
  14 (*
  15 inductive TJ (p: pts): list T → T → T → Prop ≝
  16   | ax : ∀i,j. Ax p i j → TJ p (nil T) (Sort i) (Sort j)
  17   | start: ∀G.∀A.∀i.TJ p G A (Sort i) →
  18       TJ p (A::G) (Rel 0) (lift A 0 1)
  19   | weak: ∀G.∀A,B,C.∀i.
  20      TJ p G A B → TJ p G C (Sort i) →
  21        TJ p (C::G) (lift A 0 1) (lift B 0 1)
  22   | prod: ∀G.∀A,B.∀i,j,k. Re p i j k →
  23      TJ p G A (Sort i) → TJ p (A::G) B (Sort j) →
  24        TJ p G (Prod A B) (Sort k)
  25   | app: ∀G.∀F,A,B,a.
  26      TJ p G F (Prod A B) → TJ p G a A →
  27        TJ p G (App F a) (subst B 0 a)
  28   | abs: ∀G.∀A,B,b.∀i.
  29      TJ p (A::G) b B → TJ p G (Prod A B) (Sort i) →
  30        TJ p G (Lambda A b) (Prod A B)
  31   | conv: ∀G.∀A,B,C.∀i. Co p B C →
  32      TJ p G A B → TJ p G C (Sort i) → TJ p G A C
  33   | dummy: ∀G.∀A,B.∀i.
  34      TJ p G A B → TJ p G B (Sort i) → TJ p G (D A) B.
  35 *)
  36
  37 (* the definition of liftl is tricky *)
  38 let rec liftl (G:list T) p : list T ≝
  39   match G with
  40     [ nil ⇒ nil T
  41     | cons A D ⇒ ((lift A (length ? D) p)::(liftl D p))
  42     ].
  43
  44 axiom lambda_lift : ∀A,B,C. lift A 0 1 = Lambda B C →
  45 ∃P,Q. A = Lambda P Q ∧ lift P 0 1  = B ∧ lift Q 1 1 = C.
  46
  47 axiom prod_lift : ∀A,B,C. lift A 0 1 = Prod B C →
  48 ∃P,Q. A = Prod P Q ∧ lift P 0 1  = B ∧ lift Q 1 1 = C.
  49
  50 axiom dummy_lift : ∀A,B,C. lift A 0 1 = D B C →
  51 ∃P,Q. A = D P Q ∧ lift P 0 1  = B ∧ lift Q 0 1 = C.
  52
  53 axiom conv_lift: ∀P,M,N,k. Co P M N → Co P (lift M k 1) (lift N k 1).
  54
  55 lemma weak_gen: ∀P,E,M,N. E ⊢_{P} M : N →
  56 ∀G,D,A,i. E=D@G → G ⊢_{P} A : Sort i →
  57    (liftl D 1)@(A::G) ⊢_{P}  lift M (length ? D) 1 : lift N (length ? D) 1.
  58 #Pts #E #M #N #tjMN (elim tjMN)
  59   [normalize #i #j #k #G #D #A #i (cases D)
  60     [normalize #isnil destruct #H @start_lemma1 //
  61      @(glegalk … (start … H))
  62     |#P #L normalize #isnil destruct
  63     ]
  64   |#G #A #i #tjA #Hind #G1 #D #A1 #j (cases D)
  65     [normalize #Heq #tjA1 <(lift_rel 0 1) @(weak …tjA1)
  66      <Heq @(start … tjA)
  67     |#A2 #L normalize #Heq destruct #tjA2
  68      cut (S (length ? L) = 1 + length ? L + 0) // #H >H
  69      >lift_lift_up <plus_n_O @(start … i) @Hind //
  70     ]
  71   |#G #P #Q #R #i #tjP #tjR #Hind1 #Hind2 #G1 #D #A #j (cases D) normalize
  72     [#Heq #tjA @(weak … tjA) <Heq @weak //
  73     |#A1 #L #Heq destruct #tjA
  74      cut (S (length ? L) = 1 + length ? L + 0) // #H >H
  75      >lift_lift_up >lift_lift_up @(weak … i);
  76       [<plus_n_O @Hind1 // |@Hind2 // ]
  77     ]
  78   |#G #P #Q #i #j #k #Ax #tjP #tjQ #Hind1 #Hind2
  79    #G1 #D #A #l #Heq #tjA normalize @(prod … Ax);
  80     [/2/
  81     |(cut (S (length T D) = (length T D)+1)) [//]
  82      #Heq1 <Heq1 @(Hind2 ? (P::D)) normalize //
  83     ]
  84   |#G #P #Q #R #S #tjP #tjS #Hind1 #Hind2
  85    #G1 #D #A #l #Heq #tjA (normalize in Hind1 ⊢ %)
  86    >(lift_subst_up R S 1 0 (length ? D)) @(app … (lift Q (length ? D) 1));
  87     [@Hind1 // |@Hind2 //]
  88   |#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2
  89    #G1 #D #A #l #Heq #tjA normalize @(abs … i);
  90     [cut (∀n. S n = n +1); [//] #H <H
  91      @(Hind1 G1 (P::D) … tjA) normalize //
  92     |(normalize in Hind2) @(Hind2 …tjA) //
  93     ]
  94   |#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2
  95    #G1 #D #A #l #Heq #tjA
  96    @(conv … (conv_lift … convQR) ? (Hind2 …)) // @Hind1 //
  97   |#G #P #Q #i #tjP #tjQ #Hind1 #Hind2
  98    #G1 #D #A #l #Heq #tjA @dummy /2/
  99   ]
 100 qed.
 101
 102 lemma weak_in: ∀P,G,A,B,M,N, i.
 103  A::G  ⊢_{P} M : N → G ⊢_{P} B : Sort i →
 104    (lift A 0 1)::B::G ⊢_{P}  lift M 1 1 : lift N 1 1.
 105 #P #G #A #B #M #N #i #tjM #tjB
 106 cut (∀A.(lift A 0 1)::B::G = (liftl (A::(nil ?)) 1)@(B::G)) // #H >H
 107 @(weak_gen … tjM … tjB) //
 108 qed.