matita/matita/lib/pts_dummy_new/subject.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/reduction.ma".
  13 include "pts_dummy_new/inversion.ma".
  14
  15 (*
  16 inductive T : Type[0] ≝
  17   | Sort: nat → T
  18   | Rel: nat → T
  19   | App: T → T → T
  20   | Lambda: T → T → T (* type, body *)
  21   | Prod: T → T → T (* type, body *)
  22   | D: T →T
  23 .
  24
  25 inductive red : T →T → Prop ≝
  26   | rbeta: ∀P,M,N. red (App (Lambda P M) N) (M[0 ≝ N])
  27   | rappl: ∀M,M1,N. red M M1 → red (App M N) (App M1 N)
  28   | rappr: ∀M,N,N1. red N N1 → red (App M N) (App M N1)
  29   | rlaml: ∀M,M1,N. red M M1 → red (Lambda M N) (Lambda M1 N)
  30   | rlamr: ∀M,N,N1. red N N1 → red(Lambda M N) (Lambda M N1)
  31   | rprodl: ∀M,M1,N. red M M1 → red (Prod M N) (Prod M1 N)
  32   | rprodr: ∀M,N,N1. red N N1 → red (Prod M N) (Prod M N1)
  33   | d: ∀M,M1. red M M1 → red (D M) (D M1). *)
  34
  35 lemma lift_D: ∀P,M,N. lift P 0 1 = D M N →
  36   ∃M1,N1. M = lift M1 0 1 ∧ N = lift N1 0 1 ∧ P = D M1 N1.
  37 #P (cases P) normalize
  38   [#i #M #N #H destruct
  39   |#i #M #N #H destruct
  40   |#A #B #M #N #H destruct
  41   |#A #B #M #N #H destruct
  42   |#A #B #M #N #H destruct
  43   |#A #B #M #N #H destruct @(ex_intro … A) @(ex_intro … B) /3/
  44   ]
  45 qed.
  46
  47 theorem type_of_type: ∀P,G,A,B. G ⊢_{P} A : B → (∀i. B ≠ Sort i) →
  48   ∃i. G ⊢_{P} B : Sort i.
  49 #Pts #G #A #B #t (elim t)
  50   [#i #j #Aij #j @False_ind /2/
  51   |#G1 #A #i #t1 #_ #P @(ex_intro … i) @(weak … t1 t1)
  52   |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #H3 (cases (H1 ?) )
  53     [#i #Bi @(ex_intro … i) @(weak … Bi t2)
  54     |#i @(not_to_not … (H3 i)) /2 width=2/
  55     ]
  56   |#G1 #A #B #i #j #k #h #t1 #t2 #_ #_ #H3 @False_ind /2/
  57   |#G1 #A #B #C #D #t1 #t2 #H1 #H2 #H3 cases (H1 ?);
  58     [#i #t3 cases (prod_inv … t3 … (refl …))
  59      #s1 * #s2 * #s3 * * #Ci #H4 #H5 @(ex_intro … s2)
  60      @(tj_subst_0 … t2 … H5)
  61     |#i % #H destruct
  62     ]
  63   |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #H3 /2/
  64   |#G1 #A #B #C #i #ch #t1 #t2 #H1 #H2 #H3 /2/
  65   |#G1 #A #B #i #t1 #t2 #Hind1 #Hind2 #H /2/
  66   ]
  67 qed.
  68
  69 lemma prod_sort : ∀Pts,G,M,P,Q. G ⊢_{Pts} M :Prod P Q →
  70  ∃i. P::G ⊢_{Pts} Q : Sort i.
  71 #Pts #G #M #P #Q #t cases(type_of_type …t ?);
  72   [#s #t2 cases(prod_inv … t2 …(refl …)) #s1 * #s2 * #s3 * *
  73    #_ #_ #H @(ex_intro … s2) //
  74   | #i % #H destruct
  75   ]
  76 qed.
  77
  78 axiom red_lift: ∀M,N. red (lift M 0 1) N →
  79   ∃P. N = lift P 0 1 ∧ red M P.
  80
  81 theorem tj_d : ∀P,G,M,N,N1. G ⊢_{P} D M N1: N → G ⊢_{P} M : N.
  82 #Pts #G (cut (∀M,N. G ⊢_{Pts} M : N → ∀P,Q. M = D P Q → G ⊢_{Pts} P : N)) [2: /2/]
  83 #M #N #t (elim t)
  84   [#i #j #Aij #P #Q #H destruct
  85   |#G1 #A #i #t1 #_ #P #Q #H destruct
  86   |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #P #Q #H3
  87    cases (lift_D … H3) #P1 * #Q1 * * #eqP #eqQ #eqA
  88    >eqP @(weak … i) /2/
  89   |#G1 #A #B #i #j #k #h #t1 #t2 #_ #_ #P #Q #H destruct
  90   |#G1 #A #B #C #D #t1 #t2 #_ #_ #P #Q #H destruct
  91   |#G1 #A #B #C #D #t1 #t2 #_ #_ #P #Q #H destruct
  92   |#G1 #A #B #C #i #ch #t1 #t2 #H #_ #P #Q #H
  93    @(conv… ch …t2) /2/
  94   |#G1 #A #B #i #t1 #t2 #Hind1 #Hind2 #P #Q #H destruct //
  95   ]
  96 qed.
  97
  98 definition red0 ≝ λM,N. M = N ∨ red M N.
  99
 100 axiom red_to_conv : ∀P,M,N. red M N → Co P M N.
 101 axiom red0_to_conv : ∀P,M,N. red0 M N → Co P M N.
 102 axiom conv_prod: ∀P,A,B,M,N. Co P A B → Co P M N →
 103   Co P (Prod A M) (Prod B N).
 104 axiom conv_subst_1: ∀Pts,M,P,Q. red P Q → Co Pts (M[0≝Q]) (M[0≝P]).
 105
 106 inductive redG : list T → list T → Prop ≝
 107  | rnil : redG (nil T) (nil T)
 108  | rstep : ∀A,B,G1,G2. red0 A B → redG G1 G2 →
 109      redG (A::G1) (B::G2).
 110
 111 lemma redG_inv: ∀A,G,G1. redG (A::G) G1 →
 112   ∃B. ∃G2. red0 A B ∧ redG G G2 ∧ G1 = B::G2.
 113 #A #G #G1 #rg (inversion rg)
 114   [#H destruct
 115   |#A1 #B1 #G2 #G3 #r1 #r2 #_ #H destruct
 116    #H1 @(ex_intro … B1) @(ex_intro … G3) % // % //
 117   ]
 118 qed.
 119
 120 lemma redG_nil: ∀G. redG (nil T) G → G = nil T.
 121 #G #rg (inversion rg) //
 122 #A #B #G1 #G2 #r1 #r2 #_ #H destruct
 123 qed.
 124
 125 axiom conv_prod_split: ∀P,A,A1,B,B1.
 126  Co P(Prod A B) (Prod A1 B1) → Co P A A1 ∧ Co P B B1.
 127
 128 axiom red0_prod : ∀M,N,P. red0 (Prod M N) P →
 129   (∃Q. P = Prod Q N ∧ red0 M Q) ∨
 130   (∃Q. P = Prod M Q ∧ red0 N Q).
 131
 132 theorem subject_reduction: ∀P,G,M,N. G ⊢_{P} M:N →
 133  ∀M1. red0 M M1 → ∀G1. redG G G1 → G1 ⊢_{P} M1:N.
 134 #Pts #G #M #N #d (elim d)
 135   [#i #j #Aij #M1 *
 136     [#eqM1 <eqM1 #G1 #H >(redG_nil …H) /2/
 137     |#H @False_ind /2/
 138     ]
 139   |#G1 #A #i #t1 #Hind #M1 *
 140     [#eqM1 <eqM1 #G2 #H cases (redG_inv … H)
 141      #P * #G3 * * #r1 #r2 #eqG2 >eqG2
 142      @(conv ??? (lift P O 1) ? i);
 143       [@conv_lift @sym_conv @red0_to_conv //
 144       |@(start … i) @Hind //
 145       |@(weak … (Sort i) ? i); [@Hind /2/ | @Hind //]
 146       ]
 147     |#H @False_ind /2/
 148     ]
 149   |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #M1
 150    #H cases H;
 151     [#eqM1 <eqM1 #G2 #rg (cases (redG_inv … rg))
 152      #Q * #G3 * * #r2 #rg1 #eqG2 >eqG2 @(weak … i);
 153       [@H1 /2/ | @H2 //]
 154     |#H (elim (red_lift … H)) #P * #eqM1 >eqM1 #redAP
 155       #G2 #rg (cases (redG_inv … rg)) #Q * #G3 * * #r2
 156       #rg1 #eqG2 >eqG2 @(weak … i);
 157       [@H1 /2/ | @H2 //]
 158     ]
 159   |#G #A #B #i #j #k #Rjk #t1 #t2 #Hind1 #Hind2 #M1 #redP
 160    (cases (red0_prod … redP))
 161     [* #M2 * #eqM1 #redA >eqM1 #G1 #rg @(prod … Rjk);
 162       [@Hind1 // | @Hind2 /2/]
 163     |* #M2 * #eqM1 #redA >eqM1 #G1 #rg @(prod … Rjk);
 164       [@Hind1 /2/ | @Hind2 /3/]
 165     ]
 166   |#G #A #B #C #P #t1 #t2 #Hind1 #Hind2 #M1 #red0a
 167    (cases red0a)
 168     [#eqM1 <eqM1 #G1 #rg @(app … B);
 169       [@Hind1 /2/ | @Hind2 /2/ ]
 170     |#reda (cases (red_app …reda))
 171       [*
 172         [*
 173           #M2 * #N1 * #eqA #eqM1 >eqM1 #G1 #rg
 174            cut (G1 ⊢_{Pts} A: Prod B C); [@Hind1 /2/] #H1
 175            (cases (abs_inv … H1 … eqA)) #i * #N2 * *
 176            #cProd #t3 #t4
 177            (cut (Co Pts B M2 ∧ Co Pts C N2) ) [/2/] * #convB #convC
 178            (cases (prod_inv … t3 … (refl …) )) #i * #j * #k * *
 179            #cik #t5 #t6 (cut (G1 ⊢_{Pts} P:B))
 180             [@Hind2 /2/
 181             |#Hcut cut (G1 ⊢_{Pts} N1[0:=P] : N2 [0:=P]);
 182               [@(tj_subst_0 … M2) // @(conv … convB Hcut t5)
 183               |#Hcut1 cases (prod_sort … H1) #s #Csort
 184                @(conv … s  … Hcut1);
 185                 [@conv_subst /2/ | @(tj_subst_0 … Csort) //]
 186               ]
 187             ]
 188         |* #M2 * #eqM1 >eqM1 #H #G1 #rg @(app … B);
 189           [@Hind1 /2/ | @Hind2 /2/]
 190         ]
 191       |* #M2 * #eqM1 >eqM1 #H #G1 #rg
 192        cut (G1 ⊢_{Pts} A:Prod B C); [@Hind1 /2/] #t3
 193        cases (prod_sort …t3) #i #Csort @(conv ??? C[O≝ M2] … i);
 194         [@conv_subst_1 //
 195         |@(app … B)  // @Hind2 /2/
 196         |@(tj_subst_0 … Csort) @Hind2 /2/
 197         ]
 198       ]
 199     ]
 200   |#G #A #B #C #i #t1 #t2 #Hind1 #Hind2 #M2 #red0l #G1 #rg
 201    cut (A::G1⊢_{Pts} C:B); [@Hind1 /3/] #t3
 202    cut (G1 ⊢_{Pts} Prod A B : Sort i); [@Hind2 /2/] #t4
 203    cases red0l;
 204     [#eqM2 <eqM2 @(abs … t3 t4)
 205     |#redl (cases (red_lambda … redl))
 206       [* #M3 * #eqM2 #redA >eqM2
 207          @(conv ??? (Prod M3 B) … t4);
 208           [@conv_prod /2/
 209           |@(abs … i); [@Hind1 /3/ |@Hind2 /3/]
 210           ]
 211         |* #M3 * #eqM3 #redC >eqM3
 212          @(abs … t4) @Hind1 /3/
 213       ]
 214     ]
 215   |#G #A #B #C #i #convBC #t1 #t2 #Hind1 #Hind2 #M1 #redA
 216    #G1 #rg @(conv … i … convBC); [@Hind1 // |@Hind2 /2/]
 217   |#G #A #B #i #t1 #t2 #Hind1 #Hind2 #M1 #red0d #G1 #rg
 218    cases red0d;
 219     [#eqM1 <eqM1 @(dummy … i); [@Hind1 /2/ |@Hind2 /2/]
 220     |#redd (cases (red_d … redd))
 221       [* #A1 * #eqM1 #redA >eqM1
 222        @(dummy … i);[@Hind1 /2/ |@Hind2 /2/]
 223       |* #B1 * #eqM1 #redB >eqM1
 224        cut (G1 ⊢_{Pts} B: Sort i); [@Hind2 /2/] #sB
 225        cut (G1 ⊢_{Pts} B1: Sort i); [@Hind2 /2/] #sB1
 226        @(conv … B1 … i) /2/ @(dummy … i) // @(conv … B … i) /2/
 227        @Hind1 /2/
 228       ]
 229     ]
 230   ]
 231 qed.
 232