matita/matita/lib/lambda/inversion.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 "lambda/types.ma".
  13
  14 (*
  15 inductive TJ: list T → T → T → Prop ≝
  16   | ax : ∀i,j. A i j → TJ (nil T) (Sort i) (Sort j)
  17   | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 0 1)
  18   | weak: ∀G.∀A,B,C.∀i.
  19      TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 0 1) (lift B 0 1)
  20   | prod: ∀G.∀A,B.∀i,j,k. R i j k →
  21      TJ G A (Sort i) → TJ (A::G) B (Sort j) → TJ G (Prod A B) (Sort k)
  22   | app: ∀G.∀F,A,B,a.
  23      TJ G F (Prod A B) → TJ G a A → TJ G (App F a) (subst B 0 a)
  24   | abs: ∀G.∀A,B,b.∀i.
  25      TJ (A::G) b B → TJ G (Prod A B) (Sort i) → TJ G (Lambda A b) (Prod A B)
  26   | conv: ∀G.∀A,B,C.∀i. conv B C →
  27      TJ G A B → TJ G C (Sort i) → TJ G A C
  28   | dummy: ∀G.∀A,B.∀i.
  29      TJ G A B → TJ G B (Sort i) → TJ G (D A) B.
  30      axiom prod_inv : ∀G,M,P,Q. G ⊢ M : Prod P Q →
  31  ∃i. P::G ⊢ Q : Sort i. *)
  32
  33 axiom lambda_lift : ∀A,B,C. lift A 0 1 = Lambda B C →
  34 ∃P,Q. A = Lambda P Q ∧ lift P 0 1  = B ∧ lift Q 1 1 = C.
  35
  36 axiom prod_lift : ∀A,B,C. lift A 0 1 = Prod B C →
  37 ∃P,Q. A = Prod P Q ∧ lift P 0 1  = B ∧ lift Q 1 1 = C.
  38
  39 axiom conv_lift: ∀M,N. conv M N → conv (lift M 0 1) (lift N 0 1).
  40
  41 axiom weak_in: ∀G.∀A,B,M,N.∀i.A::G  ⊢ M : N → G ⊢ B : Sort i →
  42  (lift A 0 1)::B::G ⊢  lift M 1 1 : lift N 1 1.
  43
  44 axiom refl_conv: ∀A. conv A A.
  45 axiom  sym_conv: ∀A,B. conv A B → conv B A.
  46 axiom trans_conv: ∀A,B,C. conv A B → conv B C → conv A C.
  47
  48 theorem prod_inv: ∀G,M,N. G ⊢ M : N → ∀A,B.M = Prod A B →
  49   ∃i,j,k. conv N (Sort k) ∧ G ⊢A : Sort i ∧ A::G ⊢B : Sort j.
  50 #G #M #N #t (elim t);
  51   [#i #j #Aij #A #b #H destruct
  52   |#G1 #P #i #t #_ #A #b #H destruct
  53   |#G1 #P #Q #R #i #t1 #t2 #H1 #_ #A #B #Hl
  54    cases (prod_lift … Hl) #A1 * #B1 * * #eqP #eqA #eqB
  55    cases (H1 … eqP) #i * #j * #k * * #c1 #t3 #t4
  56    @(ex_intro … i) @(ex_intro … j) @(ex_intro … k) <eqA <eqB %
  57     [% [@(conv_lift … c1) |@(weak … t3 t2)]
  58     |@(weak_in … t4 t2)
  59     ]
  60   |#G1 #A #B #i #j #k #Rijk #t1 #t2 #_ #_ #A1 #B1 #H destruct
  61    @(ex_intro … i) @(ex_intro … j) @(ex_intro … k) % // % //
  62   |#G1 #P #A #B #C #t1 #t2 #_ #_ #A1 #B1 #H destruct
  63   |#G1 #P #A #B #i #t1 #t2 #_ #_ #A1 #B1 #H destruct
  64   |#G1 #A #B #C #i #cBC #t1 #t2 #H1 #H2 #A1 #B1 #eqA
  65    cases (H1 … eqA) #i * #j * #k * * #c1 #t3 #t4
  66    @(ex_intro … i) @(ex_intro … j) @(ex_intro … k) % //
  67    % // @(trans_conv C B … c1) @sym_conv //
  68   |#G1 #A #B #i #t1 #t2 #_ #_ #A1 #B1 #eqA destruct
  69   ]
  70 qed.
  71
  72 theorem abs_inv: ∀G,M,N. G ⊢ M : N → ∀A,b.M = Lambda A b →
  73   ∃i,B. conv N (Prod A B) ∧ G ⊢Prod A B: Sort i ∧ A::G ⊢b : B.
  74 #G #M #N #t (elim t);
  75   [#i #j #Aij #A #b #H destruct
  76   |#G1 #P #i #t #_ #A #b #H destruct
  77   |#G1 #P #Q #R #i #t1 #t2 #H1 #_ #A #b #Hl
  78    cases (lambda_lift … Hl) #A1 * #b1 * * #eqP #eqA #eqb
  79    cases (H1 … eqP) #i * #B1 * * #c1 #t3 #t4
  80    @(ex_intro … i) @(ex_intro … (lift B1 1 1)) <eqA <eqb %
  81     [% [@(conv_lift … c1) |@(weak … t3 t2)]
  82     |@(weak_in … t4 t2)
  83     ]
  84   |#G1 #A #B #i #j #k #Rijk #t1 #t2 #_ #_ #A1 #b #H destruct
  85   |#G1 #P #A #B #C #t1 #t2 #_ #_ #A1 #b #H destruct
  86   |#G1 #P #A #B #i #t1 #t2 #_ #_ #A1 #b #H destruct
  87     @(ex_intro … i) @(ex_intro … A) % // % //
  88   |#G1 #A #B #C #i #cBC #t1 #t2 #H1 #H2 #A1 #b #eqA
  89    cases (H1 … eqA) #i * #B1 * * #c1 #t3 #t4
  90    @(ex_intro … i) @(ex_intro … B1) % //
  91    % // @(trans_conv C B … c1) @sym_conv //
  92   |#G1 #A #B #i #t1 #t2 #_ #_ #A1 #b #eqA destruct
  93   ]
  94 qed.
  95