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 axiom sort : Type.
  49
  50 inductive Exists (A:Type) (P:A→CProp) : CProp ≝
  51   Exists_intro: ∀w:A. P w → Exists A P.
  52
  53 definition Exists_elim ≝
  54   λA:Type.λP:A→CProp.λC:CProp.λc:Exists A P.λH:(Πx.P x → C).
  55    match c with [ Exists_intro w p ⇒ H w p ].
  56
  57 inductive Forall (A:Type) (P:A→CProp) : CProp ≝
  58  Forall_intro: (∀n:A. P n) → Forall A P.
  59
  60 definition Forall_elim ≝
  61  λA:Type.λP:A→CProp.λn:A.λf:Forall A P.match f with [ Forall_intro g ⇒ g n ].
  62
  63 (* Dummy proposition *)
  64 axiom unit : CProp.
  65
  66 (* Notations *)
  67 notation "hbox(a break ⇒ b)" right associative with precedence 20
  68 for @{ 'Imply $a $b }.
  69 interpretation "Imply" 'Imply a b = (Imply a b).
  70 interpretation "constructive or" 'or x y = (Or x y).
  71 interpretation "constructive and" 'and x y = (And x y).
  72 notation "⊤" non associative with precedence 90 for @{'Top}.
  73 interpretation "Top" 'Top = Top.
  74 notation "⊥" non associative with precedence 90 for @{'Bot}.
  75 interpretation "Bot" 'Bot = Bot.
  76 interpretation "Not" 'not a = (Not a).
  77 notation "✶" non associative with precedence 90 for @{'unit}.
  78 interpretation "dummy prop" 'unit = unit.
  79 notation > "\exists list1 ident x sep , . term 19 Px" with precedence 20
  80 for ${ fold right @{$Px} rec acc @{'myexists (λ${ident x}.$acc)} }.
  81 notation < "hvbox(\exists ident i break . p)" with precedence 20
  82 for @{ 'myexists (\lambda ${ident i} : $ty. $p) }.
  83 interpretation "constructive ex" 'myexists \eta.x = (Exists sort x).
  84 notation > "\forall ident x.break term 19 Px" with precedence 20
  85 for @{ 'Forall (λ${ident x}.$Px) }.
  86 notation < "\forall ident x.break term 19 Px" with precedence 20
  87 for @{ 'Forall (λ${ident x}:$tx.$Px) }.
  88 interpretation "Forall" 'Forall \eta.Px = (Forall _ Px).
  89
  90 (* Variables *)
  91 axiom A : CProp.
  92 axiom B : CProp.
  93 axiom C : CProp.
  94 axiom D : CProp.
  95 axiom E : CProp.
  96 axiom F : CProp.
  97 axiom G : CProp.
  98 axiom H : CProp.
  99 axiom I : CProp.
 100 axiom J : CProp.
 101 axiom K : CProp.
 102 axiom L : CProp.
 103 axiom M : CProp.
 104 axiom N : CProp.
 105 axiom O : CProp.
 106 axiom P : sort →CProp.
 107 axiom Q : sort →CProp.
 108 axiom R : sort →sort →CProp.
 109 axiom S : sort →sort →CProp.
 110 axiom f : sort → sort.
 111 axiom g : sort → sort.
 112 axiom h : sort → sort → sort.
 113
 114 (* Every formula user provided annotates its proof:
 115    `A` becomes `(show A ?)` *)
 116 definition show : ΠA.A→A ≝ λA:CProp.λa:A.a.
 117
 118 (* When something does not fit, this daemon is used *)
 119 axiom cast: ΠA,B:CProp.B → A.
 120
 121 (* begin a proof: draws the root *)
 122 notation > "'prove' p" non associative with precedence 19
 123 for @{ 'prove $p }.
 124 interpretation "prove KO" 'prove p = (cast _ _ (show p _)).
 125 interpretation "prove OK" 'prove p = (show p _).
 126
 127 (* Leaves *)
 128 notation < "\infrule (t\atop ⋮) a ?" with precedence 19
 129 for @{ 'leaf_ok $a $t }.
 130 interpretation "leaf OK" 'leaf_ok a t = (show a t).
 131 notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19
 132 for @{ 'leaf_ko $a $t }.
 133 interpretation "leaf KO" 'leaf_ko a t = (cast _ _ (show a t)).
 134
 135 (* already proved lemma *)
 136 definition Lemma : ΠA.A→A ≝ λA:CProp.λa:A.a.
 137
 138 notation < "\infrule \nbsp p mstyle color #ff0000 (\lem\emsp H)" non associative with precedence 19
 139 for @{ 'lemma_ko_1 $p $H }.
 140 interpretation "lemma_ko_1" 'lemma_ko_1 p H =
 141   (show p (cast _ _ (Lemma _ H))).
 142
 143 notation < "\infrule \nbsp mstyle color #ff0000 (p) mstyle color #ff0000 (\lem\emsp H)" non associative with precedence 19
 144 for @{ 'lemma_ko_2 $p $H }.
 145 interpretation "lemma_ko_2" 'lemma_ko_2 p H =
 146   (cast _ _ (show p (cast _ _ (Lemma _ H)))).
 147
 148 notation < "\infrule \nbsp p (\lem\emsp H)" non associative with precedence 19
 149 for @{ 'lemma_ok_1 $p $H }.
 150 interpretation "lemma_ok_1" 'lemma_ok_1 p H =
 151   (show p (Lemma _ H)).
 152 interpretation "lemma_ok_11" 'lemma_ok_1 p H =
 153   (show p (Lemma _ H _)).
 154 interpretation "lemma_ok_111" 'lemma_ok_1 p H =
 155   (show p (Lemma _ H _ _)).
 156
 157 notation < "\infrule \nbsp mstyle color #ff0000 (p) (\lem\emsp H)" non associative with precedence 19
 158 for @{ 'lemma_ok_2 $p $H }.
 159 interpretation "lemma_ok_2" 'lemma_ok_2 p H =
 160   (cast _ _ (show p (Lemma _ H))).
 161 interpretation "lemma_ok_22" 'lemma_ok_2 p H =
 162   (cast _ _ (show p (Lemma _ H _))).
 163 interpretation "lemma_ok_22" 'lemma_ok_2 p H =
 164   (cast _ _ (show p (Lemma _ H _ _))).
 165
 166 notation > "'lem' term 90 p" non associative with precedence 19
 167 for @{ 'Lemma $p  }.
 168 interpretation "lemma KO" 'Lemma p = (cast _ _ (Lemma _ p)).
 169 interpretation "lemma OK" 'Lemma p = (Lemma _ p).
 170
 171
 172 (* discharging *)
 173 notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19
 174 for @{ 'discharge_ko_1 $a $H }.
 175 interpretation "discharge_ko_1" 'discharge_ko_1 a H =
 176   (show a (cast _ _ (Discharge _ H))).
 177 notation < "[ mstyle color #ff0000 (a) ] \sup mstyle color #ff0000 (H)" with precedence 19
 178 for @{ 'discharge_ko_2 $a $H }.
 179 interpretation "discharge_ko_2" 'discharge_ko_2 a H =
 180   (cast _ _ (show a (cast _ _ (Discharge _ H)))).
 181
 182 notation < "[ a ] \sup H" with precedence 19
 183 for @{ 'discharge_ok_1 $a $H }.
 184 interpretation "discharge_ok_1" 'discharge_ok_1 a H =
 185   (show a (Discharge _ H)).
 186 notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19
 187 for @{ 'discharge_ok_2 $a $H }.
 188 interpretation "discharge_ok_2" 'discharge_ok_2 a H =
 189   (cast _ _ (show a (Discharge _ H))).
 190
 191 notation > "'discharge' [H]" with precedence 19
 192 for @{ 'discharge $H }.
 193 interpretation "discharge KO" 'discharge H = (cast _ _ (Discharge _ H)).
 194 interpretation "discharge OK" 'discharge H = (Discharge _ H).
 195
 196 (* ⇒ introduction *)
 197 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
 198 for @{ 'Imply_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
 199 interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b =
 200   (show ab (cast _ _ (Imply_intro _ _ b))).
 201
 202 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
 203 for @{ 'Imply_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
 204 interpretation "Imply_intro_ko_2" 'Imply_intro_ko_2 ab \eta.b =
 205   (cast _ _ (show ab (cast _ _ (Imply_intro _ _ b)))).
 206
 207 notation < "\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) " with precedence 19
 208 for @{ 'Imply_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
 209 interpretation "Imply_intro_ok_1" 'Imply_intro_ok_1 ab \eta.b =
 210   (show ab (Imply_intro _ _ b)).
 211
 212 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (⇒\sub\i \emsp ident H) " with precedence 19
 213 for @{ 'Imply_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
 214 interpretation "Imply_intro_ok_2" 'Imply_intro_ok_2 ab \eta.b =
 215   (cast _ _ (show ab (Imply_intro _ _ b))).
 216
 217 notation > "⇒_'i' [ident H] term 90 b" with precedence 19
 218 for @{ 'Imply_intro $b (λ${ident H}.show $b ?) }.
 219 interpretation "Imply_intro KO" 'Imply_intro b pb =
 220   (cast _ (Imply unit b) (Imply_intro _ b pb)).
 221 interpretation "Imply_intro OK" 'Imply_intro b pb =
 222   (Imply_intro _ b pb).
 223
 224 (* ⇒ elimination *)
 225 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19
 226 for @{ 'Imply_elim_ko_1 $ab $a $b }.
 227 interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b =
 228   (show b (cast _ _ (Imply_elim _ _ (cast _ _ ab) (cast _ _ a)))).
 229
 230 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19
 231 for @{ 'Imply_elim_ko_2 $ab $a $b }.
 232 interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b =
 233   (cast _ _ (show b (cast _ _ (Imply_elim _ _ (cast _ _ ab) (cast _ _ a))))).
 234
 235 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) " with precedence 19
 236 for @{ 'Imply_elim_ok_1 $ab $a $b }.
 237 interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b =
 238   (show b (Imply_elim _ _ ab a)).
 239
 240 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (⇒\sub\e) " with precedence 19
 241 for @{ 'Imply_elim_ok_2 $ab $a $b }.
 242 interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b =
 243   (cast _ _ (show b (Imply_elim _ _ ab a))).
 244
 245 notation > "⇒_'e' term 90 ab term 90 a" with precedence 19
 246 for @{ 'Imply_elim (show $ab ?) (show $a ?) }.
 247 interpretation "Imply_elim KO" 'Imply_elim ab a =
 248   (cast _ _ (Imply_elim _ _ (cast (Imply unit unit) _ ab) (cast unit _ a))).
 249 interpretation "Imply_elim OK" 'Imply_elim ab a =
 250   (Imply_elim _ _ ab a).
 251
 252 (* ∧ introduction *)
 253 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19
 254 for @{ 'And_intro_ko_1 $a $b $ab }.
 255 interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab =
 256   (show ab (cast _ _ (And_intro _ _ a b))).
 257
 258 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19
 259 for @{ 'And_intro_ko_2 $a $b $ab }.
 260 interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab =
 261   (cast _ _ (show ab (cast _ _ (And_intro _ _ a b)))).
 262
 263 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)" with precedence 19
 264 for @{ 'And_intro_ok_1 $a $b $ab }.
 265 interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab =
 266   (show ab (And_intro _ _ a b)).
 267
 268 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) (∧\sub\i)" with precedence 19
 269 for @{ 'And_intro_ok_2 $a $b $ab }.
 270 interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab =
 271   (cast _ _ (show ab (And_intro _ _ a b))).
 272
 273 notation > "∧_'i' term 90 a term 90 b" with precedence 19
 274 for @{ 'And_intro (show $a ?) (show $b ?) }.
 275 interpretation "And_intro KO" 'And_intro a b = (cast _ _ (And_intro _ _ a b)).
 276 interpretation "And_intro OK" 'And_intro a b = (And_intro _ _ a b).
 277
 278 (* ∧ elimination *)
 279 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
 280 for @{ 'And_elim_l_ko_1 $ab $a }.
 281 interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a =
 282   (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab)))).
 283
 284 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
 285 for @{ 'And_elim_l_ko_2 $ab $a }.
 286 interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a =
 287   (cast _ _ (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab))))).
 288
 289 notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))" with precedence 19
 290 for @{ 'And_elim_l_ok_1 $ab $a }.
 291 interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a =
 292   (show a (And_elim_l _ _ ab)).
 293
 294 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\l))" with precedence 19
 295 for @{ 'And_elim_l_ok_2 $ab $a }.
 296 interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a =
 297   (cast _ _ (show a (And_elim_l _ _ ab))).
 298
 299 notation > "∧_'e_l' term 90 ab" with precedence 19
 300 for @{ 'And_elim_l (show $ab ?) }.
 301 interpretation "And_elim_l KO" 'And_elim_l a = (cast _ _ (And_elim_l _ _ (cast (And unit unit) _ a))).
 302 interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l _ _ a).
 303
 304 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
 305 for @{ 'And_elim_r_ko_1 $ab $a }.
 306 interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a =
 307   (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab)))).
 308
 309 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
 310 for @{ 'And_elim_r_ko_2 $ab $a }.
 311 interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a =
 312   (cast _ _ (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab))))).
 313
 314 notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))" with precedence 19
 315 for @{ 'And_elim_r_ok_1 $ab $a }.
 316 interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a =
 317   (show a (And_elim_r _ _ ab)).
 318
 319 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\r))" with precedence 19
 320 for @{ 'And_elim_r_ok_2 $ab $a }.
 321 interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a =
 322   (cast _ _ (show a (And_elim_r _ _ ab))).
 323
 324 notation > "∧_'e_r' term 90 ab" with precedence 19
 325 for @{ 'And_elim_r (show $ab ?) }.
 326 interpretation "And_elim_r KO" 'And_elim_r a = (cast _ _ (And_elim_r _ _ (cast (And unit unit) _ a))).
 327 interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r _ _ a).
 328
 329 (* ∨ introduction *)
 330 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
 331 for @{ 'Or_intro_l_ko_1 $a $ab }.
 332 interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab =
 333   (show ab (cast _ _ (Or_intro_l _ _ a))).
 334
 335 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
 336 for @{ 'Or_intro_l_ko_2 $a $ab }.
 337 interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab =
 338   (cast _ _ (show ab (cast _ _ (Or_intro_l _ _ a)))).
 339
 340 notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))" with precedence 19
 341 for @{ 'Or_intro_l_ok_1 $a $ab }.
 342 interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab =
 343   (show ab (Or_intro_l _ _ a)).
 344
 345 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19
 346 for @{ 'Or_intro_l_ok_2 $a $ab }.
 347 interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab =
 348   (cast _ _ (show ab (Or_intro_l _ _ a))).
 349
 350 notation > "∨_'i_l' term 90 a" with precedence 19
 351 for @{ 'Or_intro_l (show $a ?) }.
 352 interpretation "Or_intro_l KO" 'Or_intro_l a = (cast _ (Or _ unit) (Or_intro_l _ _ a)).
 353 interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l _ _ a).
 354
 355 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
 356 for @{ 'Or_intro_r_ko_1 $a $ab }.
 357 interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab =
 358   (show ab (cast _ _ (Or_intro_r _ _ a))).
 359
 360 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
 361 for @{ 'Or_intro_r_ko_2 $a $ab }.
 362 interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab =
 363   (cast _ _ (show ab (cast _ _ (Or_intro_r _ _ a)))).
 364
 365 notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))" with precedence 19
 366 for @{ 'Or_intro_r_ok_1 $a $ab }.
 367 interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab =
 368   (show ab (Or_intro_r _ _ a)).
 369
 370 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19
 371 for @{ 'Or_intro_r_ok_2 $a $ab }.
 372 interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab =
 373   (cast _ _ (show ab (Or_intro_r _ _ a))).
 374
 375 notation > "∨_'i_r' term 90 a" with precedence 19
 376 for @{ 'Or_intro_r (show $a ?) }.
 377 interpretation "Or_intro_r KO" 'Or_intro_r a = (cast _ (Or unit _) (Or_intro_r _ _ a)).
 378 interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r _ _ a).
 379
 380 (* ∨ elimination *)
 381 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
 382 for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }.
 383 interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc =
 384   (show c (cast _ _ (Or_elim _ _ _ (cast _ _ ab) (cast _ _ ac) (cast _ _ bc)))).
 385
 386 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
 387 for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 388 interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c =
 389   (cast _ _ (show c (cast _ _ (Or_elim _ _ _ (cast _ _ ab) (cast _ _ ac) (cast _ _ bc))))).
 390
 391 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
 392 for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 393 interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c =
 394   (show c (Or_elim _ _ _ ab ac bc)).
 395
 396 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
 397 for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 398 interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c =
 399   (cast _ _ (show c (Or_elim _ _ _ ab ac bc))).
 400
 401 definition unit_to ≝ λx:CProp.unit → x.
 402
 403 notation > "∨_'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19
 404 for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) }.
 405 interpretation "Or_elim KO" 'Or_elim ab ac bc =
 406   (cast _ _ (Or_elim _ _ _
 407     (cast (Or unit unit) _ ab)
 408     (cast (unit_to unit) (unit_to _) ac)
 409     (cast (unit_to unit) (unit_to _) bc))).
 410 interpretation "Or_elim OK" 'Or_elim ab ac bc = (Or_elim _ _ _ ab ac bc).
 411
 412 (* ⊤ introduction *)
 413 notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19
 414 for @{'Top_intro_ko_1}.
 415 interpretation "Top_intro_ko_1" 'Top_intro_ko_1 =
 416   (show _ (cast _ _ Top_intro)).
 417
 418 notation < "\infrule \nbsp mstyle color #ff0000 (⊤) mstyle color #ff0000 (⊤\sub\i)" with precedence 19
 419 for @{'Top_intro_ko_2}.
 420 interpretation "Top_intro_ko_2" 'Top_intro_ko_2 =
 421   (cast _ _ (show _ (cast _ _ Top_intro))).
 422
 423 notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19
 424 for @{'Top_intro_ok_1}.
 425 interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show _ Top_intro).
 426
 427 notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19
 428 for @{'Top_intro_ok_2 }.
 429 interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast _ _ (show _ Top_intro)).
 430
 431 notation > "⊤_'i'" with precedence 19 for @{ 'Top_intro }.
 432 interpretation "Top_intro KO" 'Top_intro = (cast _ _ Top_intro).
 433 interpretation "Top_intro OK" 'Top_intro = Top_intro.
 434
 435 (* ⊥ introduction *)
 436 notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19
 437 for @{'Bot_elim_ko_1 $a $b}.
 438 interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b =
 439   (show a (Bot_elim _ (cast _ _ b))).
 440
 441 notation < "\infrule b mstyle color #ff0000 (a) mstyle color #ff0000 (⊥\sub\e)" with precedence 19
 442 for @{'Bot_elim_ko_2 $a $b}.
 443 interpretation "Bot_elim_ko_2" 'Bot_elim_ko_2 a b =
 444   (cast _ _ (show a (Bot_elim _ (cast _ _ b)))).
 445
 446 notation < "\infrule b a (⊥\sub\e)" with precedence 19
 447 for @{'Bot_elim_ok_1 $a $b}.
 448 interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b =
 449   (show a (Bot_elim _ b)).
 450
 451 notation < "\infrule b mstyle color #ff0000 (a) (⊥\sub\e)" with precedence 19
 452 for @{'Bot_elim_ok_2 $a $b}.
 453 interpretation "Bot_elim_ok_2" 'Bot_elim_ok_2 a b =
 454   (cast _ _ (show a (Bot_elim _ b))).
 455
 456 notation > "⊥_'e' term 90 b" with precedence 19
 457 for @{ 'Bot_elim (show $b ?) }.
 458 interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim _ (cast _ _ a)).
 459 interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim _ a).
 460
 461 (* ¬ introduction *)
 462 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
 463 for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
 464 interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b =
 465   (show ab (cast _ _ (Not_intro _ (cast _ _ b)))).
 466
 467 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
 468 for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
 469 interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b =
 470   (cast _ _ (show ab (cast _ _ (Not_intro _ (cast _ _ b))))).
 471
 472 notation < "\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) " with precedence 19
 473 for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
 474 interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b =
 475   (show ab (Not_intro _ b)).
 476
 477 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub(\emsp\i) \emsp ident H) " with precedence 19
 478 for @{ 'Not_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
 479 interpretation "Not_intro_ok_2" 'Not_intro_ok_2 ab \eta.b =
 480   (cast _ _ (show ab (Not_intro _ b))).
 481
 482 notation > "¬_'i' [ident H] term 90 b" with precedence 19
 483 for @{ 'Not_intro (λ${ident H}.show $b ?) }.
 484 interpretation "Not_intro KO" 'Not_intro a = (cast _ _ (Not_intro _ (cast _ _ a))).
 485 interpretation "Not_intro OK" 'Not_intro a = (Not_intro _ a).
 486
 487 (* ¬ elimination *)
 488 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19
 489 for @{ 'Not_elim_ko_1 $ab $a $b }.
 490 interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b =
 491   (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a)))).
 492
 493 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19
 494 for @{ 'Not_elim_ko_2 $ab $a $b }.
 495 interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b =
 496   (cast _ _ (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a))))).
 497
 498 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) " with precedence 19
 499 for @{ 'Not_elim_ok_1 $ab $a $b }.
 500 interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b =
 501   (show b (Not_elim _ ab a)).
 502
 503 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub(\emsp\e)) " with precedence 19
 504 for @{ 'Not_elim_ok_2 $ab $a $b }.
 505 interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b =
 506   (cast _ _ (show b (Not_elim _ ab a))).
 507
 508 notation > "¬_'e' term 90 ab term 90 a" with precedence 19
 509 for @{ 'Not_elim (show $ab ?) (show $a ?) }.
 510 interpretation "Not_elim KO" 'Not_elim ab a =
 511   (cast _ _ (Not_elim unit (cast _ _ ab) (cast _ _ a))).
 512 interpretation "Not_elim OK" 'Not_elim ab a =
 513   (Not_elim _ ab a).
 514
 515 (* RAA *)
 516 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
 517 for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
 518 interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn =
 519   (show Pn (cast _ _ (Raa _ (cast _ _ Px)))).
 520
 521 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
 522 for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
 523 interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn =
 524   (cast _ _ (show Pn (cast _ _ (Raa _ (cast _ _ Px))))).
 525
 526 notation < "\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)" with precedence 19
 527 for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
 528 interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn =
 529   (show Pn (Raa _ Px)).
 530
 531 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (\RAA \emsp ident x)" with precedence 19
 532 for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
 533 interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn =
 534   (cast _ _ (show Pn (Raa _ Px))).
 535
 536 notation > "'RAA' [ident H] term 90 b" with precedence 19
 537 for @{ 'Raa (λ${ident H}.show $b ?) }.
 538 interpretation "RAA KO" 'Raa p = (cast _ unit (Raa _ (cast _ (unit_to _) p))).
 539 interpretation "RAA OK" 'Raa p = (Raa _ p).
 540
 541 (* ∃ introduction *)
 542 notation < "\infrule hbox(\emsp Pn \emsp) Px mstyle color #ff0000 (∃\sub\i)" with precedence 19
 543 for @{ 'Exists_intro_ko_1 $Pn $Px }.
 544 interpretation "Exists_intro_ko_1" 'Exists_intro_ko_1 Pn Px =
 545   (show Px (cast _ _ (Exists_intro _ _ _ (cast _ _ Pn)))).
 546
 547 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) mstyle color #ff0000 (∃\sub\i)" with precedence 19
 548 for @{ 'Exists_intro_ko_2 $Pn $Px }.
 549 interpretation "Exists_intro_ko_2" 'Exists_intro_ko_2 Pn Px =
 550   (cast _ _ (show Px (cast _ _ (Exists_intro _ _ _ (cast _ _ Pn))))).
 551
 552 notation < "\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)" with precedence 19
 553 for @{ 'Exists_intro_ok_1 $Pn $Px }.
 554 interpretation "Exists_intro_ok_1" 'Exists_intro_ok_1 Pn Px =
 555   (show Px (Exists_intro _ _ _ Pn)).
 556
 557 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) (∃\sub\i)" with precedence 19
 558 for @{ 'Exists_intro_ok_2 $Pn $Px }.
 559 interpretation "Exists_intro_ok_2" 'Exists_intro_ok_2 Pn Px =
 560   (cast _ _ (show Px (Exists_intro _ _ _ Pn))).
 561
 562 notation >"∃_'i' {term 90 t} term 90 Pt" non associative with precedence 19
 563 for @{'Exists_intro $t (λ_.?) (show $Pt ?)}.
 564 interpretation "Exists_intro KO" 'Exists_intro t P Pt =
 565  (cast _ _ (Exists_intro sort P t (cast _ _ Pt))).
 566 interpretation "Exists_intro OK" 'Exists_intro t P Pt =
 567  (Exists_intro sort P t Pt).
 568
 569 (* ∃ elimination *)
 570 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
 571 for @{ 'Exists_elim_ko_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 572 interpretation "Exists_elim_ko_1" 'Exists_elim_ko_1 ExPx Pc c =
 573     (show c (cast _ _ (Exists_elim _ _ _ (cast _ _ ExPx) (cast _ _ Pc)))).
 574
 575 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
 576 for @{ 'Exists_elim_ko_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 577 interpretation "Exists_elim_ko_2" 'Exists_elim_ko_2 ExPx Pc c =
 578     (cast _ _ (show c (cast _ _ (Exists_elim _ _ _ (cast _ _ ExPx) (cast _ _ Pc))))).
 579
 580 notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)" with precedence 19
 581 for @{ 'Exists_elim_ok_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 582 interpretation "Exists_elim_ok_1" 'Exists_elim_ok_1 ExPx Pc c =
 583     (show c (Exists_elim _ _ _ ExPx Pc)).
 584
 585 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
 586 for @{ 'Exists_elim_ok_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 587 interpretation "Exists_elim_ok_2" 'Exists_elim_ok_2 ExPx Pc c =
 588     (cast _ _ (show c (Exists_elim _ _ _ ExPx Pc))).
 589
 590 definition ex_concl := λx:CProp.sort → unit → x.
 591 definition fake_pred := λx:sort.unit.
 592
 593 notation >"∃_'e' term 90 ExPt {ident t} [ident H] term 90 c" non associative with precedence 19
 594 for @{'Exists_elim (λ_.?) (show $ExPt ?) (λ${ident t}:sort.λ${ident H}.show $c ?)}.
 595 interpretation "Exists_elim KO" 'Exists_elim P ExPt c =
 596  (cast _ _ (Exists_elim sort P _
 597    (cast (Exists _ P)  _ ExPt) (cast (ex_concl unit) (ex_concl _) c))).
 598 interpretation "Exists_elim OK" 'Exists_elim P ExPt c =
 599  (Exists_elim sort P _ ExPt c).
 600
 601 (* ∀ introduction *)
 602
 603 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
 604 for @{ 'Forall_intro_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
 605 interpretation "Forall_intro_ko_1" 'Forall_intro_ko_1 Px Pn =
 606   (show Pn (cast _ _ (Forall_intro _ _ (cast _ _ Px)))).
 607
 608 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
 609 for @{ 'Forall_intro_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
 610 interpretation "Forall_intro_ko_2" 'Forall_intro_ko_2 Px Pn =
 611   (cast _ _ (show Pn (cast _ _ (Forall_intro _ _ (cast _ _ Px))))).
 612
 613 notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)" with precedence 19
 614 for @{ 'Forall_intro_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
 615 interpretation "Forall_intro_ok_1" 'Forall_intro_ok_1 Px Pn =
 616   (show Pn (Forall_intro _ _ Px)).
 617
 618 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\i \emsp ident x)" with precedence 19
 619 for @{ 'Forall_intro_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
 620 interpretation "Forall_intro_ok_2" 'Forall_intro_ok_2 Px Pn =
 621   (cast _ _ (show Pn (Forall_intro _ _ Px))).
 622
 623 notation > "∀_'i' {ident y} term 90 Px" non associative with precedence 19
 624 for @{ 'Forall_intro (λ_.?) (λ${ident y}.show $Px ?) }.
 625 interpretation "Forall_intro KO" 'Forall_intro P Px =
 626   (cast _ _ (Forall_intro sort P (cast _ _ Px))).
 627 interpretation "Forall_intro OK" 'Forall_intro P Px =
 628   (Forall_intro sort P Px).
 629
 630 (* ∀ elimination *)
 631 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\e))" with precedence 19
 632 for @{ 'Forall_elim_ko_1 $Px $Pn }.
 633 interpretation "Forall_elim_ko_1" 'Forall_elim_ko_1 Px Pn =
 634   (show Pn (cast _ _ (Forall_elim _ _ _ (cast _ _ Px)))).
 635
 636 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\e))" with precedence 19
 637 for @{ 'Forall_elim_ko_2 $Px $Pn }.
 638 interpretation "Forall_elim_ko_2" 'Forall_elim_ko_2 Px Pn =
 639   (cast _ _ (show Pn (cast _ _ (Forall_elim _ _ _ (cast _ _ Px))))).
 640
 641 notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)" with precedence 19
 642 for @{ 'Forall_elim_ok_1 $Px $Pn }.
 643 interpretation "Forall_elim_ok_1" 'Forall_elim_ok_1 Px Pn =
 644   (show Pn (Forall_elim _ _ _ Px)).
 645
 646 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\e)" with precedence 19
 647 for @{ 'Forall_elim_ok_2 $Px $Pn }.
 648 interpretation "Forall_elim_ok_2" 'Forall_elim_ok_2 Px Pn =
 649   (cast _ _ (show Pn (Forall_elim _ _ _ Px))).
 650
 651 notation > "∀_'e' {term 90 t} term 90 Pn" non associative with precedence 19
 652 for @{ 'Forall_elim (λ_.?) $t (show $Pn ?) }.
 653 interpretation "Forall_elim KO" 'Forall_elim P t Px =
 654   (cast _ unit (Forall_elim sort P t (cast _ _ Px))).
 655 interpretation "Forall_elim OK" 'Forall_elim P t Px =
 656   (Forall_elim sort P t Px).