helm/software/matita/library/didactic/support/natural_deduction.ma

   1 (* Logic system *)
   2
   3 inductive Imply (A,B:CProp) : CProp ≝
   4 | Imply_intro: (A → B) → Imply A B.
   5
   6 definition Imply_elim ≝ λA,B.λf:Imply A B. λa:A.
   7   match f with [ Imply_intro g ⇒ g a].
   8
   9 inductive And (A,B:CProp) : CProp ≝
  10 | And_intro: A → B → And A B.
  11
  12 definition And_elim_l ≝ λA,B.λc:And A B.
  13   match c with [ And_intro a b ⇒ a ].
  14
  15 definition And_elim_r ≝ λA,B.λc:And A B.
  16   match c with [ And_intro a b ⇒ b ].
  17
  18 inductive Or (A,B:CProp) : CProp ≝
  19 | Or_intro_l: A → Or A B
  20 | Or_intro_r: B → Or A B.
  21
  22 definition Or_elim ≝ λA,B,C:CProp.λc:Or A B.λfa: A → C.λfb: B → C.
  23   match c with
  24   [ Or_intro_l a ⇒ fa a
  25   | Or_intro_r b ⇒ fb b].
  26
  27 inductive Top : CProp :=
  28 | Top_intro : Top.
  29
  30 inductive Bot : CProp := .
  31
  32 definition Bot_elim ≝ λP:CProp.λx:Bot.
  33   match x in Bot return λx.P with [].
  34
  35 definition Not := λA:CProp.Imply A Bot.
  36
  37 definition Not_intro : ∀A.(A → Bot) → Not A ≝  λA.
  38   Imply_intro A Bot.
  39
  40 definition Not_elim : ∀A.Not A → A → Bot ≝ λA.
  41   Imply_elim ? Bot.
  42
  43 definition Discharge := λA:CProp.λa:A.
  44   a.
  45
  46 axiom Raa : ∀A.(Not A → Bot) → A.
  47
  48 (* Dummy proposition *)
  49 axiom unit : CProp.
  50
  51 (* Notations *)
  52 notation "hbox(a break ⇒ b)" right associative with precedence 20
  53 for @{ 'Imply $a $b }.
  54 interpretation "Imply" 'Imply a b = (Imply a b).
  55 interpretation "constructive or" 'or x y = (Or x y).
  56 interpretation "constructive and" 'and x y = (And x y).
  57 notation "⊤" non associative with precedence 90 for @{'Top}.
  58 interpretation "Top" 'Top = Top.
  59 notation "⊥" non associative with precedence 90 for @{'Bot}.
  60 interpretation "Bot" 'Bot = Bot.
  61 interpretation "Not" 'not a = (Not a).
  62 notation "✶" non associative with precedence 90 for @{'unit}.
  63 interpretation "dummy prop" 'unit = unit.
  64
  65 (* Variables *)
  66 axiom A : CProp.
  67 axiom B : CProp.
  68 axiom C : CProp.
  69 axiom D : CProp.
  70 axiom E : CProp.
  71 axiom F : CProp.
  72 axiom G : CProp.
  73 axiom H : CProp.
  74 axiom I : CProp.
  75 axiom J : CProp.
  76 axiom K : CProp.
  77 axiom L : CProp.
  78 axiom M : CProp.
  79 axiom N : CProp.
  80 axiom O : CProp.
  81 axiom P : CProp.
  82 axiom Q : CProp.
  83 axiom R : CProp.
  84 axiom S : CProp.
  85 axiom T : CProp.
  86 axiom U : CProp.
  87 axiom V : CProp.
  88 axiom W : CProp.
  89 axiom X : CProp.
  90 axiom Y : CProp.
  91 axiom Z : CProp.
  92
  93 (* Every formula user provided annotates its proof:
  94    `A` becomes `(show A ?)` *)
  95 definition show : ∀A.A→A ≝ λA:CProp.λa:A.a.
  96
  97 (* When something does not fit, this daemon is used *)
  98 axiom cast: ∀A,B:CProp.B → A.
  99
 100 (* begin a proof: draws the root *)
 101 notation > "'prove' p" non associative with precedence 19
 102 for @{ 'prove $p }.
 103 interpretation "prove KO" 'prove p = (cast _ _ (show p _)).
 104 interpretation "prove OK" 'prove p = (show p _).
 105
 106 (* Leaves *)
 107 notation < "\infrule (t\atop ⋮) a ?" with precedence 19
 108 for @{ 'leaf_ok $a $t }.
 109 interpretation "leaf OK" 'leaf_ok a t = (show a t).
 110 notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19
 111 for @{ 'leaf_ko $a $t }.
 112 interpretation "leaf KO" 'leaf_ko a t = (cast _ _ (show a t)).
 113
 114 (* already proved lemma *)
 115 definition Lemma : ∀A.A→A ≝ λA:CProp.λa:A.a.
 116
 117 notation < "\infrule \nbsp p mstyle color #ff0000 (\lem\emsp H)" non associative with precedence 19
 118 for @{ 'lemma_ko_1 $p $H }.
 119 interpretation "lemma_ko_1" 'lemma_ko_1 p H =
 120   (show p (cast _ _ (Lemma _ H))).
 121
 122 notation < "\infrule \nbsp mstyle color #ff0000 (p) mstyle color #ff0000 (\lem\emsp H)" non associative with precedence 19
 123 for @{ 'lemma_ko_2 $p $H }.
 124 interpretation "lemma_ko_2" 'lemma_ko_2 p H =
 125   (cast _ _ (show p (cast _ _ (Lemma _ H)))).
 126
 127 notation < "\infrule \nbsp p (\lem\emsp H)" non associative with precedence 19
 128 for @{ 'lemma_ok_1 $p $H }.
 129 interpretation "lemma_ok_1" 'lemma_ok_1 p H =
 130   (show p (Lemma _ H)).
 131 interpretation "lemma_ok_11" 'lemma_ok_1 p H =
 132   (show p (Lemma _ H _)).
 133 interpretation "lemma_ok_111" 'lemma_ok_1 p H =
 134   (show p (Lemma _ H _ _)).
 135
 136 notation < "\infrule \nbsp mstyle color #ff0000 (p) (\lem\emsp H)" non associative with precedence 19
 137 for @{ 'lemma_ok_2 $p $H }.
 138 interpretation "lemma_ok_2" 'lemma_ok_2 p H =
 139   (cast _ _ (show p (Lemma _ H))).
 140 interpretation "lemma_ok_22" 'lemma_ok_2 p H =
 141   (cast _ _ (show p (Lemma _ H _))).
 142 interpretation "lemma_ok_22" 'lemma_ok_2 p H =
 143   (cast _ _ (show p (Lemma _ H _ _))).
 144
 145 notation > "'lem' term 90 p" non associative with precedence 19
 146 for @{ 'Lemma $p  }.
 147 interpretation "lemma KO" 'Lemma p = (cast _ _ (Lemma _ p)).
 148 interpretation "lemma OK" 'Lemma p = (Lemma _ p).
 149
 150
 151 (* discharging *)
 152 notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19
 153 for @{ 'discharge_ko_1 $a $H }.
 154 interpretation "discharge_ko_1" 'discharge_ko_1 a H =
 155   (show a (cast _ _ (Discharge _ H))).
 156 notation < "[ mstyle color #ff0000 (a) ] \sup mstyle color #ff0000 (H)" with precedence 19
 157 for @{ 'discharge_ko_2 $a $H }.
 158 interpretation "discharge_ko_2" 'discharge_ko_2 a H =
 159   (cast _ _ (show a (cast _ _ (Discharge _ H)))).
 160
 161 notation < "[ a ] \sup H" with precedence 19
 162 for @{ 'discharge_ok_1 $a $H }.
 163 interpretation "discharge_ok_1" 'discharge_ok_1 a H =
 164   (show a (Discharge _ H)).
 165 notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19
 166 for @{ 'discharge_ok_2 $a $H }.
 167 interpretation "discharge_ok_2" 'discharge_ok_2 a H =
 168   (cast _ _ (show a (Discharge _ H))).
 169
 170 notation > "'discharge' [H]" with precedence 19
 171 for @{ 'discharge $H }.
 172 interpretation "discharge KO" 'discharge H = (cast _ _ (Discharge _ H)).
 173 interpretation "discharge OK" 'discharge H = (Discharge _ H).
 174
 175 (* ⇒ introduction *)
 176 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
 177 for @{ 'Imply_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
 178 interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b =
 179   (show ab (cast _ _ (Imply_intro _ _ b))).
 180
 181 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
 182 for @{ 'Imply_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
 183 interpretation "Imply_intro_ko_2" 'Imply_intro_ko_2 ab \eta.b =
 184   (cast _ _ (show ab (cast _ _ (Imply_intro _ _ b)))).
 185
 186 notation < "\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) " with precedence 19
 187 for @{ 'Imply_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
 188 interpretation "Imply_intro_ok_1" 'Imply_intro_ok_1 ab \eta.b =
 189   (show ab (Imply_intro _ _ b)).
 190
 191 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (⇒\sub\i \emsp ident H) " with precedence 19
 192 for @{ 'Imply_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
 193 interpretation "Imply_intro_ok_2" 'Imply_intro_ok_2 ab \eta.b =
 194   (cast _ _ (show ab (Imply_intro _ _ b))).
 195
 196 notation > "⇒_'i' [ident H] term 90 b" with precedence 19
 197 for @{ 'Imply_intro $b (λ${ident H}.show $b ?) }.
 198 interpretation "Imply_intro KO" 'Imply_intro b pb =
 199   (cast _ (Imply unit b) (Imply_intro _ b pb)).
 200 interpretation "Imply_intro OK" 'Imply_intro b pb =
 201   (Imply_intro _ b pb).
 202
 203 (* ⇒ elimination *)
 204 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19
 205 for @{ 'Imply_elim_ko_1 $ab $a $b }.
 206 interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b =
 207   (show b (cast _ _ (Imply_elim _ _ (cast _ _ ab) (cast _ _ a)))).
 208
 209 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19
 210 for @{ 'Imply_elim_ko_2 $ab $a $b }.
 211 interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b =
 212   (cast _ _ (show b (cast _ _ (Imply_elim _ _ (cast _ _ ab) (cast _ _ a))))).
 213
 214 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) " with precedence 19
 215 for @{ 'Imply_elim_ok_1 $ab $a $b }.
 216 interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b =
 217   (show b (Imply_elim _ _ ab a)).
 218
 219 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (⇒\sub\e) " with precedence 19
 220 for @{ 'Imply_elim_ok_2 $ab $a $b }.
 221 interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b =
 222   (cast _ _ (show b (Imply_elim _ _ ab a))).
 223
 224 notation > "⇒_'e' term 90 ab term 90 a" with precedence 19
 225 for @{ 'Imply_elim (show $ab ?) (show $a ?) }.
 226 interpretation "Imply_elim KO" 'Imply_elim ab a =
 227   (cast _ _ (Imply_elim _ _ (cast (Imply unit unit) _ ab) (cast unit _ a))).
 228 interpretation "Imply_elim OK" 'Imply_elim ab a =
 229   (Imply_elim _ _ ab a).
 230
 231 (* ∧ introduction *)
 232 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19
 233 for @{ 'And_intro_ko_1 $a $b $ab }.
 234 interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab =
 235   (show ab (cast _ _ (And_intro _ _ a b))).
 236
 237 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19
 238 for @{ 'And_intro_ko_2 $a $b $ab }.
 239 interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab =
 240   (cast _ _ (show ab (cast _ _ (And_intro _ _ a b)))).
 241
 242 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)" with precedence 19
 243 for @{ 'And_intro_ok_1 $a $b $ab }.
 244 interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab =
 245   (show ab (And_intro _ _ a b)).
 246
 247 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) (∧\sub\i)" with precedence 19
 248 for @{ 'And_intro_ok_2 $a $b $ab }.
 249 interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab =
 250   (cast _ _ (show ab (And_intro _ _ a b))).
 251
 252 notation > "∧_'i' term 90 a term 90 b" with precedence 19
 253 for @{ 'And_intro (show $a ?) (show $b ?) }.
 254 interpretation "And_intro KO" 'And_intro a b = (cast _ _ (And_intro _ _ a b)).
 255 interpretation "And_intro OK" 'And_intro a b = (And_intro _ _ a b).
 256
 257 (* ∧ elimination *)
 258 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
 259 for @{ 'And_elim_l_ko_1 $ab $a }.
 260 interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a =
 261   (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab)))).
 262
 263 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
 264 for @{ 'And_elim_l_ko_2 $ab $a }.
 265 interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a =
 266   (cast _ _ (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab))))).
 267
 268 notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))" with precedence 19
 269 for @{ 'And_elim_l_ok_1 $ab $a }.
 270 interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a =
 271   (show a (And_elim_l _ _ ab)).
 272
 273 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\l))" with precedence 19
 274 for @{ 'And_elim_l_ok_2 $ab $a }.
 275 interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a =
 276   (cast _ _ (show a (And_elim_l _ _ ab))).
 277
 278 notation > "∧_'e_l' term 90 ab" with precedence 19
 279 for @{ 'And_elim_l (show $ab ?) }.
 280 interpretation "And_elim_l KO" 'And_elim_l a = (cast _ _ (And_elim_l _ _ (cast (And unit unit) _ a))).
 281 interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l _ _ a).
 282
 283 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
 284 for @{ 'And_elim_r_ko_1 $ab $a }.
 285 interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a =
 286   (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab)))).
 287
 288 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
 289 for @{ 'And_elim_r_ko_2 $ab $a }.
 290 interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a =
 291   (cast _ _ (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab))))).
 292
 293 notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))" with precedence 19
 294 for @{ 'And_elim_r_ok_1 $ab $a }.
 295 interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a =
 296   (show a (And_elim_r _ _ ab)).
 297
 298 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\r))" with precedence 19
 299 for @{ 'And_elim_r_ok_2 $ab $a }.
 300 interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a =
 301   (cast _ _ (show a (And_elim_r _ _ ab))).
 302
 303 notation > "∧_'e_r' term 90 ab" with precedence 19
 304 for @{ 'And_elim_r (show $ab ?) }.
 305 interpretation "And_elim_r KO" 'And_elim_r a = (cast _ _ (And_elim_r _ _ (cast (And unit unit) _ a))).
 306 interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r _ _ a).
 307
 308 (* ∨ introduction *)
 309 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
 310 for @{ 'Or_intro_l_ko_1 $a $ab }.
 311 interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab =
 312   (show ab (cast _ _ (Or_intro_l _ _ a))).
 313
 314 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
 315 for @{ 'Or_intro_l_ko_2 $a $ab }.
 316 interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab =
 317   (cast _ _ (show ab (cast _ _ (Or_intro_l _ _ a)))).
 318
 319 notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))" with precedence 19
 320 for @{ 'Or_intro_l_ok_1 $a $ab }.
 321 interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab =
 322   (show ab (Or_intro_l _ _ a)).
 323
 324 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19
 325 for @{ 'Or_intro_l_ok_2 $a $ab }.
 326 interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab =
 327   (cast _ _ (show ab (Or_intro_l _ _ a))).
 328
 329 notation > "∨_'i_l' term 90 a" with precedence 19
 330 for @{ 'Or_intro_l (show $a ?) }.
 331 interpretation "Or_intro_l KO" 'Or_intro_l a = (cast _ (Or _ unit) (Or_intro_l _ _ a)).
 332 interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l _ _ a).
 333
 334 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
 335 for @{ 'Or_intro_r_ko_1 $a $ab }.
 336 interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab =
 337   (show ab (cast _ _ (Or_intro_r _ _ a))).
 338
 339 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
 340 for @{ 'Or_intro_r_ko_2 $a $ab }.
 341 interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab =
 342   (cast _ _ (show ab (cast _ _ (Or_intro_r _ _ a)))).
 343
 344 notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))" with precedence 19
 345 for @{ 'Or_intro_r_ok_1 $a $ab }.
 346 interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab =
 347   (show ab (Or_intro_r _ _ a)).
 348
 349 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19
 350 for @{ 'Or_intro_r_ok_2 $a $ab }.
 351 interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab =
 352   (cast _ _ (show ab (Or_intro_r _ _ a))).
 353
 354 notation > "∨_'i_r' term 90 a" with precedence 19
 355 for @{ 'Or_intro_r (show $a ?) }.
 356 interpretation "Or_intro_r KO" 'Or_intro_r a = (cast _ (Or unit _) (Or_intro_r _ _ a)).
 357 interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r _ _ a).
 358
 359 (* ∨ elimination *)
 360 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
 361 for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }.
 362 interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc =
 363   (show c (cast _ _ (Or_elim _ _ _ (cast _ _ ab) (cast _ _ ac) (cast _ _ bc)))).
 364
 365 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
 366 for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 367 interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c =
 368   (cast _ _ (show c (cast _ _ (Or_elim _ _ _ (cast _ _ ab) (cast _ _ ac) (cast _ _ bc))))).
 369
 370 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
 371 for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 372 interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c =
 373   (show c (Or_elim _ _ _ ab ac bc)).
 374
 375 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
 376 for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 377 interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c =
 378   (cast _ _ (show c (Or_elim _ _ _ ab ac bc))).
 379
 380 definition unit_to ≝ λx:CProp.unit → x.
 381
 382 notation > "∨_'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19
 383 for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) }.
 384 interpretation "Or_elim KO" 'Or_elim ab ac bc =
 385   (cast _ _ (Or_elim _ _ _
 386     (cast (Or unit unit) _ ab)
 387     (cast (unit_to unit) (unit_to _) ac)
 388     (cast (unit_to unit) (unit_to _) bc))).
 389 interpretation "Or_elim OK" 'Or_elim ab ac bc = (Or_elim _ _ _ ab ac bc).
 390
 391 (* ⊤ introduction *)
 392 notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19
 393 for @{'Top_intro_ko_1}.
 394 interpretation "Top_intro_ko_1" 'Top_intro_ko_1 =
 395   (show _ (cast _ _ Top_intro)).
 396
 397 notation < "\infrule \nbsp mstyle color #ff0000 (⊤) mstyle color #ff0000 (⊤\sub\i)" with precedence 19
 398 for @{'Top_intro_ko_2}.
 399 interpretation "Top_intro_ko_2" 'Top_intro_ko_2 =
 400   (cast _ _ (show _ (cast _ _ Top_intro))).
 401
 402 notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19
 403 for @{'Top_intro_ok_1}.
 404 interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show _ Top_intro).
 405
 406 notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19
 407 for @{'Top_intro_ok_2 }.
 408 interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast _ _ (show _ Top_intro)).
 409
 410 notation > "⊤_'i'" with precedence 19 for @{ 'Top_intro }.
 411 interpretation "Top_intro KO" 'Top_intro = (cast _ _ Top_intro).
 412 interpretation "Top_intro OK" 'Top_intro = Top_intro.
 413
 414 (* ⊥ introduction *)
 415 notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19
 416 for @{'Bot_elim_ko_1 $a $b}.
 417 interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b =
 418   (show a (Bot_elim _ (cast _ _ b))).
 419
 420 notation < "\infrule b mstyle color #ff0000 (a) mstyle color #ff0000 (⊥\sub\e)" with precedence 19
 421 for @{'Bot_elim_ko_2 $a $b}.
 422 interpretation "Bot_elim_ko_2" 'Bot_elim_ko_2 a b =
 423   (cast _ _ (show a (Bot_elim _ (cast _ _ b)))).
 424
 425 notation < "\infrule b a (⊥\sub\e)" with precedence 19
 426 for @{'Bot_elim_ok_1 $a $b}.
 427 interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b =
 428   (show a (Bot_elim _ b)).
 429
 430 notation < "\infrule b mstyle color #ff0000 (a) (⊥\sub\e)" with precedence 19
 431 for @{'Bot_elim_ok_2 $a $b}.
 432 interpretation "Bot_elim_ok_2" 'Bot_elim_ok_2 a b =
 433   (cast _ _ (show a (Bot_elim _ b))).
 434
 435 notation > "⊥_'e' term 90 b" with precedence 19
 436 for @{ 'Bot_elim (show $b ?) }.
 437 interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim _ (cast _ _ a)).
 438 interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim _ a).
 439
 440 (* ¬ introduction *)
 441 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub\i) \emsp ident H)" with precedence 19
 442 for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
 443 interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b =
 444   (show ab (cast _ _ (Not_intro _ (cast _ _ b)))).
 445
 446 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub\i) \emsp ident H)" with precedence 19
 447 for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
 448 interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b =
 449   (cast _ _ (show ab (cast _ _ (Not_intro _ (cast _ _ b))))).
 450
 451 notation < "\infrule hbox(\emsp b \emsp) ab (\lnot\sub\i \emsp ident H) " with precedence 19
 452 for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
 453 interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b =
 454   (show ab (Not_intro _ b)).
 455
 456 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub\i \emsp ident H) " with precedence 19
 457 for @{ 'Not_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
 458 interpretation "Not_intro_ok_2" 'Not_intro_ok_2 ab \eta.b =
 459   (cast _ _ (show ab (Not_intro _ b))).
 460
 461 notation > "¬_'i' [ident H] term 90 b" with precedence 19
 462 for @{ 'Not_intro (λ${ident H}.show $b ?) }.
 463 interpretation "Not_intro KO" 'Not_intro a = (cast _ _ (Not_intro _ (cast _ _ a))).
 464 interpretation "Not_intro OK" 'Not_intro a = (Not_intro _ a).
 465
 466 (* ¬ elimination *)
 467 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19
 468 for @{ 'Not_elim_ko_1 $ab $a $b }.
 469 interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b =
 470   (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a)))).
 471
 472 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19
 473 for @{ 'Not_elim_ko_2 $ab $a $b }.
 474 interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b =
 475   (cast _ _ (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a))))).
 476
 477 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) " with precedence 19
 478 for @{ 'Not_elim_ok_1 $ab $a $b }.
 479 interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b =
 480   (show b (Not_elim _ ab a)).
 481
 482 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub(\emsp\e)) " with precedence 19
 483 for @{ 'Not_elim_ok_2 $ab $a $b }.
 484 interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b =
 485   (cast _ _ (show b (Not_elim _ ab a))).
 486
 487 notation > "¬_'e' term 90 ab term 90 a" with precedence 19
 488 for @{ 'Not_elim (show $ab ?) (show $a ?) }.
 489 interpretation "Not_elim KO" 'Not_elim ab a =
 490   (cast _ _ (Not_elim unit (cast _ _ ab) (cast _ _ a))).
 491 interpretation "Not_elim OK" 'Not_elim ab a =
 492   (Not_elim _ ab a).
 493
 494 (* RAA *)
 495 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
 496 for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
 497 interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn =
 498   (show Pn (cast _ _ (Raa _ (cast _ _ Px)))).
 499
 500 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
 501 for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
 502 interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn =
 503   (cast _ _ (show Pn (cast _ _ (Raa _ (cast _ _ Px))))).
 504
 505 notation < "\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)" with precedence 19
 506 for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
 507 interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn =
 508   (show Pn (Raa _ Px)).
 509
 510 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (\RAA \emsp ident x)" with precedence 19
 511 for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
 512 interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn =
 513   (cast _ _ (show Pn (Raa _ Px))).
 514
 515 notation > "'RAA' [ident H] term 90 b" with precedence 19
 516 for @{ 'Raa (λ${ident H}.show $b ?) }.
 517 interpretation "RAA KO" 'Raa p = (cast _ unit (Raa _ (cast _ (unit_to _) p))).
 518 interpretation "RAA OK" 'Raa p = (Raa _ p).
 519
 520 (*DOCBEGIN
 521 Templates for rules:
 522
 523         apply rule (⇒_i […] (…)).
 524
 525         apply rule (∧_i (…) (…));
 526                 [
 527                 |
 528                 ]
 529
 530         apply rule (∨_i_l (…)).
 531
 532         apply rule (∨_i_r (…)).
 533
 534         apply rule (¬_i […] (…)).
 535
 536         apply rule (⊤_i).
 537
 538         apply rule (⇒_e (…) (…));
 539                 [
 540                 |
 541                 ]
 542
 543         apply rule (∧_e_l (…)).
 544
 545         apply rule (∧_e_r (…)).
 546
 547         apply rule (∨_e (…) […] (…) […] (…));
 548                 [
 549                 |
 550                 |
 551                 ]
 552
 553         apply rule (¬_e (…) (…));
 554                 [
 555                 |
 556                 ]
 557
 558         apply rule (⊥_e (…)).
 559
 560         apply rule (prove (…)).
 561
 562         apply rule (RAA […] (…)).
 563
 564         apply rule (discharge […]).
 565
 566 DOCEND*)
 567
 568
 569
 570