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