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 *)