1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
17 inductive Imply (A,B:CProp) : CProp ≝
18 | Imply_intro: (A → B) → Imply A B.
20 definition Imply_elim ≝ λA,B.λf:Imply A B. λa:A.
21 match f with [ Imply_intro g ⇒ g a].
23 inductive And (A,B:CProp) : CProp ≝
24 | And_intro: A → B → And A B.
26 definition And_elim_l ≝ λA,B.λc:And A B.
27 match c with [ And_intro a b ⇒ a ].
29 definition And_elim_r ≝ λA,B.λc:And A B.
30 match c with [ And_intro a b ⇒ b ].
32 inductive Or (A,B:CProp) : CProp ≝
33 | Or_intro_l: A → Or A B
34 | Or_intro_r: B → Or A B.
36 definition Or_elim ≝ λA,B,C:CProp.λc:Or A B.λfa: A → C.λfb: B → C.
39 | Or_intro_r b ⇒ fb b].
41 inductive Top : CProp :=
44 inductive Bot : CProp := .
46 definition Bot_elim ≝ λP:CProp.λx:Bot.
47 match x in Bot return λx.P with [].
49 definition Not := λA:CProp.Imply A Bot.
51 definition Not_intro : ∀A.(A → Bot) → Not A ≝ λA.
54 definition Not_elim : ∀A.Not A → A → Bot ≝ λA.
57 definition Discharge := λA:CProp.λa:A.
60 axiom Raa : ∀A.(Not A → Bot) → A.
64 inductive Exists (A:Type) (P:A→CProp) : CProp ≝
65 Exists_intro: ∀w:A. P w → Exists A P.
67 definition Exists_elim ≝
68 λA:Type.λP:A→CProp.λC:CProp.λc:Exists A P.λH:(Πx.P x → C).
69 match c with [ Exists_intro w p ⇒ H w p ].
71 inductive Forall (A:Type) (P:A→CProp) : CProp ≝
72 Forall_intro: (∀n:A. P n) → Forall A P.
74 definition Forall_elim ≝
75 λA:Type.λP:A→CProp.λn:A.λf:Forall A P.match f with [ Forall_intro g ⇒ g n ].
77 (* Dummy proposition *)
81 notation "hbox(a break ⇒ b)" right associative with precedence 20
82 for @{ 'Imply $a $b }.
83 interpretation "Imply" 'Imply a b = (Imply a b).
84 interpretation "constructive or" 'or x y = (Or x y).
85 interpretation "constructive and" 'and x y = (And x y).
86 notation "⊤" non associative with precedence 90 for @{'Top}.
87 interpretation "Top" 'Top = Top.
88 notation "⊥" non associative with precedence 90 for @{'Bot}.
89 interpretation "Bot" 'Bot = Bot.
90 interpretation "Not" 'not a = (Not a).
91 notation "✶" non associative with precedence 90 for @{'unit}.
92 interpretation "dummy prop" 'unit = unit.
93 notation > "\exists list1 ident x sep , . term 19 Px" with precedence 20
94 for ${ fold right @{$Px} rec acc @{'myexists (λ${ident x}.$acc)} }.
95 notation < "hvbox(\exists ident i break . p)" with precedence 20
96 for @{ 'myexists (\lambda ${ident i} : $ty. $p) }.
97 interpretation "constructive ex" 'myexists \eta.x = (Exists sort x).
98 notation > "\forall ident x.break term 19 Px" with precedence 20
99 for @{ 'Forall (λ${ident x}.$Px) }.
100 notation < "\forall ident x.break term 19 Px" with precedence 20
101 for @{ 'Forall (λ${ident x}:$tx.$Px) }.
102 interpretation "Forall" 'Forall \eta.Px = (Forall ? Px).
125 (* Every formula user provided annotates its proof:
126 `A` becomes `(show A ?)` *)
127 definition show : ΠA.A→A ≝ λA:CProp.λa:A.a.
129 (* When something does not fit, this daemon is used *)
130 axiom cast: ΠA,B:CProp.B → A.
132 (* begin a proof: draws the root *)
133 notation > "'prove' p" non associative with precedence 19
135 interpretation "prove KO" 'prove p = (cast ? ? (show p ?)).
136 interpretation "prove OK" 'prove p = (show p ?).
139 notation < "\infrule (t\atop ⋮) a ?" with precedence 19
140 for @{ 'leaf_ok $a $t }.
141 interpretation "leaf OK" 'leaf_ok a t = (show a t).
142 notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19
143 for @{ 'leaf_ko $a $t }.
144 interpretation "leaf KO" 'leaf_ko a t = (cast ? ? (show a t)).
147 notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19
148 for @{ 'discharge_ko_1 $a $H }.
149 interpretation "discharge_ko_1" 'discharge_ko_1 a H =
150 (show a (cast ? ? (Discharge ? H))).
151 notation < "[ mstyle color #ff0000 (a) ] \sup mstyle color #ff0000 (H)" with precedence 19
152 for @{ 'discharge_ko_2 $a $H }.
153 interpretation "discharge_ko_2" 'discharge_ko_2 a H =
154 (cast ? ? (show a (cast ? ? (Discharge ? H)))).
156 notation < "[ a ] \sup H" with precedence 19
157 for @{ 'discharge_ok_1 $a $H }.
158 interpretation "discharge_ok_1" 'discharge_ok_1 a H =
159 (show a (Discharge ? H)).
160 notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19
161 for @{ 'discharge_ok_2 $a $H }.
162 interpretation "discharge_ok_2" 'discharge_ok_2 a H =
163 (cast ? ? (show a (Discharge ? H))).
165 notation > "'discharge' [H]" with precedence 19
166 for @{ 'discharge $H }.
167 interpretation "discharge KO" 'discharge H = (cast ? ? (Discharge ? H)).
168 interpretation "discharge OK" 'discharge H = (Discharge ? H).
171 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
172 for @{ 'Imply_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
173 interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b =
174 (show ab (cast ? ? (Imply_intro ? ? b))).
176 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
177 for @{ 'Imply_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
178 interpretation "Imply_intro_ko_2" 'Imply_intro_ko_2 ab \eta.b =
179 (cast ? ? (show ab (cast ? ? (Imply_intro ? ? b)))).
181 notation < "maction (\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) ) (\vdots)" with precedence 19
182 for @{ 'Imply_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
183 interpretation "Imply_intro_ok_1" 'Imply_intro_ok_1 ab \eta.b =
184 (show ab (Imply_intro ? ? b)).
186 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (⇒\sub\i \emsp ident H) " with precedence 19
187 for @{ 'Imply_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
188 interpretation "Imply_intro_ok_2" 'Imply_intro_ok_2 ab \eta.b =
189 (cast ? ? (show ab (Imply_intro ? ? b))).
191 notation > "⇒#'i' [ident H] term 90 b" with precedence 19
192 for @{ 'Imply_intro $b (λ${ident H}.show $b ?) }.
194 interpretation "Imply_intro KO" 'Imply_intro b pb =
195 (cast ? (Imply unit b) (Imply_intro ? b pb)).
196 interpretation "Imply_intro OK" 'Imply_intro b pb =
197 (Imply_intro ? b pb).
200 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19
201 for @{ 'Imply_elim_ko_1 $ab $a $b }.
202 interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b =
203 (show b (cast ? ? (Imply_elim ? ? (cast ? ? ab) (cast ? ? a)))).
205 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19
206 for @{ 'Imply_elim_ko_2 $ab $a $b }.
207 interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b =
208 (cast ? ? (show b (cast ? ? (Imply_elim ? ? (cast ? ? ab) (cast ? ? a))))).
210 notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) ) (\vdots)" with precedence 19
211 for @{ 'Imply_elim_ok_1 $ab $a $b }.
212 interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b =
213 (show b (Imply_elim ? ? ab a)).
215 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (⇒\sub\e) " with precedence 19
216 for @{ 'Imply_elim_ok_2 $ab $a $b }.
217 interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b =
218 (cast ? ? (show b (Imply_elim ? ? ab a))).
220 notation > "⇒#'e' term 90 ab term 90 a" with precedence 19
221 for @{ 'Imply_elim (show $ab ?) (show $a ?) }.
222 interpretation "Imply_elim KO" 'Imply_elim ab a =
223 (cast ? ? (Imply_elim ? ? (cast (Imply unit unit) ? ab) (cast unit ? a))).
224 interpretation "Imply_elim OK" 'Imply_elim ab a =
225 (Imply_elim ? ? ab a).
228 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19
229 for @{ 'And_intro_ko_1 $a $b $ab }.
230 interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab =
231 (show ab (cast ? ? (And_intro ? ? a b))).
233 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19
234 for @{ 'And_intro_ko_2 $a $b $ab }.
235 interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab =
236 (cast ? ? (show ab (cast ? ? (And_intro ? ? a b)))).
238 notation < "maction (\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)) (\vdots)" with precedence 19
239 for @{ 'And_intro_ok_1 $a $b $ab }.
240 interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab =
241 (show ab (And_intro ? ? a b)).
243 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) (∧\sub\i)" with precedence 19
244 for @{ 'And_intro_ok_2 $a $b $ab }.
245 interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab =
246 (cast ? ? (show ab (And_intro ? ? a b))).
248 notation > "∧#'i' term 90 a term 90 b" with precedence 19
249 for @{ 'And_intro (show $a ?) (show $b ?) }.
250 interpretation "And_intro KO" 'And_intro a b = (cast ? ? (And_intro ? ? a b)).
251 interpretation "And_intro OK" 'And_intro a b = (And_intro ? ? a b).
254 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
255 for @{ 'And_elim_l_ko_1 $ab $a }.
256 interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a =
257 (show a (cast ? ? (And_elim_l ? ? (cast ? ? ab)))).
259 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
260 for @{ 'And_elim_l_ko_2 $ab $a }.
261 interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a =
262 (cast ? ? (show a (cast ? ? (And_elim_l ? ? (cast ? ? ab))))).
264 notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))) (\vdots)" with precedence 19
265 for @{ 'And_elim_l_ok_1 $ab $a }.
266 interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a =
267 (show a (And_elim_l ? ? ab)).
269 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\l))" with precedence 19
270 for @{ 'And_elim_l_ok_2 $ab $a }.
271 interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a =
272 (cast ? ? (show a (And_elim_l ? ? ab))).
274 notation > "∧#'e_l' term 90 ab" with precedence 19
275 for @{ 'And_elim_l (show $ab ?) }.
276 interpretation "And_elim_l KO" 'And_elim_l a = (cast ? ? (And_elim_l ? ? (cast (And unit unit) ? a))).
277 interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l ? ? a).
279 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
280 for @{ 'And_elim_r_ko_1 $ab $a }.
281 interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a =
282 (show a (cast ? ? (And_elim_r ? ? (cast ? ? ab)))).
284 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
285 for @{ 'And_elim_r_ko_2 $ab $a }.
286 interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a =
287 (cast ? ? (show a (cast ? ? (And_elim_r ? ? (cast ? ? ab))))).
289 notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))) (\vdots)" with precedence 19
290 for @{ 'And_elim_r_ok_1 $ab $a }.
291 interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a =
292 (show a (And_elim_r ? ? ab)).
294 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\r))" with precedence 19
295 for @{ 'And_elim_r_ok_2 $ab $a }.
296 interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a =
297 (cast ? ? (show a (And_elim_r ? ? ab))).
299 notation > "∧#'e_r' term 90 ab" with precedence 19
300 for @{ 'And_elim_r (show $ab ?) }.
301 interpretation "And_elim_r KO" 'And_elim_r a = (cast ? ? (And_elim_r ? ? (cast (And unit unit) ? a))).
302 interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r ? ? a).
305 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
306 for @{ 'Or_intro_l_ko_1 $a $ab }.
307 interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab =
308 (show ab (cast ? ? (Or_intro_l ? ? a))).
310 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
311 for @{ 'Or_intro_l_ko_2 $a $ab }.
312 interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab =
313 (cast ? ? (show ab (cast ? ? (Or_intro_l ? ? a)))).
315 notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))) (\vdots)" with precedence 19
316 for @{ 'Or_intro_l_ok_1 $a $ab }.
317 interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab =
318 (show ab (Or_intro_l ? ? a)).
320 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19
321 for @{ 'Or_intro_l_ok_2 $a $ab }.
322 interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab =
323 (cast ? ? (show ab (Or_intro_l ? ? a))).
325 notation > "∨#'i_l' term 90 a" with precedence 19
326 for @{ 'Or_intro_l (show $a ?) }.
327 interpretation "Or_intro_l KO" 'Or_intro_l a = (cast ? (Or ? unit) (Or_intro_l ? ? a)).
328 interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l ? ? a).
330 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
331 for @{ 'Or_intro_r_ko_1 $a $ab }.
332 interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab =
333 (show ab (cast ? ? (Or_intro_r ? ? a))).
335 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
336 for @{ 'Or_intro_r_ko_2 $a $ab }.
337 interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab =
338 (cast ? ? (show ab (cast ? ? (Or_intro_r ? ? a)))).
340 notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))) (\vdots)" with precedence 19
341 for @{ 'Or_intro_r_ok_1 $a $ab }.
342 interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab =
343 (show ab (Or_intro_r ? ? a)).
345 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19
346 for @{ 'Or_intro_r_ok_2 $a $ab }.
347 interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab =
348 (cast ? ? (show ab (Or_intro_r ? ? a))).
350 notation > "∨#'i_r' term 90 a" with precedence 19
351 for @{ 'Or_intro_r (show $a ?) }.
352 interpretation "Or_intro_r KO" 'Or_intro_r a = (cast ? (Or unit ?) (Or_intro_r ? ? a)).
353 interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r ? ? a).
356 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
357 for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }.
358 interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc =
359 (show c (cast ? ? (Or_elim ? ? ? (cast ? ? ab) (cast ? ? ac) (cast ? ? bc)))).
361 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
362 for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
363 interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c =
364 (cast ? ? (show c (cast ? ? (Or_elim ? ? ? (cast ? ? ab) (cast ? ? ac) (cast ? ? bc))))).
366 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
367 for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
368 interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c =
369 (show c (Or_elim ? ? ? ab ac bc)).
371 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
372 for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
373 interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c =
374 (cast ? ? (show c (Or_elim ? ? ? ab ac bc))).
376 definition unit_to ≝ λx:CProp.unit → x.
378 notation > "∨#'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19
379 for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) }.
380 interpretation "Or_elim KO" 'Or_elim ab ac bc =
381 (cast ? ? (Or_elim ? ? ?
382 (cast (Or unit unit) ? ab)
383 (cast (unit_to unit) (unit_to ?) ac)
384 (cast (unit_to unit) (unit_to ?) bc))).
385 interpretation "Or_elim OK" 'Or_elim ab ac bc = (Or_elim ? ? ? ab ac bc).
388 notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19
389 for @{'Top_intro_ko_1}.
390 interpretation "Top_intro_ko_1" 'Top_intro_ko_1 =
391 (show ? (cast ? ? Top_intro)).
393 notation < "\infrule \nbsp mstyle color #ff0000 (⊤) mstyle color #ff0000 (⊤\sub\i)" with precedence 19
394 for @{'Top_intro_ko_2}.
395 interpretation "Top_intro_ko_2" 'Top_intro_ko_2 =
396 (cast ? ? (show ? (cast ? ? Top_intro))).
398 notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19
399 for @{'Top_intro_ok_1}.
400 interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show ? Top_intro).
402 notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19
403 for @{'Top_intro_ok_2 }.
404 interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast ? ? (show ? Top_intro)).
406 notation > "⊤#'i'" with precedence 19 for @{ 'Top_intro }.
407 interpretation "Top_intro KO" 'Top_intro = (cast ? ? Top_intro).
408 interpretation "Top_intro OK" 'Top_intro = Top_intro.
411 notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19
412 for @{'Bot_elim_ko_1 $a $b}.
413 interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b =
414 (show a (Bot_elim ? (cast ? ? b))).
416 notation < "\infrule b mstyle color #ff0000 (a) mstyle color #ff0000 (⊥\sub\e)" with precedence 19
417 for @{'Bot_elim_ko_2 $a $b}.
418 interpretation "Bot_elim_ko_2" 'Bot_elim_ko_2 a b =
419 (cast ? ? (show a (Bot_elim ? (cast ? ? b)))).
421 notation < "maction (\infrule b a (⊥\sub\e)) (\vdots)" with precedence 19
422 for @{'Bot_elim_ok_1 $a $b}.
423 interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b =
424 (show a (Bot_elim ? b)).
426 notation < "\infrule b mstyle color #ff0000 (a) (⊥\sub\e)" with precedence 19
427 for @{'Bot_elim_ok_2 $a $b}.
428 interpretation "Bot_elim_ok_2" 'Bot_elim_ok_2 a b =
429 (cast ? ? (show a (Bot_elim ? b))).
431 notation > "⊥#'e' term 90 b" with precedence 19
432 for @{ 'Bot_elim (show $b ?) }.
433 interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim ? (cast ? ? a)).
434 interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim ? a).
437 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
438 for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
439 interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b =
440 (show ab (cast ? ? (Not_intro ? (cast ? ? b)))).
442 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
443 for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
444 interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b =
445 (cast ? ? (show ab (cast ? ? (Not_intro ? (cast ? ? b))))).
447 notation < "maction (\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) ) (\vdots)" with precedence 19
448 for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
449 interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b =
450 (show ab (Not_intro ? b)).
452 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub(\emsp\i) \emsp ident H) " with precedence 19
453 for @{ 'Not_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
454 interpretation "Not_intro_ok_2" 'Not_intro_ok_2 ab \eta.b =
455 (cast ? ? (show ab (Not_intro ? b))).
457 notation > "¬#'i' [ident H] term 90 b" with precedence 19
458 for @{ 'Not_intro (λ${ident H}.show $b ?) }.
459 interpretation "Not_intro KO" 'Not_intro a = (cast ? ? (Not_intro ? (cast ? ? a))).
460 interpretation "Not_intro OK" 'Not_intro a = (Not_intro ? a).
463 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19
464 for @{ 'Not_elim_ko_1 $ab $a $b }.
465 interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b =
466 (show b (cast ? ? (Not_elim ? (cast ? ? ab) (cast ? ? a)))).
468 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19
469 for @{ 'Not_elim_ko_2 $ab $a $b }.
470 interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b =
471 (cast ? ? (show b (cast ? ? (Not_elim ? (cast ? ? ab) (cast ? ? a))))).
473 notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) ) (\vdots)" with precedence 19
474 for @{ 'Not_elim_ok_1 $ab $a $b }.
475 interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b =
476 (show b (Not_elim ? ab a)).
478 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub(\emsp\e)) " with precedence 19
479 for @{ 'Not_elim_ok_2 $ab $a $b }.
480 interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b =
481 (cast ? ? (show b (Not_elim ? ab a))).
483 notation > "¬#'e' term 90 ab term 90 a" with precedence 19
484 for @{ 'Not_elim (show $ab ?) (show $a ?) }.
485 interpretation "Not_elim KO" 'Not_elim ab a =
486 (cast ? ? (Not_elim unit (cast ? ? ab) (cast ? ? a))).
487 interpretation "Not_elim OK" 'Not_elim ab a =
491 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
492 for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
493 interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn =
494 (show Pn (cast ? ? (Raa ? (cast ? ? Px)))).
496 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
497 for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
498 interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn =
499 (cast ? ? (show Pn (cast ? ? (Raa ? (cast ? ? Px))))).
501 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)) (\vdots)" with precedence 19
502 for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
503 interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn =
504 (show Pn (Raa ? Px)).
506 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (\RAA \emsp ident x)" with precedence 19
507 for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
508 interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn =
509 (cast ? ? (show Pn (Raa ? Px))).
511 notation > "'RAA' [ident H] term 90 b" with precedence 19
512 for @{ 'Raa (λ${ident H}.show $b ?) }.
513 interpretation "RAA KO" 'Raa p = (cast ? unit (Raa ? (cast ? (unit_to ?) p))).
514 interpretation "RAA OK" 'Raa p = (Raa ? p).
517 notation < "\infrule hbox(\emsp Pn \emsp) Px mstyle color #ff0000 (∃\sub\i)" with precedence 19
518 for @{ 'Exists_intro_ko_1 $Pn $Px }.
519 interpretation "Exists_intro_ko_1" 'Exists_intro_ko_1 Pn Px =
520 (show Px (cast ? ? (Exists_intro ? ? ? (cast ? ? Pn)))).
522 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) mstyle color #ff0000 (∃\sub\i)" with precedence 19
523 for @{ 'Exists_intro_ko_2 $Pn $Px }.
524 interpretation "Exists_intro_ko_2" 'Exists_intro_ko_2 Pn Px =
525 (cast ? ? (show Px (cast ? ? (Exists_intro ? ? ? (cast ? ? Pn))))).
527 notation < "maction (\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)) (\vdots)" with precedence 19
528 for @{ 'Exists_intro_ok_1 $Pn $Px }.
529 interpretation "Exists_intro_ok_1" 'Exists_intro_ok_1 Pn Px =
530 (show Px (Exists_intro ? ? ? Pn)).
532 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) (∃\sub\i)" with precedence 19
533 for @{ 'Exists_intro_ok_2 $Pn $Px }.
534 interpretation "Exists_intro_ok_2" 'Exists_intro_ok_2 Pn Px =
535 (cast ? ? (show Px (Exists_intro ? ? ? Pn))).
537 notation >"∃#'i' {term 90 t} term 90 Pt" non associative with precedence 19
538 for @{'Exists_intro $t (λw.? w) (show $Pt ?)}.
539 interpretation "Exists_intro KO" 'Exists_intro t P Pt =
540 (cast ? ? (Exists_intro sort P t (cast ? ? Pt))).
541 interpretation "Exists_intro OK" 'Exists_intro t P Pt =
542 (Exists_intro sort P t Pt).
545 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
546 for @{ 'Exists_elim_ko_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
547 interpretation "Exists_elim_ko_1" 'Exists_elim_ko_1 ExPx Pc c =
548 (show c (cast ? ? (Exists_elim ? ? ? (cast ? ? ExPx) (cast ? ? Pc)))).
550 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
551 for @{ 'Exists_elim_ko_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
552 interpretation "Exists_elim_ko_2" 'Exists_elim_ko_2 ExPx Pc c =
553 (cast ? ? (show c (cast ? ? (Exists_elim ? ? ? (cast ? ? ExPx) (cast ? ? Pc))))).
555 notation < "maction (\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)) (\vdots)" with precedence 19
556 for @{ 'Exists_elim_ok_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
557 interpretation "Exists_elim_ok_1" 'Exists_elim_ok_1 ExPx Pc c =
558 (show c (Exists_elim ? ? ? ExPx Pc)).
560 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
561 for @{ 'Exists_elim_ok_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
562 interpretation "Exists_elim_ok_2" 'Exists_elim_ok_2 ExPx Pc c =
563 (cast ? ? (show c (Exists_elim ? ? ? ExPx Pc))).
565 definition ex_concl := λx:sort → CProp.∀y:sort.unit → x y.
566 definition ex_concl_dummy := ∀y:sort.unit → unit.
567 definition fake_pred := λx:sort.unit.
569 notation >"∃#'e' term 90 ExPt {ident t} [ident H] term 90 c" non associative with precedence 19
570 for @{'Exists_elim (λx.? x) (show $ExPt ?) (λ${ident t}:sort.λ${ident H}.show $c ?)}.
571 interpretation "Exists_elim KO" 'Exists_elim P ExPt c =
572 (cast ? ? (Exists_elim sort P ?
573 (cast (Exists ? P) ? ExPt)
574 (cast ex_concl_dummy (ex_concl ?) c))).
575 interpretation "Exists_elim OK" 'Exists_elim P ExPt c =
576 (Exists_elim sort P ? ExPt c).
580 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
581 for @{ 'Forall_intro_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
582 interpretation "Forall_intro_ko_1" 'Forall_intro_ko_1 Px Pn =
583 (show Pn (cast ? ? (Forall_intro ? ? (cast ? ? Px)))).
585 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
586 for @{ 'Forall_intro_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
587 interpretation "Forall_intro_ko_2" 'Forall_intro_ko_2 Px Pn =
588 (cast ? ? (show Pn (cast ? ? (Forall_intro ? ? (cast ? ? Px))))).
590 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)) (\vdots)" with precedence 19
591 for @{ 'Forall_intro_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
592 interpretation "Forall_intro_ok_1" 'Forall_intro_ok_1 Px Pn =
593 (show Pn (Forall_intro ? ? Px)).
595 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\i \emsp ident x)" with precedence 19
596 for @{ 'Forall_intro_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
597 interpretation "Forall_intro_ok_2" 'Forall_intro_ok_2 Px Pn =
598 (cast ? ? (show Pn (Forall_intro ? ? Px))).
600 notation > "∀#'i' {ident y} term 90 Px" non associative with precedence 19
601 for @{ 'Forall_intro (λ_.?) (λ${ident y}.show $Px ?) }.
602 interpretation "Forall_intro KO" 'Forall_intro P Px =
603 (cast ? ? (Forall_intro sort P (cast ? ? Px))).
604 interpretation "Forall_intro OK" 'Forall_intro P Px =
605 (Forall_intro sort P Px).
608 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\e))" with precedence 19
609 for @{ 'Forall_elim_ko_1 $Px $Pn }.
610 interpretation "Forall_elim_ko_1" 'Forall_elim_ko_1 Px Pn =
611 (show Pn (cast ? ? (Forall_elim ? ? ? (cast ? ? Px)))).
613 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\e))" with precedence 19
614 for @{ 'Forall_elim_ko_2 $Px $Pn }.
615 interpretation "Forall_elim_ko_2" 'Forall_elim_ko_2 Px Pn =
616 (cast ? ? (show Pn (cast ? ? (Forall_elim ? ? ? (cast ? ? Px))))).
618 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)) (\vdots)" with precedence 19
619 for @{ 'Forall_elim_ok_1 $Px $Pn }.
620 interpretation "Forall_elim_ok_1" 'Forall_elim_ok_1 Px Pn =
621 (show Pn (Forall_elim ? ? ? Px)).
623 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\e)" with precedence 19
624 for @{ 'Forall_elim_ok_2 $Px $Pn }.
625 interpretation "Forall_elim_ok_2" 'Forall_elim_ok_2 Px Pn =
626 (cast ? ? (show Pn (Forall_elim ? ? ? Px))).
628 notation > "∀#'e' {term 90 t} term 90 Pn" non associative with precedence 19
629 for @{ 'Forall_elim (λ_.?) $t (show $Pn ?) }.
630 interpretation "Forall_elim KO" 'Forall_elim P t Px =
631 (cast ? unit (Forall_elim sort P t (cast ? ? Px))).
632 interpretation "Forall_elim OK" 'Forall_elim P t Px =
633 (Forall_elim sort P t Px).
635 (* already proved lemma *)
636 definition hide_args : ∀A:Type.A→A := λA:Type.λa:A.a.
637 notation < "t" non associative with precedence 90 for @{'hide_args $t}.
638 interpretation "hide 0 args" 'hide_args t = (hide_args ? t).
639 interpretation "hide 1 args" 'hide_args t = (hide_args ? t ?).
640 interpretation "hide 2 args" 'hide_args t = (hide_args ? t ? ?).
641 interpretation "hide 3 args" 'hide_args t = (hide_args ? t ? ? ?).
642 interpretation "hide 4 args" 'hide_args t = (hide_args ? t ? ? ? ?).
643 interpretation "hide 5 args" 'hide_args t = (hide_args ? t ? ? ? ? ?).
644 interpretation "hide 6 args" 'hide_args t = (hide_args ? t ? ? ? ? ? ?).
645 interpretation "hide 7 args" 'hide_args t = (hide_args ? t ? ? ? ? ? ? ?).
647 (* more args crashes the pattern matcher *)
649 (* already proved lemma, 0 assumptions *)
650 definition Lemma : ΠA.A→A ≝ λA:CProp.λa:A.a.
655 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
657 non associative with precedence 19
658 for @{ 'lemma_ko_1 $p ($H : $_) }.
659 interpretation "lemma_ko_1" 'lemma_ko_1 p H =
660 (show p (cast ? ? (Lemma ? (cast ? ? H)))).
665 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
666 mstyle color #ff0000 (p) \nbsp"
667 non associative with precedence 19
668 for @{ 'lemma_ko_2 $p ($H : $_) }.
669 interpretation "lemma_ko_2" 'lemma_ko_2 p H =
670 (cast ? ? (show p (cast ? ?
671 (Lemma ? (cast ? ? H))))).
677 (╲ mstyle mathsize normal (H) ╱) \nbsp)
679 non associative with precedence 19
680 for @{ 'lemma_ok_1 $p ($H : $_) }.
681 interpretation "lemma_ok_1" 'lemma_ok_1 p H =
682 (show p (Lemma ? H)).
687 (╲ mstyle mathsize normal (H) ╱) \nbsp)
688 mstyle color #ff0000 (p) \nbsp"
689 non associative with precedence 19
690 for @{ 'lemma_ok_2 $p ($H : $_) }.
691 interpretation "lemma_ok_2" 'lemma_ok_2 p H =
692 (cast ? ? (show p (Lemma ? H))).
694 notation > "'lem' 0 term 90 l" non associative with precedence 19
695 for @{ 'Lemma (hide_args ? $l : ?) }.
696 interpretation "lemma KO" 'Lemma l =
697 (cast ? ? (Lemma unit (cast unit ? l))).
698 interpretation "lemma OK" 'Lemma l = (Lemma ? l).
701 (* already proved lemma, 1 assumption *)
702 definition Lemma1 : ΠA,B. (A ⇒ B) → A → B ≝
703 λA,B:CProp.λf:A⇒B.λa:A.
709 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
711 non associative with precedence 19
712 for @{ 'lemma1_ko_1 $a $p ($H : $_) }.
713 interpretation "lemma1_ko_1" 'lemma1_ko_1 a p H =
714 (show p (cast ? ? (Lemma1 ? ? (cast ? ? H) (cast ? ? a)))).
719 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
720 mstyle color #ff0000 (p) \nbsp"
721 non associative with precedence 19
722 for @{ 'lemma1_ko_2 $a $p ($H : $_) }.
723 interpretation "lemma1_ko_2" 'lemma1_ko_2 a p H =
724 (cast ? ? (show p (cast ? ?
725 (Lemma1 ? ? (cast ? ? H) (cast ? ? a))))).
731 (╲ mstyle mathsize normal (H) ╱) \nbsp)
733 non associative with precedence 19
734 for @{ 'lemma1_ok_1 $a $p ($H : $_) }.
735 interpretation "lemma1_ok_1" 'lemma1_ok_1 a p H =
736 (show p (Lemma1 ? ? H a)).
741 (╲ mstyle mathsize normal (H) ╱) \nbsp)
742 mstyle color #ff0000 (p) \nbsp"
743 non associative with precedence 19
744 for @{ 'lemma1_ok_2 $a $p ($H : $_) }.
745 interpretation "lemma1_ok_2" 'lemma1_ok_2 a p H =
746 (cast ? ? (show p (Lemma1 ? ? H a))).
749 notation > "'lem' 1 term 90 l term 90 p" non associative with precedence 19
750 for @{ 'Lemma1 (hide_args ? $l : ?) (show $p ?) }.
751 interpretation "lemma 1 KO" 'Lemma1 l p =
752 (cast ? ? (Lemma1 unit unit (cast (Imply unit unit) ? l) (cast unit ? p))).
753 interpretation "lemma 1 OK" 'Lemma1 l p = (Lemma1 ? ? l p).
755 (* already proved lemma, 2 assumptions *)
756 definition Lemma2 : ΠA,B,C. (A ⇒ B ⇒ C) → A → B → C ≝
757 λA,B,C:CProp.λf:A⇒B⇒C.λa:A.λb:B.
758 Imply_elim B C (Imply_elim A (B⇒C) f a) b.
762 (\emsp a \emsp\emsp\emsp b \emsp)
763 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
765 non associative with precedence 19
766 for @{ 'lemma2_ko_1 $a $b $p ($H : $_) }.
767 interpretation "lemma2_ko_1" 'lemma2_ko_1 a b p H =
768 (show p (cast ? ? (Lemma2 ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b)))).
772 (\emsp a \emsp\emsp\emsp b \emsp)
773 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
774 mstyle color #ff0000 (p) \nbsp"
775 non associative with precedence 19
776 for @{ 'lemma2_ko_2 $a $b $p ($H : $_) }.
777 interpretation "lemma2_ko_2" 'lemma2_ko_2 a b p H =
778 (cast ? ? (show p (cast ? ?
779 (Lemma2 ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b))))).
784 (\emsp a \emsp\emsp\emsp b \emsp)
785 (╲ mstyle mathsize normal (H) ╱) \nbsp)
787 non associative with precedence 19
788 for @{ 'lemma2_ok_1 $a $b $p ($H : $_) }.
789 interpretation "lemma2_ok_1" 'lemma2_ok_1 a b p H =
790 (show p (Lemma2 ? ? ? H a b)).
794 (\emsp a \emsp\emsp\emsp b \emsp)
795 (╲ mstyle mathsize normal (H) ╱) \nbsp)
796 mstyle color #ff0000 (p) \nbsp"
797 non associative with precedence 19
798 for @{ 'lemma2_ok_2 $a $b $p ($H : $_) }.
799 interpretation "lemma2_ok_2" 'lemma2_ok_2 a b p H =
800 (cast ? ? (show p (Lemma2 ? ? ? H a b))).
802 notation > "'lem' 2 term 90 l term 90 p term 90 q" non associative with precedence 19
803 for @{ 'Lemma2 (hide_args ? $l : ?) (show $p ?) (show $q ?) }.
804 interpretation "lemma 2 KO" 'Lemma2 l p q =
805 (cast ? ? (Lemma2 unit unit unit (cast (Imply unit (Imply unit unit)) ? l) (cast unit ? p) (cast unit ? q))).
806 interpretation "lemma 2 OK" 'Lemma2 l p q = (Lemma2 ? ? ? l p q).
808 (* already proved lemma, 3 assumptions *)
809 definition Lemma3 : ΠA,B,C,D. (A ⇒ B ⇒ C ⇒ D) → A → B → C → D ≝
810 λA,B,C,D:CProp.λf:A⇒B⇒C⇒D.λa:A.λb:B.λc:C.
811 Imply_elim C D (Imply_elim B (C⇒D) (Imply_elim A (B⇒C⇒D) f a) b) c.
815 (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
816 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
818 non associative with precedence 19
819 for @{ 'lemma3_ko_1 $a $b $c $p ($H : $_) }.
820 interpretation "lemma3_ko_1" 'lemma3_ko_1 a b c p H =
822 (Lemma3 ? ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b) (cast ? ? c)))).
826 (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
827 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
828 mstyle color #ff0000 (p) \nbsp"
829 non associative with precedence 19
830 for @{ 'lemma3_ko_2 $a $b $c $p ($H : $_) }.
831 interpretation "lemma3_ko_2" 'lemma3_ko_2 a b c p H =
832 (cast ? ? (show p (cast ? ?
833 (Lemma3 ? ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b) (cast ? ? c))))).
838 (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
839 (╲ mstyle mathsize normal (H) ╱) \nbsp)
841 non associative with precedence 19
842 for @{ 'lemma3_ok_1 $a $b $c $p ($H : $_) }.
843 interpretation "lemma3_ok_1" 'lemma3_ok_1 a b c p H =
844 (show p (Lemma3 ? ? ? ? H a b c)).
848 (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
849 (╲ mstyle mathsize normal (H) ╱) \nbsp)
850 mstyle color #ff0000 (p) \nbsp"
851 non associative with precedence 19
852 for @{ 'lemma3_ok_2 $a $b $c $p ($H : $_) }.
853 interpretation "lemma3_ok_2" 'lemma3_ok_2 a b c p H =
854 (cast ? ? (show p (Lemma3 ? ? ? ? H a b c))).
856 notation > "'lem' 3 term 90 l term 90 p term 90 q term 90 r" non associative with precedence 19
857 for @{ 'Lemma3 (hide_args ? $l : ?) (show $p ?) (show $q ?) (show $r ?) }.
858 interpretation "lemma 3 KO" 'Lemma3 l p q r =
859 (cast ? ? (Lemma3 unit unit unit unit (cast (Imply unit (Imply unit (Imply unit unit))) ? l) (cast unit ? p) (cast unit ? q) (cast unit ? r))).
860 interpretation "lemma 3 OK" 'Lemma3 l p q r = (Lemma3 ? ? ? ? l p q r).