\ /
V_______________________________________________________________ *)
-include "lambda/types.ma".
+include "lambdaN/thinning.ma".
(*
inductive TJ (p: pts): list T → T → T → Prop ≝
TJ p G A B → TJ p G B (Sort i) → TJ p G (D A) B.
*)
-axiom lambda_lift : ∀A,B,C. lift A 0 1 = Lambda B C →
-∃P,Q. A = Lambda P Q ∧ lift P 0 1 = B ∧ lift Q 1 1 = C.
-
-axiom prod_lift : ∀A,B,C. lift A 0 1 = Prod B C →
-∃P,Q. A = Prod P Q ∧ lift P 0 1 = B ∧ lift Q 1 1 = C.
-
-axiom conv_lift: ∀P,M,N. Co P M N → Co P (lift M 0 1) (lift N 0 1).
-
-axiom weak_in: ∀P,G,A,B,M,N, i.
- A::G ⊢_{P} M : N → G ⊢_{P} B : Sort i →
- (lift A 0 1)::B::G ⊢_{P} lift M 1 1 : lift N 1 1.
-
axiom refl_conv: ∀P,A. Co P A A.
axiom sym_conv: ∀P,A,B. Co P A B → Co P B A.
axiom trans_conv: ∀P,A,B,C. Co P A B → Co P B C → Co P A C.
|#G1 #A #B #i #t1 #t2 #_ #_ #A1 #b #eqA destruct
]
qed.
+
+theorem dummy_inv: ∀P,G,M,N. G ⊢ _{P} M: N → ∀A,B.M = D A B →
+ Co P N B ∧ G ⊢_{P} A : B.
+#Pts #G #M #N #t (elim t);
+ [#i #j #Aij #A #b #H destruct
+ |#G1 #P #i #t #_ #A #b #H destruct
+ |#G1 #P #Q #R #i #t1 #t2 #H1 #_ #A #b #Hl
+ cases (dummy_lift … Hl) #A1 * #b1 * * #eqP #eqA #eqb
+ cases (H1 … eqP) #c1 #t3 <eqb %
+ [@(conv_lift … c1) |<eqA @(weak … t3 t2) ]
+ |#G1 #A #B #i #j #k #Rijk #t1 #t2 #_ #_ #A1 #b #H destruct
+ |#G1 #P #A #B #C #t1 #t2 #_ #_ #A1 #b #H destruct
+ |#G1 #P #A #B #i #t1 #t2 #_ #_ #A1 #b #H destruct
+ |#G1 #A #B #C #i #cBC #t1 #t2 #H1 #H2 #A1 #b #eqA
+ cases (H1 … eqA) #c1 #t3 % // @(trans_conv Pts … c1) @sym_conv //
+ |#G1 #A #B #i #t1 #t2 #_ #_ #A1 #b #eqA destruct /2/
+ ]
+qed.
\ /
V_______________________________________________________________ *)
-include "lambda/reduction.ma".
-include "lambda/inversion.ma".
+include "lambdaN/reduction.ma".
+include "lambdaN/inversion.ma".
(*
inductive T : Type[0] ≝
| rprodr: ∀M,N,N1. red N N1 → red (Prod M N) (Prod M N1)
| d: ∀M,M1. red M M1 → red (D M) (D M1). *)
-lemma lift_D: ∀M,N. lift M 0 1 = D N →
- ∃P. N = lift P 0 1 ∧ M = D P.
-#M (cases M) normalize
- [#i #N #H destruct
- |#i #N #H destruct
- |#A #B #N #H destruct
- |#A #B #N #H destruct
- |#A #B #N #H destruct
- |#A #N #H destruct @(ex_intro … A) /2/
+lemma lift_D: ∀P,M,N. lift P 0 1 = D M N →
+ ∃M1,N1. M = lift M1 0 1 ∧ N = lift N1 0 1 ∧ P = D M1 N1.
+#P (cases P) normalize
+ [#i #M #N #H destruct
+ |#i #M #N #H destruct
+ |#A #B #M #N #H destruct
+ |#A #B #M #N #H destruct
+ |#A #B #M #N #H destruct
+ |#A #B #M #N #H destruct @(ex_intro … A) @(ex_intro … B) /3/
]
qed.
axiom red_lift: ∀M,N. red (lift M 0 1) N →
∃P. N = lift P 0 1 ∧ red M P.
-theorem tj_d : ∀P,G,M,N. G ⊢_{P} D M : N → G ⊢_{P} M : N.
-#Pts #G (cut (∀M,N. G ⊢_{Pts} M : N → ∀P. M = D P → G ⊢_{Pts} P : N)) [2: /2/]
+theorem tj_d : ∀P,G,M,N,N1. G ⊢_{P} D M N1: N → G ⊢_{P} M : N.
+#Pts #G (cut (∀M,N. G ⊢_{Pts} M : N → ∀P,Q. M = D P Q → G ⊢_{Pts} P : N)) [2: /2/]
#M #N #t (elim t)
- [#i #j #Aij #P #H destruct
- |#G1 #A #i #t1 #_ #P #H destruct
- |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #P #H3
- cases (lift_D … H3) #P * #eqP #eqA >eqP @(weak … i) /2/
- |#G1 #A #B #i #j #k #h #t1 #t2 #_ #_ #P #H destruct
- |#G1 #A #B #C #D #t1 #t2 #_ #_ #P #H destruct
- |#G1 #A #B #C #D #t1 #t2 #_ #_ #P #H destruct
- |#G1 #A #B #C #i #ch #t1 #t2 #H #_ #P #H
+ [#i #j #Aij #P #Q #H destruct
+ |#G1 #A #i #t1 #_ #P #Q #H destruct
+ |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #P #Q #H3
+ cases (lift_D … H3) #P1 * #Q1 * * #eqP #eqQ #eqA
+ >eqP @(weak … i) /2/
+ |#G1 #A #B #i #j #k #h #t1 #t2 #_ #_ #P #Q #H destruct
+ |#G1 #A #B #C #D #t1 #t2 #_ #_ #P #Q #H destruct
+ |#G1 #A #B #C #D #t1 #t2 #_ #_ #P #Q #H destruct
+ |#G1 #A #B #C #i #ch #t1 #t2 #H #_ #P #Q #H
@(conv… ch …t2) /2/
- |#G1 #A #B #i #t1 #t2 #Hind1 #Hind2 #P #H destruct //
+ |#G1 #A #B #i #t1 #t2 #Hind1 #Hind2 #P #Q #H destruct //
]
qed.
definition red0 ≝ λM,N. M = N ∨ red M N.
-axiom conv_lift: ∀P,i,M,N. Co P M N →
- Co P (lift M 0 i) (lift N 0 i).
axiom red_to_conv : ∀P,M,N. red M N → Co P M N.
axiom red0_to_conv : ∀P,M,N. red0 M N → Co P M N.
axiom conv_prod: ∀P,A,B,M,N. Co P A B → Co P M N →
|#G #A #B #i #t1 #t2 #Hind1 #Hind2 #M1 #red0d #G1 #rg
cases red0d;
[#eqM1 <eqM1 @(dummy … i); [@Hind1 /2/ |@Hind2 /2/]
- |#redd (cases (red_d … redd)) #Q * #eqM1 #redA >eqM1
- @(dummy … i);[@Hind1 /2/ |@Hind2 /2/]
+ |#redd (cases (red_d … redd))
+ [* #A1 * #eqM1 #redA >eqM1
+ @(dummy … i);[@Hind1 /2/ |@Hind2 /2/]
+ |* #B1 * #eqM1 #redB >eqM1
+ cut (G1 ⊢_{Pts} B: Sort i); [@Hind2 /2/] #sB
+ cut (G1 ⊢_{Pts} B1: Sort i); [@Hind2 /2/] #sB1
+ @(conv … B1 … i) /2/ @(dummy … i) // @(conv … B … i) /2/
+ @Hind1 /2/
+ ]
+ ]
]
qed.
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+include "lambdaN/types.ma".
+
+(*
+inductive TJ (p: pts): list T → T → T → Prop ≝
+ | ax : ∀i,j. Ax p i j → TJ p (nil T) (Sort i) (Sort j)
+ | start: ∀G.∀A.∀i.TJ p G A (Sort i) →
+ TJ p (A::G) (Rel 0) (lift A 0 1)
+ | weak: ∀G.∀A,B,C.∀i.
+ TJ p G A B → TJ p G C (Sort i) →
+ TJ p (C::G) (lift A 0 1) (lift B 0 1)
+ | prod: ∀G.∀A,B.∀i,j,k. Re p i j k →
+ TJ p G A (Sort i) → TJ p (A::G) B (Sort j) →
+ TJ p G (Prod A B) (Sort k)
+ | app: ∀G.∀F,A,B,a.
+ TJ p G F (Prod A B) → TJ p G a A →
+ TJ p G (App F a) (subst B 0 a)
+ | abs: ∀G.∀A,B,b.∀i.
+ TJ p (A::G) b B → TJ p G (Prod A B) (Sort i) →
+ TJ p G (Lambda A b) (Prod A B)
+ | conv: ∀G.∀A,B,C.∀i. Co p B C →
+ TJ p G A B → TJ p G C (Sort i) → TJ p G A C
+ | dummy: ∀G.∀A,B.∀i.
+ TJ p G A B → TJ p G B (Sort i) → TJ p G (D A) B.
+*)
+
+(* the definition of liftl is tricky *)
+let rec liftl (G:list T) p : list T ≝
+ match G with
+ [ nil ⇒ nil T
+ | cons A D ⇒ ((lift A (length ? D) p)::(liftl D p))
+ ].
+
+axiom lambda_lift : ∀A,B,C. lift A 0 1 = Lambda B C →
+∃P,Q. A = Lambda P Q ∧ lift P 0 1 = B ∧ lift Q 1 1 = C.
+
+axiom prod_lift : ∀A,B,C. lift A 0 1 = Prod B C →
+∃P,Q. A = Prod P Q ∧ lift P 0 1 = B ∧ lift Q 1 1 = C.
+
+axiom dummy_lift : ∀A,B,C. lift A 0 1 = D B C →
+∃P,Q. A = D P Q ∧ lift P 0 1 = B ∧ lift Q 0 1 = C.
+
+axiom conv_lift: ∀P,M,N,k. Co P M N → Co P (lift M k 1) (lift N k 1).
+
+lemma weak_gen: ∀P,E,M,N. E ⊢_{P} M : N →
+∀G,D,A,i. E=D@G → G ⊢_{P} A : Sort i →
+ (liftl D 1)@(A::G) ⊢_{P} lift M (length ? D) 1 : lift N (length ? D) 1.
+#Pts #E #M #N #tjMN (elim tjMN)
+ [normalize #i #j #k #G #D #A #i (cases D)
+ [normalize #isnil destruct #H @start_lemma1 //
+ @(glegalk … (start … H))
+ |#P #L normalize #isnil destruct
+ ]
+ |#G #A #i #tjA #Hind #G1 #D #A1 #j (cases D)
+ [normalize #Heq #tjA1 <(lift_rel 0 1) @(weak …tjA1)
+ <Heq @(start … tjA)
+ |#A2 #L normalize #Heq destruct #tjA2
+ cut (S (length ? L) = 1 + length ? L + 0) // #H >H
+ >lift_lift_up <plus_n_O @(start … i) @Hind //
+ ]
+ |#G #P #Q #R #i #tjP #tjR #Hind1 #Hind2 #G1 #D #A #j (cases D) normalize
+ [#Heq #tjA @(weak … tjA) <Heq @weak //
+ |#A1 #L #Heq destruct #tjA
+ cut (S (length ? L) = 1 + length ? L + 0) // #H >H
+ >lift_lift_up >lift_lift_up @(weak … i);
+ [<plus_n_O @Hind1 // |@Hind2 // ]
+ ]
+ |#G #P #Q #i #j #k #Ax #tjP #tjQ #Hind1 #Hind2
+ #G1 #D #A #l #Heq #tjA normalize @(prod … Ax);
+ [/2/
+ |(cut (S (length T D) = (length T D)+1)) [//]
+ #Heq1 <Heq1 @(Hind2 ? (P::D)) normalize //
+ ]
+ |#G #P #Q #R #S #tjP #tjS #Hind1 #Hind2
+ #G1 #D #A #l #Heq #tjA (normalize in Hind1 ⊢ %)
+ >(lift_subst_up R S 1 0 (length ? D)) @(app … (lift Q (length ? D) 1));
+ [@Hind1 // |@Hind2 //]
+ |#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2
+ #G1 #D #A #l #Heq #tjA normalize @(abs … i);
+ [cut (∀n. S n = n +1); [//] #H <H
+ @(Hind1 G1 (P::D) … tjA) normalize //
+ |(normalize in Hind2) @(Hind2 …tjA) //
+ ]
+ |#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2
+ #G1 #D #A #l #Heq #tjA
+ @(conv … (conv_lift … convQR) ? (Hind2 …)) // @Hind1 //
+ |#G #P #Q #i #tjP #tjQ #Hind1 #Hind2
+ #G1 #D #A #l #Heq #tjA @dummy /2/
+ ]
+qed.
+
+lemma weak_in: ∀P,G,A,B,M,N, i.
+ A::G ⊢_{P} M : N → G ⊢_{P} B : Sort i →
+ (lift A 0 1)::B::G ⊢_{P} lift M 1 1 : lift N 1 1.
+#P #G #A #B #M #N #i #tjM #tjB
+cut (∀A.(lift A 0 1)::B::G = (liftl (A::(nil ?)) 1)@(B::G)) // #H >H
+@(weak_gen … tjM … tjB) //
+qed.
\ /
V_______________________________________________________________ *)
-include "lambda/subst.ma".
+include "lambdaN/subst.ma".
include "basics/list.ma".
| conv: ∀G.∀A,B,C.∀i. Co p B C →
TJ p G A B → TJ p G C (Sort i) → TJ p G A C
| dummy: ∀G.∀A,B.∀i.
- TJ p G A B → TJ p G B (Sort i) → TJ p G (D A) B.
+ TJ p G A B → TJ p G B (Sort i) → TJ p G (D A B) B.
interpretation "generic type judgement" 'TJT P G A B = (TJ P G A B).
|#G #A #B #C #i #tjAB #tjC #Hind1 #_ #m (cases m)
/2/ #p #Hle @start_rel // @Hind1 @le_S_S_to_le @Hle
]
-qed.
+qed.
axiom conv_subst: ∀T,P,Q,N,i.Co T P Q → Co T P[i := N] Q[i := N].
projects / helm.git / commitdiff