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