Getting witnesses used in existential proofs?

Stream: general

[Gabriel Ebner]

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⟩

[Johan Commelin]

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

[Johan Commelin]

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

[Chris Hughes]

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

[Johan Commelin]

Aah, of course