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.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "lambda/types.ma".
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)
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)
23 TJ G F (Prod A B) → TJ G a A → TJ G (App F a) (subst B 0 a)
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
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. *)
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.
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.
39 axiom conv_lift: ∀M,N. conv M N → conv (lift M 0 1) (lift N 0 1).
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.
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.
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.
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)]
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
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.
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)]
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