3 inductive Imply (A,B:CProp) : CProp ≝
4 | Imply_intro: (A → B) → Imply A B.
6 definition Imply_elim ≝ λA,B.λf:Imply A B. λa:A.
7 match f with [ Imply_intro g ⇒ g a].
9 inductive And (A,B:CProp) : CProp ≝
10 | And_intro: A → B → And A B.
12 definition And_elim_l ≝ λA,B.λc:And A B.
13 match c with [ And_intro a b ⇒ a ].
15 definition And_elim_r ≝ λA,B.λc:And A B.
16 match c with [ And_intro a b ⇒ b ].
18 inductive Or (A,B:CProp) : CProp ≝
19 | Or_intro_l: A → Or A B
20 | Or_intro_r: B → Or A B.
22 definition Or_elim ≝ λA,B,C:CProp.λc:Or A B.λfa: A → C.λfb: B → C.
25 | Or_intro_r b ⇒ fb b].
27 inductive Top : CProp :=
30 inductive Bot : CProp := .
32 definition Bot_elim ≝ λP:CProp.λx:Bot.
33 match x in Bot return λx.P with [].
35 definition Not := λA:CProp.Imply A Bot.
37 definition Not_intro : ∀A.(A → Bot) → Not A ≝ λA.
40 definition Not_elim : ∀A.Not A → A → Bot ≝ λA.
43 definition Discharge := λA:CProp.λa:A.
46 axiom Raa : ∀A.(Not A → Bot) → A.
48 (* Dummy proposition *)
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.
93 (* Every formula user provided annotates its proof:
94 `A` becomes `(show A ?)` *)
95 definition show : ∀A.A→A ≝ λA:CProp.λa:A.a.
97 (* When something does not fit, this daemon is used *)
98 axiom cast: ∀A,B:CProp.B → A.
100 (* begin a proof: draws the root *)
101 notation > "'prove' p" non associative with precedence 19
103 interpretation "prove KO" 'prove p = (cast _ _ (show p _)).
104 interpretation "prove OK" 'prove p = (show p _).
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)).
114 (* already proved lemma *)
115 definition Lemma : ∀A.A→A ≝ λA:CProp.λa:A.a.
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))).
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)))).
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 _ _)).
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 _ _))).
145 notation > "'lem' term 90 p" non associative with precedence 19
147 interpretation "lemma KO" 'Lemma p = (cast _ _ (Lemma _ p)).
148 interpretation "lemma OK" 'Lemma p = (Lemma _ p).
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)))).
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))).
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).
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))).
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)))).
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)).
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))).
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).
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)))).
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))))).
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)).
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))).
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).
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))).
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)))).
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)).
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))).
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).
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)))).
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))))).
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)).
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))).
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).
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)))).
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))))).
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)).
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))).
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).
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))).
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)))).
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)).
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))).
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).
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))).
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)))).
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)).
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))).
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).
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)))).
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))))).
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)).
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))).
380 definition unit_to ≝ λx:CProp.unit → x.
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).
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)).
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))).
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).
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)).
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.
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))).
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)))).
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)).
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))).
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).
441 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub(\emsp\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)))).
446 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub(\emsp\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))))).
451 notation < "\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\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)).
456 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub(\emsp\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))).
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).
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)))).
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))))).
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)).
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))).
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 =
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)))).
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))))).
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)).
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))).
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).
523 apply rule (⇒_i […] (…)).
525 apply rule (∧_i (…) (…));
530 apply rule (∨_i_l (…)).
532 apply rule (∨_i_r (…)).
534 apply rule (¬_i […] (…)).
538 apply rule (⇒_e (…) (…));
543 apply rule (∧_e_l (…)).
545 apply rule (∧_e_r (…)).
547 apply rule (∨_e (…) […] (…) […] (…));
553 apply rule (¬_e (…) (…));
558 apply rule (⊥_e (…)).
560 apply rule (prove (…)).
562 apply rule (RAA […] (…)).
564 apply rule (discharge […]).