matita/matita/lib/didactic/natural_deduction.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* Logic system *)
  16
  17 include "basics/pts.ma".
  18 include "hints_declaration.ma".
  19
  20 inductive Imply (A,B:Prop) : Prop ≝
  21 | Imply_intro: (A → B) → Imply A B.
  22
  23 definition Imply_elim ≝ λA,B:Prop.λf:Imply A B. λa:A.
  24   match f with [ Imply_intro g ⇒ g a].
  25
  26 inductive And (A,B:Prop) : Prop ≝
  27 | And_intro: A → B → And A B.
  28
  29 definition And_elim_l ≝ λA,B.λc:And A B.
  30   match c with [ And_intro a b ⇒ a ].
  31
  32 definition And_elim_r ≝ λA,B.λc:And A B.
  33   match c with [ And_intro a b ⇒ b ].
  34
  35 inductive Or (A,B:Prop) : Prop ≝
  36 | Or_intro_l: A → Or A B
  37 | Or_intro_r: B → Or A B.
  38
  39 definition Or_elim ≝ λA,B,C:Prop.λc:Or A B.λfa: A → C.λfb: B → C.
  40   match c with
  41   [ Or_intro_l a ⇒ fa a
  42   | Or_intro_r b ⇒ fb b].
  43
  44 inductive Top : Prop :=
  45 | Top_intro : Top.
  46
  47 inductive Bot : Prop := .
  48
  49 definition Bot_elim ≝ λP:Prop.λx:Bot.
  50   match x in Bot return λx.P with [].
  51
  52 definition Not := λA:Prop.Imply A Bot.
  53
  54 definition Not_intro : ∀A.(A → Bot) → Not A ≝  λA.
  55   Imply_intro A Bot.
  56
  57 definition Not_elim : ∀A.Not A → A → Bot ≝ λA.
  58   Imply_elim ? Bot.
  59
  60 definition Discharge := λA:Prop.λa:A.
  61   a.
  62
  63 axiom Raa : ∀A.(Not A → Bot) → A.
  64
  65 axiom sort : Type[0].
  66
  67 inductive Exists (A:Type[0]) (P:A→Prop) : Prop ≝
  68   Exists_intro: ∀w:A. P w → Exists A P.
  69
  70 definition Exists_elim ≝
  71   λA:Type[0].λP:A→Prop.λC:Prop.λc:Exists A P.λH:(Πx.P x → C).
  72    match c with [ Exists_intro w p ⇒ H w p ].
  73
  74 inductive Forall (A:Type[0]) (P:A→Prop) : Prop ≝
  75  Forall_intro: (∀n:A. P n) → Forall A P.
  76
  77 definition Forall_elim ≝
  78  λA:Type[0].λP:A→Prop.λn:A.λf:Forall A P.match f with [ Forall_intro g ⇒ g n ].
  79
  80 (* Dummy proposition *)
  81 axiom unit : Prop.
  82
  83 (* Notations *)
  84 notation "hbox(a break ⇒ b)" right associative with precedence 20
  85 for @{ 'Imply $a $b }.
  86 interpretation "Imply" 'Imply a b = (Imply a b).
  87 interpretation "constructive or" 'or x y = (Or x y).
  88 interpretation "constructive and" 'and x y = (And x y).
  89 notation "⊤" non associative with precedence 90 for @{'Top}.
  90 interpretation "Top" 'Top = Top.
  91 notation "⊥" non associative with precedence 90 for @{'Bot}.
  92 interpretation "Bot" 'Bot = Bot.
  93 interpretation "Not" 'not a = (Not a).
  94 notation "✶" non associative with precedence 90 for @{'unit}.
  95 interpretation "dummy prop" 'unit = unit.
  96 notation > "\exists list1 ident x sep , . term 19 Px" with precedence 20
  97 for ${ fold right @{$Px} rec acc @{'myexists (λ${ident x}.$acc)} }.
  98 notation < "hvbox(\exists ident i break . p)" with precedence 20
  99 for @{ 'myexists (\lambda ${ident i} : $ty. $p) }.
 100 interpretation "constructive ex" 'myexists \eta.x = (Exists sort x).
 101 notation > "\forall ident x.break term 19 Px" with precedence 20
 102 for @{ 'Forall (λ${ident x}.$Px) }.
 103 notation < "\forall ident x.break term 19 Px" with precedence 20
 104 for @{ 'Forall (λ${ident x}:$tx.$Px) }.
 105 interpretation "Forall" 'Forall \eta.Px = (Forall ? Px).
 106
 107 (* Variables *)
 108 axiom A : Prop.
 109 axiom B : Prop.
 110 axiom C : Prop.
 111 axiom D : Prop.
 112 axiom E : Prop.
 113 axiom F : Prop.
 114 axiom G : Prop.
 115 axiom H : Prop.
 116 axiom I : Prop.
 117 axiom J : Prop.
 118 axiom K : Prop.
 119 axiom L : Prop.
 120 axiom M : Prop.
 121 axiom N : Prop.
 122 axiom O : Prop.
 123 axiom  x: sort.
 124 axiom  y: sort.
 125 axiom  z: sort.
 126 axiom  w: sort.
 127
 128 (* Every formula user provided annotates its proof:
 129    `A` becomes `(show A ?)` *)
 130 definition show : ΠA.A→A ≝ λA:Prop.λa:A.a.
 131
 132 (* When something does not fit, this daemon is used *)
 133 axiom cast: ΠA,B:Prop.B → A.
 134
 135 (* begin a proof: draws the root *)
 136 notation > "'prove' p" non associative with precedence 19
 137 for @{ 'prove $p }.
 138 interpretation "prove KO" 'prove p = (cast ? ? (show p ?)).
 139 interpretation "prove OK" 'prove p = (show p ?).
 140
 141 (* Leaves *)
 142 notation < "\infrule (t\atop ⋮) a ?" with precedence 19
 143 for @{ 'leaf_ok $a $t }.
 144 interpretation "leaf OK" 'leaf_ok a t = (show a t).
 145 notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19
 146 for @{ 'leaf_ko $a $t }.
 147 interpretation "leaf KO" 'leaf_ko a t = (cast ? ? (show a t)).
 148
 149 (* discharging *)
 150 notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19
 151 for @{ 'discharge_ko_1 $a $H }.
 152 interpretation "discharge_ko_1" 'discharge_ko_1 a H =
 153   (show a (cast ? ? (Discharge ? H))).
 154 notation < "[ mstyle color #ff0000 (a) ] \sup mstyle color #ff0000 (H)" with precedence 19
 155 for @{ 'discharge_ko_2 $a $H }.
 156 interpretation "discharge_ko_2" 'discharge_ko_2 a H =
 157   (cast ? ? (show a (cast ? ? (Discharge ? H)))).
 158
 159 notation < "[ a ] \sup H" with precedence 19
 160 for @{ 'discharge_ok_1 $a $H }.
 161 interpretation "discharge_ok_1" 'discharge_ok_1 a H =
 162   (show a (Discharge ? H)).
 163 notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19
 164 for @{ 'discharge_ok_2 $a $H }.
 165 interpretation "discharge_ok_2" 'discharge_ok_2 a H =
 166   (cast ? ? (show a (Discharge ? H))).
 167
 168 notation > "'discharge' [H]" with precedence 19
 169 for @{ 'discharge $H }.
 170 interpretation "discharge KO" 'discharge H = (cast ? ? (Discharge ? H)).
 171 interpretation "discharge OK" 'discharge H = (Discharge ? H).
 172
 173 (* ⇒ introduction *)
 174 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
 175 for @{ 'Imply_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
 176 interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b =
 177   (show ab (cast ? ? (Imply_intro ? ? b))).
 178
 179 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
 180 for @{ 'Imply_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
 181 interpretation "Imply_intro_ko_2" 'Imply_intro_ko_2 ab \eta.b =
 182   (cast ? ? (show ab (cast ? ? (Imply_intro ? ? b)))).
 183
 184 notation < "maction (\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) ) (\vdots)" with precedence 19
 185 for @{ 'Imply_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
 186 interpretation "Imply_intro_ok_1" 'Imply_intro_ok_1 ab \eta.b =
 187   (show ab (Imply_intro ? ? b)).
 188
 189 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (⇒\sub\i \emsp ident H) " with precedence 19
 190 for @{ 'Imply_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
 191 interpretation "Imply_intro_ok_2" 'Imply_intro_ok_2 ab \eta.b =
 192   (cast ? ? (show ab (Imply_intro ? ? b))).
 193
 194 notation > "⇒#'i' [ident H] term 90 b" with precedence 19
 195 for @{ 'Imply_intro $b (λ${ident H}.show $b ?) }.
 196
 197 interpretation "Imply_intro KO" 'Imply_intro b pb =
 198   (cast ? (Imply unit b) (Imply_intro ? b pb)).
 199 interpretation "Imply_intro OK" 'Imply_intro b pb =
 200   (Imply_intro ? b pb).
 201
 202 (* ⇒ elimination *)
 203 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19
 204 for @{ 'Imply_elim_ko_1 $ab $a $b }.
 205 interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b =
 206   (show b (cast ? ? (Imply_elim ? ? (cast ? ? ab) (cast ? ? a)))).
 207
 208 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19
 209 for @{ 'Imply_elim_ko_2 $ab $a $b }.
 210 interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b =
 211   (cast ? ? (show b (cast ? ? (Imply_elim ? ? (cast ? ? ab) (cast ? ? a))))).
 212
 213 notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) ) (\vdots)" with precedence 19
 214 for @{ 'Imply_elim_ok_1 $ab $a $b }.
 215 interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b =
 216   (show b (Imply_elim ? ? ab a)).
 217
 218 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (⇒\sub\e) " with precedence 19
 219 for @{ 'Imply_elim_ok_2 $ab $a $b }.
 220 interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b =
 221   (cast ? ? (show b (Imply_elim ? ? ab a))).
 222
 223 notation > "⇒#'e' term 90 ab term 90 a" with precedence 19
 224 for @{ 'Imply_elim (show $ab ?) (show $a ?) }.
 225 interpretation "Imply_elim KO" 'Imply_elim ab a =
 226   (cast ? ? (Imply_elim ? ? (cast (Imply unit unit) ? ab) (cast unit ? a))).
 227 interpretation "Imply_elim OK" 'Imply_elim ab a =
 228   (Imply_elim ? ? ab a).
 229
 230 (* ∧ introduction *)
 231 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19
 232 for @{ 'And_intro_ko_1 $a $b $ab }.
 233 interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab =
 234   (show ab (cast ? ? (And_intro ? ? a b))).
 235
 236 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19
 237 for @{ 'And_intro_ko_2 $a $b $ab }.
 238 interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab =
 239   (cast ? ? (show ab (cast ? ? (And_intro ? ? a b)))).
 240
 241 notation < "maction (\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)) (\vdots)" with precedence 19
 242 for @{ 'And_intro_ok_1 $a $b $ab }.
 243 interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab =
 244   (show ab (And_intro ? ? a b)).
 245
 246 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) (∧\sub\i)" with precedence 19
 247 for @{ 'And_intro_ok_2 $a $b $ab }.
 248 interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab =
 249   (cast ? ? (show ab (And_intro ? ? a b))).
 250
 251 notation > "∧#'i' term 90 a term 90 b" with precedence 19
 252 for @{ 'And_intro (show $a ?) (show $b ?) }.
 253 interpretation "And_intro KO" 'And_intro a b = (cast ? ? (And_intro ? ? a b)).
 254 interpretation "And_intro OK" 'And_intro a b = (And_intro ? ? a b).
 255
 256 (* ∧ elimination *)
 257 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
 258 for @{ 'And_elim_l_ko_1 $ab $a }.
 259 interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a =
 260   (show a (cast ? ? (And_elim_l ? ? (cast ? ? ab)))).
 261
 262 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
 263 for @{ 'And_elim_l_ko_2 $ab $a }.
 264 interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a =
 265   (cast ? ? (show a (cast ? ? (And_elim_l ? ? (cast ? ? ab))))).
 266
 267 notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))) (\vdots)" with precedence 19
 268 for @{ 'And_elim_l_ok_1 $ab $a }.
 269 interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a =
 270   (show a (And_elim_l ? ? ab)).
 271
 272 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\l))" with precedence 19
 273 for @{ 'And_elim_l_ok_2 $ab $a }.
 274 interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a =
 275   (cast ? ? (show a (And_elim_l ? ? ab))).
 276
 277 notation > "∧#'e_l' term 90 ab" with precedence 19
 278 for @{ 'And_elim_l (show $ab ?) }.
 279 interpretation "And_elim_l KO" 'And_elim_l a = (cast ? ? (And_elim_l ? ? (cast (And unit unit) ? a))).
 280 interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l ? ? a).
 281
 282 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
 283 for @{ 'And_elim_r_ko_1 $ab $a }.
 284 interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a =
 285   (show a (cast ? ? (And_elim_r ? ? (cast ? ? ab)))).
 286
 287 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
 288 for @{ 'And_elim_r_ko_2 $ab $a }.
 289 interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a =
 290   (cast ? ? (show a (cast ? ? (And_elim_r ? ? (cast ? ? ab))))).
 291
 292 notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))) (\vdots)" with precedence 19
 293 for @{ 'And_elim_r_ok_1 $ab $a }.
 294 interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a =
 295   (show a (And_elim_r ? ? ab)).
 296
 297 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\r))" with precedence 19
 298 for @{ 'And_elim_r_ok_2 $ab $a }.
 299 interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a =
 300   (cast ? ? (show a (And_elim_r ? ? ab))).
 301
 302 notation > "∧#'e_r' term 90 ab" with precedence 19
 303 for @{ 'And_elim_r (show $ab ?) }.
 304 interpretation "And_elim_r KO" 'And_elim_r a = (cast ? ? (And_elim_r ? ? (cast (And unit unit) ? a))).
 305 interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r ? ? a).
 306
 307 (* ∨ introduction *)
 308 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
 309 for @{ 'Or_intro_l_ko_1 $a $ab }.
 310 interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab =
 311   (show ab (cast ? ? (Or_intro_l ? ? a))).
 312
 313 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
 314 for @{ 'Or_intro_l_ko_2 $a $ab }.
 315 interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab =
 316   (cast ? ? (show ab (cast ? ? (Or_intro_l ? ? a)))).
 317
 318 notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))) (\vdots)" with precedence 19
 319 for @{ 'Or_intro_l_ok_1 $a $ab }.
 320 interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab =
 321   (show ab (Or_intro_l ? ? a)).
 322
 323 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19
 324 for @{ 'Or_intro_l_ok_2 $a $ab }.
 325 interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab =
 326   (cast ? ? (show ab (Or_intro_l ? ? a))).
 327
 328 notation > "∨#'i_l' term 90 a" with precedence 19
 329 for @{ 'Or_intro_l (show $a ?) }.
 330 interpretation "Or_intro_l KO" 'Or_intro_l a = (cast ? (Or ? unit) (Or_intro_l ? ? a)).
 331 interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l ? ? a).
 332
 333 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
 334 for @{ 'Or_intro_r_ko_1 $a $ab }.
 335 interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab =
 336   (show ab (cast ? ? (Or_intro_r ? ? a))).
 337
 338 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
 339 for @{ 'Or_intro_r_ko_2 $a $ab }.
 340 interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab =
 341   (cast ? ? (show ab (cast ? ? (Or_intro_r ? ? a)))).
 342
 343 notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))) (\vdots)" with precedence 19
 344 for @{ 'Or_intro_r_ok_1 $a $ab }.
 345 interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab =
 346   (show ab (Or_intro_r ? ? a)).
 347
 348 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19
 349 for @{ 'Or_intro_r_ok_2 $a $ab }.
 350 interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab =
 351   (cast ? ? (show ab (Or_intro_r ? ? a))).
 352
 353 notation > "∨#'i_r' term 90 a" with precedence 19
 354 for @{ 'Or_intro_r (show $a ?) }.
 355 interpretation "Or_intro_r KO" 'Or_intro_r a = (cast ? (Or unit ?) (Or_intro_r ? ? a)).
 356 interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r ? ? a).
 357
 358 (* ∨ elimination *)
 359 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (mstyle color #ff0000 (∨\sub\e \emsp) ident Ha \emsp ident Hb)" with precedence 19
 360 for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }.
 361 interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc =
 362   (show c (cast ? ? (Or_elim ? ? ? (cast ? ? ab) (cast ? ? ac) (cast ? ? bc)))).
 363
 364 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∨\sub\e) \emsp ident Ha \emsp ident Hb)" with precedence 19
 365 for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 366 interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c =
 367   (cast ? ? (show c (cast ? ? (Or_elim ? ? ? (cast ? ? ab) (cast ? ? ac) (cast ? ? bc))))).
 368
 369 notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)) (\vdots)" with precedence 19
 370 for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 371 interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c =
 372   (show c (Or_elim ? ? ? ab ac bc)).
 373
 374 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
 375 for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 376 interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c =
 377   (cast ? ? (show c (Or_elim ? ? ? ab ac bc))).
 378
 379 definition unit_to ≝ λx:Prop.unit → x.
 380
 381 notation > "∨#'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19
 382 for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) }.
 383 interpretation "Or_elim KO" 'Or_elim ab ac bc =
 384   (cast ? ? (Or_elim ? ? ?
 385     (cast (Or unit unit) ? ab)
 386     (cast (unit_to unit) (unit_to ?) ac)
 387     (cast (unit_to unit) (unit_to ?) bc))).
 388 interpretation "Or_elim OK" 'Or_elim ab ac bc = (Or_elim ? ? ? ab ac bc).
 389
 390 (* ⊤ introduction *)
 391 notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19
 392 for @{'Top_intro_ko_1}.
 393 interpretation "Top_intro_ko_1" 'Top_intro_ko_1 =
 394   (show ? (cast ? ? Top_intro)).
 395
 396 notation < "\infrule \nbsp mstyle color #ff0000 (⊤) mstyle color #ff0000 (⊤\sub\i)" with precedence 19
 397 for @{'Top_intro_ko_2}.
 398 interpretation "Top_intro_ko_2" 'Top_intro_ko_2 =
 399   (cast ? ? (show ? (cast ? ? Top_intro))).
 400
 401 notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19
 402 for @{'Top_intro_ok_1}.
 403 interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show ? Top_intro).
 404
 405 notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19
 406 for @{'Top_intro_ok_2 }.
 407 interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast ? ? (show ? Top_intro)).
 408
 409 notation > "⊤#'i'" with precedence 19 for @{ 'Top_intro }.
 410 interpretation "Top_intro KO" 'Top_intro = (cast ? ? Top_intro).
 411 interpretation "Top_intro OK" 'Top_intro = Top_intro.
 412
 413 (* ⊥ introduction *)
 414 notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19
 415 for @{'Bot_elim_ko_1 $a $b}.
 416 interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b =
 417   (show a (Bot_elim ? (cast ? ? b))).
 418
 419 notation < "\infrule b mstyle color #ff0000 (a) mstyle color #ff0000 (⊥\sub\e)" with precedence 19
 420 for @{'Bot_elim_ko_2 $a $b}.
 421 interpretation "Bot_elim_ko_2" 'Bot_elim_ko_2 a b =
 422   (cast ? ? (show a (Bot_elim ? (cast ? ? b)))).
 423
 424 notation < "maction (\infrule b a (⊥\sub\e)) (\vdots)" with precedence 19
 425 for @{'Bot_elim_ok_1 $a $b}.
 426 interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b =
 427   (show a (Bot_elim ? b)).
 428
 429 notation < "\infrule b mstyle color #ff0000 (a) (⊥\sub\e)" with precedence 19
 430 for @{'Bot_elim_ok_2 $a $b}.
 431 interpretation "Bot_elim_ok_2" 'Bot_elim_ok_2 a b =
 432   (cast ? ? (show a (Bot_elim ? b))).
 433
 434 notation > "⊥#'e' term 90 b" with precedence 19
 435 for @{ 'Bot_elim (show $b ?) }.
 436 interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim ? (cast ? ? a)).
 437 interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim ? a).
 438
 439 (* ¬ introduction *)
 440 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
 441 for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
 442 interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b =
 443   (show ab (cast ? ? (Not_intro ? (cast ? ? b)))).
 444
 445 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
 446 for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
 447 interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b =
 448   (cast ? ? (show ab (cast ? ? (Not_intro ? (cast ? ? b))))).
 449
 450 notation < "maction (\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) ) (\vdots)" with precedence 19
 451 for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
 452 interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b =
 453   (show ab (Not_intro ? b)).
 454
 455 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub(\emsp\i) \emsp ident H) " with precedence 19
 456 for @{ 'Not_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
 457 interpretation "Not_intro_ok_2" 'Not_intro_ok_2 ab \eta.b =
 458   (cast ? ? (show ab (Not_intro ? b))).
 459
 460 notation > "¬#'i' [ident H] term 90 b" with precedence 19
 461 for @{ 'Not_intro (λ${ident H}.show $b ?) }.
 462 interpretation "Not_intro KO" 'Not_intro a = (cast ? ? (Not_intro ? (cast ? ? a))).
 463 interpretation "Not_intro OK" 'Not_intro a = (Not_intro ? a).
 464
 465 (* ¬ elimination *)
 466 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19
 467 for @{ 'Not_elim_ko_1 $ab $a $b }.
 468 interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b =
 469   (show b (cast ? ? (Not_elim ? (cast ? ? ab) (cast ? ? a)))).
 470
 471 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19
 472 for @{ 'Not_elim_ko_2 $ab $a $b }.
 473 interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b =
 474   (cast ? ? (show b (cast ? ? (Not_elim ? (cast ? ? ab) (cast ? ? a))))).
 475
 476 notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) ) (\vdots)" with precedence 19
 477 for @{ 'Not_elim_ok_1 $ab $a $b }.
 478 interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b =
 479   (show b (Not_elim ? ab a)).
 480
 481 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub(\emsp\e)) " with precedence 19
 482 for @{ 'Not_elim_ok_2 $ab $a $b }.
 483 interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b =
 484   (cast ? ? (show b (Not_elim ? ab a))).
 485
 486 notation > "¬#'e' term 90 ab term 90 a" with precedence 19
 487 for @{ 'Not_elim (show $ab ?) (show $a ?) }.
 488 interpretation "Not_elim KO" 'Not_elim ab a =
 489   (cast ? ? (Not_elim unit (cast ? ? ab) (cast ? ? a))).
 490 interpretation "Not_elim OK" 'Not_elim ab a =
 491   (Not_elim ? ab a).
 492
 493 (* RAA *)
 494 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
 495 for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
 496 interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn =
 497   (show Pn (cast ? ? (Raa ? (cast ? ? Px)))).
 498
 499 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
 500 for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
 501 interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn =
 502   (cast ? ? (show Pn (cast ? ? (Raa ? (cast ? ? Px))))).
 503
 504 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)) (\vdots)" with precedence 19
 505 for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
 506 interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn =
 507   (show Pn (Raa ? Px)).
 508
 509 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (\RAA \emsp ident x)" with precedence 19
 510 for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
 511 interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn =
 512   (cast ? ? (show Pn (Raa ? Px))).
 513
 514 notation > "'RAA' [ident H] term 90 b" with precedence 19
 515 for @{ 'Raa (λ${ident H}.show $b ?) }.
 516 interpretation "RAA KO" 'Raa p = (cast ? unit (Raa ? (cast ? (unit_to ?) p))).
 517 interpretation "RAA OK" 'Raa p = (Raa ? p).
 518
 519 (* ∃ introduction *)
 520 notation < "\infrule hbox(\emsp Pn \emsp) Px mstyle color #ff0000 (∃\sub\i)" with precedence 19
 521 for @{ 'Exists_intro_ko_1 $Pn $Px }.
 522 interpretation "Exists_intro_ko_1" 'Exists_intro_ko_1 Pn Px =
 523   (show Px (cast ? ? (Exists_intro ? ? ? (cast ? ? Pn)))).
 524
 525 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) mstyle color #ff0000 (∃\sub\i)" with precedence 19
 526 for @{ 'Exists_intro_ko_2 $Pn $Px }.
 527 interpretation "Exists_intro_ko_2" 'Exists_intro_ko_2 Pn Px =
 528   (cast ? ? (show Px (cast ? ? (Exists_intro ? ? ? (cast ? ? Pn))))).
 529
 530 notation < "maction (\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)) (\vdots)" with precedence 19
 531 for @{ 'Exists_intro_ok_1 $Pn $Px }.
 532 interpretation "Exists_intro_ok_1" 'Exists_intro_ok_1 Pn Px =
 533   (show Px (Exists_intro ? ? ? Pn)).
 534
 535 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) (∃\sub\i)" with precedence 19
 536 for @{ 'Exists_intro_ok_2 $Pn $Px }.
 537 interpretation "Exists_intro_ok_2" 'Exists_intro_ok_2 Pn Px =
 538   (cast ? ? (show Px (Exists_intro ? ? ? Pn))).
 539
 540 notation >"∃#'i' {term 90 t} term 90 Pt" non associative with precedence 19
 541 for @{'Exists_intro $t (λw.? w) (show $Pt ?)}.
 542 interpretation "Exists_intro KO" 'Exists_intro t P Pt =
 543  (cast ? ? (Exists_intro sort P t (cast ? ? Pt))).
 544 interpretation "Exists_intro OK" 'Exists_intro t P Pt =
 545  (Exists_intro sort P t Pt).
 546
 547 (* ∃ elimination *)
 548 notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (mstyle color #ff0000 (∃\sub\e) \emsp ident n \emsp ident HPn)" with precedence 19
 549 for @{ 'Exists_elim_ko_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 550 interpretation "Exists_elim_ko_1" 'Exists_elim_ko_1 ExPx Pc c =
 551     (show c (cast ? ? (Exists_elim ? ? ? (cast ? ? ExPx) (cast ? ? Pc)))).
 552
 553 notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∃\sub\e) \emsp ident n \emsp ident HPn)" with precedence 19
 554 for @{ 'Exists_elim_ko_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 555 interpretation "Exists_elim_ko_2" 'Exists_elim_ko_2 ExPx Pc c =
 556     (cast ? ? (show c (cast ? ? (Exists_elim ? ? ? (cast ? ? ExPx) (cast ? ? Pc))))).
 557
 558 notation < "maction (\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)) (\vdots)" with precedence 19
 559 for @{ 'Exists_elim_ok_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 560 interpretation "Exists_elim_ok_1" 'Exists_elim_ok_1 ExPx Pc c =
 561     (show c (Exists_elim ? ? ? ExPx Pc)).
 562
 563 notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) mstyle color #ff0000 (c) (∃\sub\e \emsp ident n \emsp ident HPn)" with precedence 19
 564 for @{ 'Exists_elim_ok_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 565 interpretation "Exists_elim_ok_2" 'Exists_elim_ok_2 ExPx Pc c =
 566     (cast ? ? (show c (Exists_elim ? ? ? ExPx Pc))).
 567
 568 definition ex_concl := λx:sort → Prop.Πy:sort.unit → x y.
 569 definition ex_concl_dummy := Πy:sort.unit → unit.
 570 definition fake_pred := λx:sort.unit.
 571
 572 notation >"∃#'e' term 90 ExPt {ident t} [ident H] term 90 c" non associative with precedence 19
 573 for @{'Exists_elim (λx.? x) (show $ExPt ?) (λ${ident t}:sort.λ${ident H}.show $c ?)}.
 574 interpretation "Exists_elim KO" 'Exists_elim P ExPt c =
 575  (cast ? ? (Exists_elim sort P ?
 576    (cast (Exists ? P)  ? ExPt)
 577    (cast ex_concl_dummy (ex_concl ?) c))).
 578 interpretation "Exists_elim OK" 'Exists_elim P ExPt c =
 579  (Exists_elim sort P ? ExPt c).
 580
 581 (* ∀ introduction *)
 582
 583 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
 584 for @{ 'Forall_intro_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
 585 interpretation "Forall_intro_ko_1" 'Forall_intro_ko_1 Px Pn =
 586   (show Pn (cast ? ? (Forall_intro ? ? (cast ? ? Px)))).
 587
 588 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
 589 for @{ 'Forall_intro_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
 590 interpretation "Forall_intro_ko_2" 'Forall_intro_ko_2 Px Pn =
 591   (cast ? ? (show Pn (cast ? ? (Forall_intro ? ? (cast ? ? Px))))).
 592
 593 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)) (\vdots)" with precedence 19
 594 for @{ 'Forall_intro_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
 595 interpretation "Forall_intro_ok_1" 'Forall_intro_ok_1 Px Pn =
 596   (show Pn (Forall_intro ? ? Px)).
 597
 598 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\i \emsp ident x)" with precedence 19
 599 for @{ 'Forall_intro_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
 600 interpretation "Forall_intro_ok_2" 'Forall_intro_ok_2 Px Pn =
 601   (cast ? ? (show Pn (Forall_intro ? ? Px))).
 602
 603 notation > "∀#'i' {ident y} term 90 Px" non associative with precedence 19
 604 for @{ 'Forall_intro (λ_.?) (λ${ident y}.show $Px ?) }.
 605 interpretation "Forall_intro KO" 'Forall_intro P Px =
 606   (cast ? ? (Forall_intro sort P (cast ? ? Px))).
 607 interpretation "Forall_intro OK" 'Forall_intro P Px =
 608   (Forall_intro sort P Px).
 609
 610 (* ∀ elimination *)
 611 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\e))" with precedence 19
 612 for @{ 'Forall_elim_ko_1 $Px $Pn }.
 613 interpretation "Forall_elim_ko_1" 'Forall_elim_ko_1 Px Pn =
 614   (show Pn (cast ? ? (Forall_elim ? ? ? (cast ? ? Px)))).
 615
 616 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\e))" with precedence 19
 617 for @{ 'Forall_elim_ko_2 $Px $Pn }.
 618 interpretation "Forall_elim_ko_2" 'Forall_elim_ko_2 Px Pn =
 619   (cast ? ? (show Pn (cast ? ? (Forall_elim ? ? ? (cast ? ? Px))))).
 620
 621 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)) (\vdots)" with precedence 19
 622 for @{ 'Forall_elim_ok_1 $Px $Pn }.
 623 interpretation "Forall_elim_ok_1" 'Forall_elim_ok_1 Px Pn =
 624   (show Pn (Forall_elim ? ? ? Px)).
 625
 626 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\e)" with precedence 19
 627 for @{ 'Forall_elim_ok_2 $Px $Pn }.
 628 interpretation "Forall_elim_ok_2" 'Forall_elim_ok_2 Px Pn =
 629   (cast ? ? (show Pn (Forall_elim ? ? ? Px))).
 630
 631 notation > "∀#'e' {term 90 t} term 90 Pn" non associative with precedence 19
 632 for @{ 'Forall_elim (λ_.?) $t (show $Pn ?) }.
 633 interpretation "Forall_elim KO" 'Forall_elim P t Px =
 634   (cast ? unit (Forall_elim sort P t (cast ? ? Px))).
 635 interpretation "Forall_elim OK" 'Forall_elim P t Px =
 636   (Forall_elim sort P t Px).
 637
 638 (* already proved lemma *)
 639 definition hide_args : ΠA:Type[0].A→A := λA:Type[0].λa:A.a.
 640 notation < "t" non associative with precedence 90 for @{'hide_args $t}.
 641 interpretation "hide 0 args"  'hide_args t = (hide_args ? t).
 642 interpretation "hide 1 args"  'hide_args t = (hide_args ? t ?).
 643 interpretation "hide 2 args"  'hide_args t = (hide_args ? t ? ?).
 644 interpretation "hide 3 args"  'hide_args t = (hide_args ? t ? ? ?).
 645 interpretation "hide 4 args"  'hide_args t = (hide_args ? t ? ? ? ?).
 646 interpretation "hide 5 args"  'hide_args t = (hide_args ? t ? ? ? ? ?).
 647 interpretation "hide 6 args"  'hide_args t = (hide_args ? t ? ? ? ? ? ?).
 648 interpretation "hide 7 args"  'hide_args t = (hide_args ? t ? ? ? ? ? ? ?).
 649
 650 (* more args crashes the pattern matcher *)
 651
 652 (* already proved lemma, 0 assumptions *)
 653 definition Lemma : ΠA.A→A ≝ λA:Prop.λa:A.a.
 654
 655 notation < "\infrule
 656          (\infrule
 657              (\emsp)
 658              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 659          p \nbsp"
 660 non associative with precedence 19
 661 for @{ 'lemma_ko_1 $p ($H : $_) }.
 662 interpretation "lemma_ko_1" 'lemma_ko_1 p H =
 663   (show p (cast ? ? (Lemma ? (cast ? ? H)))).
 664
 665 notation < "\infrule
 666          (\infrule
 667              (\emsp)
 668              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 669          mstyle color #ff0000 (p) \nbsp"
 670 non associative with precedence 19
 671 for @{ 'lemma_ko_2 $p ($H : $_) }.
 672 interpretation "lemma_ko_2" 'lemma_ko_2 p H =
 673   (cast ? ? (show p (cast ? ?
 674     (Lemma ? (cast ? ? H))))).
 675
 676
 677 notation < "\infrule
 678          (\infrule
 679              (\emsp)
 680              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 681          p \nbsp"
 682 non associative with precedence 19
 683 for @{ 'lemma_ok_1 $p ($H : $_) }.
 684 interpretation "lemma_ok_1" 'lemma_ok_1 p H =
 685   (show p (Lemma ? H)).
 686
 687 notation < "\infrule
 688          (\infrule
 689              (\emsp)
 690              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 691          mstyle color #ff0000 (p) \nbsp"
 692 non associative with precedence 19
 693 for @{ 'lemma_ok_2 $p ($H : $_) }.
 694 interpretation "lemma_ok_2" 'lemma_ok_2 p H =
 695   (cast ? ? (show p (Lemma ? H))).
 696
 697 notation > "'lem' 0 term 90 l" non associative with precedence 19
 698 for @{ 'Lemma (hide_args ? $l : ?) }.
 699 interpretation "lemma KO" 'Lemma l =
 700   (cast ? ? (Lemma unit (cast unit ? l))).
 701 interpretation "lemma OK" 'Lemma l = (Lemma ? l).
 702
 703
 704 (* already proved lemma, 1 assumption *)
 705 definition Lemma1 : ΠA,B. (A ⇒ B) → A → B ≝
 706  λA,B:Prop.λf:A⇒B.λa:A.
 707   Imply_elim A B f a.
 708
 709 notation < "\infrule
 710          (\infrule
 711              (\emsp a \emsp)
 712              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 713          p \nbsp"
 714 non associative with precedence 19
 715 for @{ 'lemma1_ko_1 $a $p ($H : $_) }.
 716 interpretation "lemma1_ko_1" 'lemma1_ko_1 a p H =
 717   (show p (cast ? ? (Lemma1 ? ? (cast ? ? H) (cast ? ? a)))).
 718
 719 notation < "\infrule
 720          (\infrule
 721              (\emsp a \emsp)
 722              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 723          mstyle color #ff0000 (p) \nbsp"
 724 non associative with precedence 19
 725 for @{ 'lemma1_ko_2 $a $p ($H : $_) }.
 726 interpretation "lemma1_ko_2" 'lemma1_ko_2 a p H =
 727   (cast ? ? (show p (cast ? ?
 728     (Lemma1 ? ? (cast ? ? H) (cast ? ? a))))).
 729
 730
 731 notation < "\infrule
 732          (\infrule
 733              (\emsp a \emsp)
 734              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 735          p \nbsp"
 736 non associative with precedence 19
 737 for @{ 'lemma1_ok_1 $a $p ($H : $_) }.
 738 interpretation "lemma1_ok_1" 'lemma1_ok_1 a p H =
 739   (show p (Lemma1 ? ? H a)).
 740
 741 notation < "\infrule
 742          (\infrule
 743              (\emsp a \emsp)
 744              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 745          mstyle color #ff0000 (p) \nbsp"
 746 non associative with precedence 19
 747 for @{ 'lemma1_ok_2 $a $p ($H : $_) }.
 748 interpretation "lemma1_ok_2" 'lemma1_ok_2 a p H =
 749   (cast ? ? (show p (Lemma1 ? ? H a))).
 750
 751
 752 notation > "'lem' 1 term 90 l term 90 p" non associative with precedence 19
 753 for @{ 'Lemma1 (hide_args ? $l : ?) (show $p ?) }.
 754 interpretation "lemma 1 KO" 'Lemma1 l p =
 755   (cast ? ? (Lemma1 unit unit (cast (Imply unit unit) ? l) (cast unit ? p))).
 756 interpretation "lemma 1 OK" 'Lemma1 l p = (Lemma1 ? ? l p).
 757
 758 (* already proved lemma, 2 assumptions *)
 759 definition Lemma2 : ΠA,B,C. (A ⇒ B ⇒ C) → A → B → C ≝
 760  λA,B,C:Prop.λf:A⇒B⇒C.λa:A.λb:B.
 761   Imply_elim B C (Imply_elim A (B⇒C) f a) b.
 762
 763 notation < "\infrule
 764          (\infrule
 765              (\emsp a \emsp\emsp\emsp b \emsp)
 766              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 767          p \nbsp"
 768 non associative with precedence 19
 769 for @{ 'lemma2_ko_1 $a $b $p ($H : $_) }.
 770 interpretation "lemma2_ko_1" 'lemma2_ko_1 a b p H =
 771   (show p (cast ? ? (Lemma2 ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b)))).
 772
 773 notation < "\infrule
 774          (\infrule
 775              (\emsp a \emsp\emsp\emsp b \emsp)
 776              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 777          mstyle color #ff0000 (p) \nbsp"
 778 non associative with precedence 19
 779 for @{ 'lemma2_ko_2 $a $b $p ($H : $_) }.
 780 interpretation "lemma2_ko_2" 'lemma2_ko_2 a b p H =
 781   (cast ? ? (show p (cast ? ?
 782     (Lemma2 ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b))))).
 783
 784
 785 notation < "\infrule
 786          (\infrule
 787              (\emsp a \emsp\emsp\emsp b \emsp)
 788              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 789          p \nbsp"
 790 non associative with precedence 19
 791 for @{ 'lemma2_ok_1 $a $b $p ($H : $_) }.
 792 interpretation "lemma2_ok_1" 'lemma2_ok_1 a b p H =
 793   (show p (Lemma2 ? ? ? H a b)).
 794
 795 notation < "\infrule
 796          (\infrule
 797              (\emsp a \emsp\emsp\emsp b \emsp)
 798              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 799          mstyle color #ff0000 (p) \nbsp"
 800 non associative with precedence 19
 801 for @{ 'lemma2_ok_2 $a $b $p ($H : $_) }.
 802 interpretation "lemma2_ok_2" 'lemma2_ok_2 a b p H =
 803   (cast ? ? (show p (Lemma2 ? ? ? H a b))).
 804
 805 notation > "'lem' 2 term 90 l term 90 p term 90 q" non associative with precedence 19
 806 for @{ 'Lemma2 (hide_args ? $l : ?) (show $p ?) (show $q ?) }.
 807 interpretation "lemma 2 KO" 'Lemma2 l p q =
 808   (cast ? ? (Lemma2 unit unit unit (cast (Imply unit (Imply unit unit)) ? l) (cast unit ? p) (cast unit ? q))).
 809 interpretation "lemma 2 OK" 'Lemma2 l p q = (Lemma2 ? ? ? l p q).
 810
 811 (* already proved lemma, 3 assumptions *)
 812 definition Lemma3 : ΠA,B,C,D. (A ⇒ B ⇒ C ⇒ D) → A → B → C → D ≝
 813  λA,B,C,D:Prop.λf:A⇒B⇒C⇒D.λa:A.λb:B.λc:C.
 814   Imply_elim C D (Imply_elim B (C⇒D) (Imply_elim A (B⇒C⇒D) f a) b) c.
 815
 816 notation < "\infrule
 817          (\infrule
 818              (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
 819              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 820          p \nbsp"
 821 non associative with precedence 19
 822 for @{ 'lemma3_ko_1 $a $b $c $p ($H : $_) }.
 823 interpretation "lemma3_ko_1" 'lemma3_ko_1 a b c p H =
 824   (show p (cast ? ?
 825    (Lemma3 ? ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b) (cast ? ? c)))).
 826
 827 notation < "\infrule
 828          (\infrule
 829              (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
 830              (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
 831          mstyle color #ff0000 (p) \nbsp"
 832 non associative with precedence 19
 833 for @{ 'lemma3_ko_2 $a $b $c $p ($H : $_) }.
 834 interpretation "lemma3_ko_2" 'lemma3_ko_2 a b c p H =
 835   (cast ? ? (show p (cast ? ?
 836     (Lemma3 ? ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b) (cast ? ? c))))).
 837
 838
 839 notation < "\infrule
 840          (\infrule
 841              (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
 842              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 843          p \nbsp"
 844 non associative with precedence 19
 845 for @{ 'lemma3_ok_1 $a $b $c $p ($H : $_) }.
 846 interpretation "lemma3_ok_1" 'lemma3_ok_1 a b c p H =
 847   (show p (Lemma3 ? ? ? ? H a b c)).
 848
 849 notation < "\infrule
 850          (\infrule
 851              (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
 852              (╲ mstyle mathsize normal (H) ╱) \nbsp)
 853          mstyle color #ff0000 (p) \nbsp"
 854 non associative with precedence 19
 855 for @{ 'lemma3_ok_2 $a $b $c $p ($H : $_) }.
 856 interpretation "lemma3_ok_2" 'lemma3_ok_2 a b c p H =
 857   (cast ? ? (show p (Lemma3 ? ? ? ? H a b c))).
 858
 859 notation > "'lem' 3 term 90 l term 90 p term 90 q term 90 r" non associative with precedence 19
 860 for @{ 'Lemma3 (hide_args ? $l : ?) (show $p ?) (show $q ?) (show $r ?) }.
 861 interpretation "lemma 3 KO" 'Lemma3 l p q r =
 862   (cast ? ? (Lemma3 unit unit unit unit (cast (Imply unit (Imply unit (Imply unit unit))) ? l) (cast unit ? p) (cast unit ? q) (cast unit ? r))).
 863 interpretation "lemma 3 OK" 'Lemma3 l p q r = (Lemma3 ? ? ? ? l p q r).