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 ?) }.
193 interpretation "Imply_intro KO" 'Imply_intro b pb =
194 (cast _ (Imply unit b) (Imply_intro _ b pb)).
195 interpretation "Imply_intro OK" 'Imply_intro b pb =
196 (Imply_intro _ b pb).
199 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19
200 for @{ 'Imply_elim_ko_1 $ab $a $b }.
201 interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b =
202 (show b (cast _ _ (Imply_elim _ _ (cast _ _ ab) (cast _ _ a)))).
204 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19
205 for @{ 'Imply_elim_ko_2 $ab $a $b }.
206 interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b =
207 (cast _ _ (show b (cast _ _ (Imply_elim _ _ (cast _ _ ab) (cast _ _ a))))).
209 notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) ) (\vdots)" with precedence 19
210 for @{ 'Imply_elim_ok_1 $ab $a $b }.
211 interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b =
212 (show b (Imply_elim _ _ ab a)).
214 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (⇒\sub\e) " with precedence 19
215 for @{ 'Imply_elim_ok_2 $ab $a $b }.
216 interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b =
217 (cast _ _ (show b (Imply_elim _ _ ab a))).
219 notation > "⇒_'e' term 90 ab term 90 a" with precedence 19
220 for @{ 'Imply_elim (show $ab ?) (show $a ?) }.
221 interpretation "Imply_elim KO" 'Imply_elim ab a =
222 (cast _ _ (Imply_elim _ _ (cast (Imply unit unit) _ ab) (cast unit _ a))).
223 interpretation "Imply_elim OK" 'Imply_elim ab a =
224 (Imply_elim _ _ ab a).
227 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19
228 for @{ 'And_intro_ko_1 $a $b $ab }.
229 interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab =
230 (show ab (cast _ _ (And_intro _ _ a b))).
232 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19
233 for @{ 'And_intro_ko_2 $a $b $ab }.
234 interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab =
235 (cast _ _ (show ab (cast _ _ (And_intro _ _ a b)))).
237 notation < "maction (\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)) (\vdots)" with precedence 19
238 for @{ 'And_intro_ok_1 $a $b $ab }.
239 interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab =
240 (show ab (And_intro _ _ a b)).
242 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) (∧\sub\i)" with precedence 19
243 for @{ 'And_intro_ok_2 $a $b $ab }.
244 interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab =
245 (cast _ _ (show ab (And_intro _ _ a b))).
247 notation > "∧_'i' term 90 a term 90 b" with precedence 19
248 for @{ 'And_intro (show $a ?) (show $b ?) }.
249 interpretation "And_intro KO" 'And_intro a b = (cast _ _ (And_intro _ _ a b)).
250 interpretation "And_intro OK" 'And_intro a b = (And_intro _ _ a b).
253 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
254 for @{ 'And_elim_l_ko_1 $ab $a }.
255 interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a =
256 (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab)))).
258 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
259 for @{ 'And_elim_l_ko_2 $ab $a }.
260 interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a =
261 (cast _ _ (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab))))).
263 notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))) (\vdots)" with precedence 19
264 for @{ 'And_elim_l_ok_1 $ab $a }.
265 interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a =
266 (show a (And_elim_l _ _ ab)).
268 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\l))" with precedence 19
269 for @{ 'And_elim_l_ok_2 $ab $a }.
270 interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a =
271 (cast _ _ (show a (And_elim_l _ _ ab))).
273 notation > "∧_'e_l' term 90 ab" with precedence 19
274 for @{ 'And_elim_l (show $ab ?) }.
275 interpretation "And_elim_l KO" 'And_elim_l a = (cast _ _ (And_elim_l _ _ (cast (And unit unit) _ a))).
276 interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l _ _ a).
278 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
279 for @{ 'And_elim_r_ko_1 $ab $a }.
280 interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a =
281 (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab)))).
283 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
284 for @{ 'And_elim_r_ko_2 $ab $a }.
285 interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a =
286 (cast _ _ (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab))))).
288 notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))) (\vdots)" with precedence 19
289 for @{ 'And_elim_r_ok_1 $ab $a }.
290 interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a =
291 (show a (And_elim_r _ _ ab)).
293 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\r))" with precedence 19
294 for @{ 'And_elim_r_ok_2 $ab $a }.
295 interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a =
296 (cast _ _ (show a (And_elim_r _ _ ab))).
298 notation > "∧_'e_r' term 90 ab" with precedence 19
299 for @{ 'And_elim_r (show $ab ?) }.
300 interpretation "And_elim_r KO" 'And_elim_r a = (cast _ _ (And_elim_r _ _ (cast (And unit unit) _ a))).
301 interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r _ _ a).
304 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
305 for @{ 'Or_intro_l_ko_1 $a $ab }.
306 interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab =
307 (show ab (cast _ _ (Or_intro_l _ _ a))).
309 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
310 for @{ 'Or_intro_l_ko_2 $a $ab }.
311 interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab =
312 (cast _ _ (show ab (cast _ _ (Or_intro_l _ _ a)))).
314 notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))) (\vdots)" with precedence 19
315 for @{ 'Or_intro_l_ok_1 $a $ab }.
316 interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab =
317 (show ab (Or_intro_l _ _ a)).
319 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19
320 for @{ 'Or_intro_l_ok_2 $a $ab }.
321 interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab =
322 (cast _ _ (show ab (Or_intro_l _ _ a))).
324 notation > "∨_'i_l' term 90 a" with precedence 19
325 for @{ 'Or_intro_l (show $a ?) }.
326 interpretation "Or_intro_l KO" 'Or_intro_l a = (cast _ (Or _ unit) (Or_intro_l _ _ a)).
327 interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l _ _ a).
329 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
330 for @{ 'Or_intro_r_ko_1 $a $ab }.
331 interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab =
332 (show ab (cast _ _ (Or_intro_r _ _ a))).
334 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
335 for @{ 'Or_intro_r_ko_2 $a $ab }.
336 interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab =
337 (cast _ _ (show ab (cast _ _ (Or_intro_r _ _ a)))).
339 notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))) (\vdots)" with precedence 19
340 for @{ 'Or_intro_r_ok_1 $a $ab }.
341 interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab =
342 (show ab (Or_intro_r _ _ a)).
344 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19
345 for @{ 'Or_intro_r_ok_2 $a $ab }.
346 interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab =
347 (cast _ _ (show ab (Or_intro_r _ _ a))).
349 notation > "∨_'i_r' term 90 a" with precedence 19
350 for @{ 'Or_intro_r (show $a ?) }.
351 interpretation "Or_intro_r KO" 'Or_intro_r a = (cast _ (Or unit _) (Or_intro_r _ _ a)).
352 interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r _ _ a).
355 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
356 for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }.
357 interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc =
358 (show c (cast _ _ (Or_elim _ _ _ (cast _ _ ab) (cast _ _ ac) (cast _ _ bc)))).
360 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
361 for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
362 interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c =
363 (cast _ _ (show c (cast _ _ (Or_elim _ _ _ (cast _ _ ab) (cast _ _ ac) (cast _ _ bc))))).
365 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
366 for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
367 interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c =
368 (show c (Or_elim _ _ _ ab ac bc)).
370 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
371 for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
372 interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c =
373 (cast _ _ (show c (Or_elim _ _ _ ab ac bc))).
375 definition unit_to ≝ λx:CProp.unit → x.
377 notation > "∨_'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19
378 for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) }.
379 interpretation "Or_elim KO" 'Or_elim ab ac bc =
380 (cast _ _ (Or_elim _ _ _
381 (cast (Or unit unit) _ ab)
382 (cast (unit_to unit) (unit_to _) ac)
383 (cast (unit_to unit) (unit_to _) bc))).
384 interpretation "Or_elim OK" 'Or_elim ab ac bc = (Or_elim _ _ _ ab ac bc).
387 notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19
388 for @{'Top_intro_ko_1}.
389 interpretation "Top_intro_ko_1" 'Top_intro_ko_1 =
390 (show _ (cast _ _ Top_intro)).
392 notation < "\infrule \nbsp mstyle color #ff0000 (⊤) mstyle color #ff0000 (⊤\sub\i)" with precedence 19
393 for @{'Top_intro_ko_2}.
394 interpretation "Top_intro_ko_2" 'Top_intro_ko_2 =
395 (cast _ _ (show _ (cast _ _ Top_intro))).
397 notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19
398 for @{'Top_intro_ok_1}.
399 interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show _ Top_intro).
401 notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19
402 for @{'Top_intro_ok_2 }.
403 interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast _ _ (show _ Top_intro)).
405 notation > "⊤_'i'" with precedence 19 for @{ 'Top_intro }.
406 interpretation "Top_intro KO" 'Top_intro = (cast _ _ Top_intro).
407 interpretation "Top_intro OK" 'Top_intro = Top_intro.
410 notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19
411 for @{'Bot_elim_ko_1 $a $b}.
412 interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b =
413 (show a (Bot_elim _ (cast _ _ b))).
415 notation < "\infrule b mstyle color #ff0000 (a) mstyle color #ff0000 (⊥\sub\e)" with precedence 19
416 for @{'Bot_elim_ko_2 $a $b}.
417 interpretation "Bot_elim_ko_2" 'Bot_elim_ko_2 a b =
418 (cast _ _ (show a (Bot_elim _ (cast _ _ b)))).
420 notation < "maction (\infrule b a (⊥\sub\e)) (\vdots)" with precedence 19
421 for @{'Bot_elim_ok_1 $a $b}.
422 interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b =
423 (show a (Bot_elim _ b)).
425 notation < "\infrule b mstyle color #ff0000 (a) (⊥\sub\e)" with precedence 19
426 for @{'Bot_elim_ok_2 $a $b}.
427 interpretation "Bot_elim_ok_2" 'Bot_elim_ok_2 a b =
428 (cast _ _ (show a (Bot_elim _ b))).
430 notation > "⊥_'e' term 90 b" with precedence 19
431 for @{ 'Bot_elim (show $b ?) }.
432 interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim _ (cast _ _ a)).
433 interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim _ a).
436 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
437 for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
438 interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b =
439 (show ab (cast _ _ (Not_intro _ (cast _ _ b)))).
441 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
442 for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
443 interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b =
444 (cast _ _ (show ab (cast _ _ (Not_intro _ (cast _ _ b))))).
446 notation < "maction (\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) ) (\vdots)" with precedence 19
447 for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
448 interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b =
449 (show ab (Not_intro _ b)).
451 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub(\emsp\i) \emsp ident H) " with precedence 19
452 for @{ 'Not_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
453 interpretation "Not_intro_ok_2" 'Not_intro_ok_2 ab \eta.b =
454 (cast _ _ (show ab (Not_intro _ b))).
456 notation > "¬_'i' [ident H] term 90 b" with precedence 19
457 for @{ 'Not_intro (λ${ident H}.show $b ?) }.
458 interpretation "Not_intro KO" 'Not_intro a = (cast _ _ (Not_intro _ (cast _ _ a))).
459 interpretation "Not_intro OK" 'Not_intro a = (Not_intro _ a).
462 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19
463 for @{ 'Not_elim_ko_1 $ab $a $b }.
464 interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b =
465 (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a)))).
467 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19
468 for @{ 'Not_elim_ko_2 $ab $a $b }.
469 interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b =
470 (cast _ _ (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a))))).
472 notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) ) (\vdots)" with precedence 19
473 for @{ 'Not_elim_ok_1 $ab $a $b }.
474 interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b =
475 (show b (Not_elim _ ab a)).
477 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub(\emsp\e)) " with precedence 19
478 for @{ 'Not_elim_ok_2 $ab $a $b }.
479 interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b =
480 (cast _ _ (show b (Not_elim _ ab a))).
482 notation > "¬_'e' term 90 ab term 90 a" with precedence 19
483 for @{ 'Not_elim (show $ab ?) (show $a ?) }.
484 interpretation "Not_elim KO" 'Not_elim ab a =
485 (cast _ _ (Not_elim unit (cast _ _ ab) (cast _ _ a))).
486 interpretation "Not_elim OK" 'Not_elim ab a =
490 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
491 for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
492 interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn =
493 (show Pn (cast _ _ (Raa _ (cast _ _ Px)))).
495 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
496 for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
497 interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn =
498 (cast _ _ (show Pn (cast _ _ (Raa _ (cast _ _ Px))))).
500 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)) (\vdots)" with precedence 19
501 for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
502 interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn =
503 (show Pn (Raa _ Px)).
505 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (\RAA \emsp ident x)" with precedence 19
506 for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
507 interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn =
508 (cast _ _ (show Pn (Raa _ Px))).
510 notation > "'RAA' [ident H] term 90 b" with precedence 19
511 for @{ 'Raa (λ${ident H}.show $b ?) }.
512 interpretation "RAA KO" 'Raa p = (cast _ unit (Raa _ (cast _ (unit_to _) p))).
513 interpretation "RAA OK" 'Raa p = (Raa _ p).
516 notation < "\infrule hbox(\emsp Pn \emsp) Px mstyle color #ff0000 (∃\sub\i)" with precedence 19
517 for @{ 'Exists_intro_ko_1 $Pn $Px }.
518 interpretation "Exists_intro_ko_1" 'Exists_intro_ko_1 Pn Px =
519 (show Px (cast _ _ (Exists_intro _ _ _ (cast _ _ Pn)))).
521 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) mstyle color #ff0000 (∃\sub\i)" with precedence 19
522 for @{ 'Exists_intro_ko_2 $Pn $Px }.
523 interpretation "Exists_intro_ko_2" 'Exists_intro_ko_2 Pn Px =
524 (cast _ _ (show Px (cast _ _ (Exists_intro _ _ _ (cast _ _ Pn))))).
526 notation < "maction (\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)) (\vdots)" with precedence 19
527 for @{ 'Exists_intro_ok_1 $Pn $Px }.
528 interpretation "Exists_intro_ok_1" 'Exists_intro_ok_1 Pn Px =
529 (show Px (Exists_intro _ _ _ Pn)).
531 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) (∃\sub\i)" with precedence 19
532 for @{ 'Exists_intro_ok_2 $Pn $Px }.
533 interpretation "Exists_intro_ok_2" 'Exists_intro_ok_2 Pn Px =
534 (cast _ _ (show Px (Exists_intro _ _ _ Pn))).
536 notation >"∃_'i' {term 90 t} term 90 Pt" non associative with precedence 19
537 for @{'Exists_intro $t (λw.? w) (show $Pt ?)}.
538 interpretation "Exists_intro KO" 'Exists_intro t P Pt =
539 (cast _ _ (Exists_intro sort P t (cast _ _ Pt))).
540 interpretation "Exists_intro OK" 'Exists_intro t P Pt =
541 (Exists_intro sort P t Pt).
544 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
545 for @{ 'Exists_elim_ko_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
546 interpretation "Exists_elim_ko_1" 'Exists_elim_ko_1 ExPx Pc c =
547 (show c (cast _ _ (Exists_elim _ _ _ (cast _ _ ExPx) (cast _ _ Pc)))).
549 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
550 for @{ 'Exists_elim_ko_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
551 interpretation "Exists_elim_ko_2" 'Exists_elim_ko_2 ExPx Pc c =
552 (cast _ _ (show c (cast _ _ (Exists_elim _ _ _ (cast _ _ ExPx) (cast _ _ Pc))))).
554 notation < "maction (\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)) (\vdots)" with precedence 19
555 for @{ 'Exists_elim_ok_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
556 interpretation "Exists_elim_ok_1" 'Exists_elim_ok_1 ExPx Pc c =
557 (show c (Exists_elim _ _ _ ExPx Pc)).
559 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
560 for @{ 'Exists_elim_ok_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
561 interpretation "Exists_elim_ok_2" 'Exists_elim_ok_2 ExPx Pc c =
562 (cast _ _ (show c (Exists_elim _ _ _ ExPx Pc))).
564 definition ex_concl := λx:sort → CProp.∀y:sort.unit → x y.
565 definition ex_concl_dummy := ∀y:sort.unit → unit.
566 definition fake_pred := λx:sort.unit.
568 notation >"∃_'e' term 90 ExPt {ident t} [ident H] term 90 c" non associative with precedence 19
569 for @{'Exists_elim (λx.? x) (show $ExPt ?) (λ${ident t}:sort.λ${ident H}.show $c ?)}.
570 interpretation "Exists_elim KO" 'Exists_elim P ExPt c =
571 (cast _ _ (Exists_elim sort P _
572 (cast (Exists _ P) _ ExPt)
573 (cast ex_concl_dummy (ex_concl _) c))).
574 interpretation "Exists_elim OK" 'Exists_elim P ExPt c =
575 (Exists_elim sort P _ ExPt c).
579 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
580 for @{ 'Forall_intro_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
581 interpretation "Forall_intro_ko_1" 'Forall_intro_ko_1 Px Pn =
582 (show Pn (cast _ _ (Forall_intro _ _ (cast _ _ Px)))).
584 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
585 for @{ 'Forall_intro_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
586 interpretation "Forall_intro_ko_2" 'Forall_intro_ko_2 Px Pn =
587 (cast _ _ (show Pn (cast _ _ (Forall_intro _ _ (cast _ _ Px))))).
589 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)) (\vdots)" with precedence 19
590 for @{ 'Forall_intro_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
591 interpretation "Forall_intro_ok_1" 'Forall_intro_ok_1 Px Pn =
592 (show Pn (Forall_intro _ _ Px)).
594 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\i \emsp ident x)" with precedence 19
595 for @{ 'Forall_intro_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
596 interpretation "Forall_intro_ok_2" 'Forall_intro_ok_2 Px Pn =
597 (cast _ _ (show Pn (Forall_intro _ _ Px))).
599 notation > "∀_'i' {ident y} term 90 Px" non associative with precedence 19
600 for @{ 'Forall_intro (λ_.?) (λ${ident y}.show $Px ?) }.
601 interpretation "Forall_intro KO" 'Forall_intro P Px =
602 (cast _ _ (Forall_intro sort P (cast _ _ Px))).
603 interpretation "Forall_intro OK" 'Forall_intro P Px =
604 (Forall_intro sort P Px).
607 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\e))" with precedence 19
608 for @{ 'Forall_elim_ko_1 $Px $Pn }.
609 interpretation "Forall_elim_ko_1" 'Forall_elim_ko_1 Px Pn =
610 (show Pn (cast _ _ (Forall_elim _ _ _ (cast _ _ Px)))).
612 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\e))" with precedence 19
613 for @{ 'Forall_elim_ko_2 $Px $Pn }.
614 interpretation "Forall_elim_ko_2" 'Forall_elim_ko_2 Px Pn =
615 (cast _ _ (show Pn (cast _ _ (Forall_elim _ _ _ (cast _ _ Px))))).
617 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)) (\vdots)" with precedence 19
618 for @{ 'Forall_elim_ok_1 $Px $Pn }.
619 interpretation "Forall_elim_ok_1" 'Forall_elim_ok_1 Px Pn =
620 (show Pn (Forall_elim _ _ _ Px)).
622 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\e)" with precedence 19
623 for @{ 'Forall_elim_ok_2 $Px $Pn }.
624 interpretation "Forall_elim_ok_2" 'Forall_elim_ok_2 Px Pn =
625 (cast _ _ (show Pn (Forall_elim _ _ _ Px))).
627 notation > "∀_'e' {term 90 t} term 90 Pn" non associative with precedence 19
628 for @{ 'Forall_elim (λ_.?) $t (show $Pn ?) }.
629 interpretation "Forall_elim KO" 'Forall_elim P t Px =
630 (cast _ unit (Forall_elim sort P t (cast _ _ Px))).
631 interpretation "Forall_elim OK" 'Forall_elim P t Px =
632 (Forall_elim sort P t Px).
634 (* already proved lemma *)
635 definition hide_args : ∀A:Type.∀a:A.A := λA:Type.λa:A.a.
636 notation < "t" non associative with precedence 90 for @{'hide_args $t}.
637 interpretation "hide 0 args" 'hide_args t = (hide_args _ t).
638 interpretation "hide 1 args" 'hide_args t = (hide_args _ t _).
639 interpretation "hide 2 args" 'hide_args t = (hide_args _ t _ _).
640 interpretation "hide 3 args" 'hide_args t = (hide_args _ t _ _ _).
641 interpretation "hide 4 args" 'hide_args t = (hide_args _ t _ _ _ _).
642 interpretation "hide 5 args" 'hide_args t = (hide_args _ t _ _ _ _ _).
643 interpretation "hide 6 args" 'hide_args t = (hide_args _ t _ _ _ _ _ _).
644 interpretation "hide 7 args" 'hide_args t = (hide_args _ t _ _ _ _ _ _ _).
646 (* more args crashes the pattern matcher *)
648 (* already proved lemma, 0 assumptions *)
649 definition Lemma : ΠA.A→A ≝ λA:CProp.λa:A.a.
654 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
656 non associative with precedence 19
657 for @{ 'lemma_ko_1 $p ($H : $_) }.
658 interpretation "lemma_ko_1" 'lemma_ko_1 p H =
659 (show p (cast _ _ (Lemma _ (cast _ _ H)))).
664 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
665 mstyle color #ff0000 (p) \nbsp"
666 non associative with precedence 19
667 for @{ 'lemma_ko_2 $p ($H : $_) }.
668 interpretation "lemma_ko_2" 'lemma_ko_2 p H =
669 (cast _ _ (show p (cast _ _
670 (Lemma _ (cast _ _ H))))).
676 (╲ mstyle mathsize normal (H) ╱) \nbsp)
678 non associative with precedence 19
679 for @{ 'lemma_ok_1 $p ($H : $_) }.
680 interpretation "lemma_ok_1" 'lemma_ok_1 p H =
681 (show p (Lemma _ H)).
686 (╲ mstyle mathsize normal (H) ╱) \nbsp)
687 mstyle color #ff0000 (p) \nbsp"
688 non associative with precedence 19
689 for @{ 'lemma_ok_2 $p ($H : $_) }.
690 interpretation "lemma_ok_2" 'lemma_ok_2 p H =
691 (cast _ _ (show p (Lemma _ H))).
693 notation > "'lem' 0 term 90 l" non associative with precedence 19
694 for @{ 'Lemma (hide_args ? $l : ?) }.
695 interpretation "lemma KO" 'Lemma l =
696 (cast _ _ (Lemma unit (cast unit _ l))).
697 interpretation "lemma OK" 'Lemma l = (Lemma _ l).
700 (* already proved lemma, 1 assumption *)
701 definition Lemma1 : ΠA,B. (A ⇒ B) → A → B ≝
702 λA,B:CProp.λf:A⇒B.λa:A.
708 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
710 non associative with precedence 19
711 for @{ 'lemma1_ko_1 $a $p ($H : $_) }.
712 interpretation "lemma1_ko_1" 'lemma1_ko_1 a p H =
713 (show p (cast _ _ (Lemma1 _ _ (cast _ _ H) (cast _ _ a)))).
718 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
719 mstyle color #ff0000 (p) \nbsp"
720 non associative with precedence 19
721 for @{ 'lemma1_ko_2 $a $p ($H : $_) }.
722 interpretation "lemma1_ko_2" 'lemma1_ko_2 a p H =
723 (cast _ _ (show p (cast _ _
724 (Lemma1 _ _ (cast _ _ H) (cast _ _ a))))).
730 (╲ mstyle mathsize normal (H) ╱) \nbsp)
732 non associative with precedence 19
733 for @{ 'lemma1_ok_1 $a $p ($H : $_) }.
734 interpretation "lemma1_ok_1" 'lemma1_ok_1 a p H =
735 (show p (Lemma1 _ _ H a)).
740 (╲ mstyle mathsize normal (H) ╱) \nbsp)
741 mstyle color #ff0000 (p) \nbsp"
742 non associative with precedence 19
743 for @{ 'lemma1_ok_2 $a $p ($H : $_) }.
744 interpretation "lemma1_ok_2" 'lemma1_ok_2 a p H =
745 (cast _ _ (show p (Lemma1 _ _ H a))).
748 notation > "'lem' 1 term 90 l term 90 p" non associative with precedence 19
749 for @{ 'Lemma1 (hide_args ? $l : ?) (show $p ?) }.
750 interpretation "lemma 1 KO" 'Lemma1 l p =
751 (cast _ _ (Lemma1 unit unit (cast (Imply unit unit) _ l) (cast unit _ p))).
752 interpretation "lemma 1 OK" 'Lemma1 l p = (Lemma1 _ _ l p).
754 (* already proved lemma, 2 assumptions *)
755 definition Lemma2 : ΠA,B,C. (A ⇒ B ⇒ C) → A → B → C ≝
756 λA,B,C:CProp.λf:A⇒B⇒C.λa:A.λb:B.
757 Imply_elim B C (Imply_elim A (B⇒C) f a) b.
761 (\emsp a \emsp\emsp\emsp b \emsp)
762 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
764 non associative with precedence 19
765 for @{ 'lemma2_ko_1 $a $b $p ($H : $_) }.
766 interpretation "lemma2_ko_1" 'lemma2_ko_1 a b p H =
767 (show p (cast _ _ (Lemma2 _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b)))).
771 (\emsp a \emsp\emsp\emsp b \emsp)
772 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
773 mstyle color #ff0000 (p) \nbsp"
774 non associative with precedence 19
775 for @{ 'lemma2_ko_2 $a $b $p ($H : $_) }.
776 interpretation "lemma2_ko_2" 'lemma2_ko_2 a b p H =
777 (cast _ _ (show p (cast _ _
778 (Lemma2 _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b))))).
783 (\emsp a \emsp\emsp\emsp b \emsp)
784 (╲ mstyle mathsize normal (H) ╱) \nbsp)
786 non associative with precedence 19
787 for @{ 'lemma2_ok_1 $a $b $p ($H : $_) }.
788 interpretation "lemma2_ok_1" 'lemma2_ok_1 a b p H =
789 (show p (Lemma2 _ _ _ H a b)).
793 (\emsp a \emsp\emsp\emsp b \emsp)
794 (╲ mstyle mathsize normal (H) ╱) \nbsp)
795 mstyle color #ff0000 (p) \nbsp"
796 non associative with precedence 19
797 for @{ 'lemma2_ok_2 $a $b $p ($H : $_) }.
798 interpretation "lemma2_ok_2" 'lemma2_ok_2 a b p H =
799 (cast _ _ (show p (Lemma2 _ _ _ H a b))).
801 notation > "'lem' 2 term 90 l term 90 p term 90 q" non associative with precedence 19
802 for @{ 'Lemma2 (hide_args ? $l : ?) (show $p ?) (show $q ?) }.
803 interpretation "lemma 2 KO" 'Lemma2 l p q =
804 (cast _ _ (Lemma2 unit unit unit (cast (Imply unit (Imply unit unit)) _ l) (cast unit _ p) (cast unit _ q))).
805 interpretation "lemma 2 OK" 'Lemma2 l p q = (Lemma2 _ _ _ l p q).
807 (* already proved lemma, 3 assumptions *)
808 definition Lemma3 : ΠA,B,C,D. (A ⇒ B ⇒ C ⇒ D) → A → B → C → D ≝
809 λA,B,C,D:CProp.λf:A⇒B⇒C⇒D.λa:A.λb:B.λc:C.
810 Imply_elim C D (Imply_elim B (C⇒D) (Imply_elim A (B⇒C⇒D) f a) b) c.
814 (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
815 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
817 non associative with precedence 19
818 for @{ 'lemma3_ko_1 $a $b $c $p ($H : $_) }.
819 interpretation "lemma3_ko_1" 'lemma3_ko_1 a b c p H =
821 (Lemma3 _ _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b) (cast _ _ c)))).
825 (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
826 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
827 mstyle color #ff0000 (p) \nbsp"
828 non associative with precedence 19
829 for @{ 'lemma3_ko_2 $a $b $c $p ($H : $_) }.
830 interpretation "lemma3_ko_2" 'lemma3_ko_2 a b c p H =
831 (cast _ _ (show p (cast _ _
832 (Lemma3 _ _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b) (cast _ _ c))))).
837 (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
838 (╲ mstyle mathsize normal (H) ╱) \nbsp)
840 non associative with precedence 19
841 for @{ 'lemma3_ok_1 $a $b $c $p ($H : $_) }.
842 interpretation "lemma3_ok_1" 'lemma3_ok_1 a b c p H =
843 (show p (Lemma3 _ _ _ _ H a b c)).
847 (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
848 (╲ mstyle mathsize normal (H) ╱) \nbsp)
849 mstyle color #ff0000 (p) \nbsp"
850 non associative with precedence 19
851 for @{ 'lemma3_ok_2 $a $b $c $p ($H : $_) }.
852 interpretation "lemma3_ok_2" 'lemma3_ok_2 a b c p H =
853 (cast _ _ (show p (Lemma3 _ _ _ _ H a b c))).
855 notation > "'lem' 3 term 90 l term 90 p term 90 q term 90 r" non associative with precedence 19
856 for @{ 'Lemma3 (hide_args ? $l : ?) (show $p ?) (show $q ?) (show $r ?) }.
857 interpretation "lemma 3 KO" 'Lemma3 l p q r =
858 (cast _ _ (Lemma3 unit unit unit unit (cast (Imply unit (Imply unit (Imply unit unit))) _ l) (cast unit _ p) (cast unit _ q) (cast unit _ r))).
859 interpretation "lemma 3 OK" 'Lemma3 l p q r = (Lemma3 _ _ _ _ l p q r).