## Stream: general

### Topic: Getting witnesses used in existential proofs?

#### 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⟩


#### Johan Commelin (May 05 2020 at 11:03):

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

#### Johan Commelin (May 05 2020 at 11:11):

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

#### Chris Hughes (May 05 2020 at 11:11):

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

#### Johan Commelin (May 05 2020 at 11:12):

Aah, of course

Last updated: May 15 2021 at 00:39 UTC