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