Zulip Chat Archive

Stream: general

Topic: Getting witnesses used in existential proofs?


view this post on Zulip Gabriel Ebner (May 05 2020 at 10:43):

Johan Commelin said:

So secretly we could actually pull of the mathematicians trick of "by the object constructed in the proof of Theorem 5.4"...

For those who haven't been following the PR review thread, you can actually extract the witnesses used in proofs of existential statements (without metaprogramming):

structure g {α} {p : α  Prop} (h :  a, p a) := mk ( ).
def f {α} {p : α  Prop} {a : α} {h : p a} (x : g a, h) : α := a

lemma l :  n : , n = n := 42, rfl
-- prints witness 42 used in proof l
#eval show , from f l

view this post on Zulip Johan Commelin (May 05 2020 at 11:03):

But some time in the future, this should no longer work in lean

view this post on Zulip Johan Commelin (May 05 2020 at 11:11):

Soo, why can't I use this to prove that 37 = 42?

view this post on Zulip Chris Hughes (May 05 2020 at 11:11):

Because 42 is an argument to f, just an implicit one

view this post on Zulip Johan Commelin (May 05 2020 at 11:12):

Aah, of course


Last updated: May 15 2021 at 00:39 UTC