]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/pts_dummy/inversion.ma
Many changes
[helm.git] / matita / matita / lib / pts_dummy / 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 "pts_dummy/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 axiom lambda_lift : ∀A,B,C. lift A 0 1 = Lambda B C →
38 ∃P,Q. A = Lambda P Q ∧ lift P 0 1  = B ∧ lift Q 1 1 = C.
39
40 axiom prod_lift : ∀A,B,C. lift A 0 1 = Prod B C →
41 ∃P,Q. A = Prod P Q ∧ lift P 0 1  = B ∧ lift Q 1 1 = C.
42
43 axiom conv_lift: ∀P,M,N. Co P M N → Co P (lift M 0 1) (lift N 0 1).
44  
45 axiom weak_in: ∀P,G,A,B,M,N, i.
46  A::G  ⊢_{P} M : N → G ⊢_{P} B : Sort i → 
47    (lift A 0 1)::B::G ⊢_{P}  lift M 1 1 : lift N 1 1.
48
49 axiom refl_conv: ∀P,A. Co P A A.
50 axiom  sym_conv: ∀P,A,B. Co P A B → Co P B A.
51 axiom trans_conv: ∀P,A,B,C. Co P A B → Co P B C → Co P A C.
52
53 theorem prod_inv: ∀P,G,M,N. G ⊢_{P} M : N → ∀A,B.M = Prod A B → 
54   ∃i,j,k. Co P N (Sort k) ∧ G ⊢_{P} A : Sort i ∧ A::G ⊢_{P} B : Sort j. 
55 #Pts #G #M #N #t (elim t);
56   [#i #j #Aij #A #b #H destruct
57   |#G1 #P #i #t #_ #A #b #H destruct
58   |#G1 #P #Q #R #i #t1 #t2 #H1 #_ #A #B #Hl
59    cases (prod_lift … Hl) #A1 * #B1 * * #eqP #eqA #eqB
60    cases (H1 … eqP) #i * #j * #k * * #c1 #t3 #t4
61    @(ex_intro … i) @(ex_intro … j) @(ex_intro … k) <eqA <eqB %
62     [% [@(conv_lift … c1) |@(weak … t3 t2)]
63     |@(weak_in … t4 t2) 
64     ]
65   |#G1 #A #B #i #j #k #Rijk #t1 #t2 #_ #_ #A1 #B1 #H destruct
66    @(ex_intro … i) @(ex_intro … j) @(ex_intro … k) % // % //
67   |#G1 #P #A #B #C #t1 #t2 #_ #_ #A1 #B1 #H destruct
68   |#G1 #P #A #B #i #t1 #t2 #_ #_ #A1 #B1 #H destruct
69   |#G1 #A #B #C #i #cBC #t1 #t2 #H1 #H2 #A1 #B1 #eqA
70    cases (H1 … eqA) #i * #j * #k * * #c1 #t3 #t4
71    @(ex_intro … i) @(ex_intro … j) @(ex_intro … k) % //
72    % // @(trans_conv Pts C B … c1) @sym_conv //
73   |#G1 #A #B #i #t1 #t2 #_ #_ #A1 #B1 #eqA destruct
74   ]
75 qed.
76
77 theorem abs_inv: ∀P,G,M,N. G ⊢ _{P} M : N → ∀A,b.M = Lambda A b → 
78   ∃i,B. Co P N (Prod A B) ∧ G ⊢_{P} Prod A B: Sort i ∧ A::G ⊢_{P} b : B. 
79 #Pts #G #M #N #t (elim t);
80   [#i #j #Aij #A #b #H destruct
81   |#G1 #P #i #t #_ #A #b #H destruct
82   |#G1 #P #Q #R #i #t1 #t2 #H1 #_ #A #b #Hl
83    cases (lambda_lift … Hl) #A1 * #b1 * * #eqP #eqA #eqb
84    cases (H1 … eqP) #i * #B1 * * #c1 #t3 #t4
85    @(ex_intro … i) @(ex_intro … (lift B1 1 1)) <eqA <eqb %
86     [% [@(conv_lift … c1) |@(weak … t3 t2)]
87     |@(weak_in … t4 t2) 
88     ]
89   |#G1 #A #B #i #j #k #Rijk #t1 #t2 #_ #_ #A1 #b #H destruct
90   |#G1 #P #A #B #C #t1 #t2 #_ #_ #A1 #b #H destruct
91   |#G1 #P #A #B #i #t1 #t2 #_ #_ #A1 #b #H destruct
92     @(ex_intro … i) @(ex_intro … A) % // % //
93   |#G1 #A #B #C #i #cBC #t1 #t2 #H1 #H2 #A1 #b #eqA
94    cases (H1 … eqA) #i * #B1 * * #c1 #t3 #t4
95    @(ex_intro … i) @(ex_intro … B1) % //
96    % // @(trans_conv Pts C B … c1) @sym_conv //
97   |#G1 #A #B #i #t1 #t2 #_ #_ #A1 #b #eqA destruct
98   ]
99 qed.
100    
101 *)