Zulip Chat Archive

Stream: new members

Topic: Exists witness in a def

Cayden Codel (Nov 16 2021 at 21:39):

I'm trying to code up and prove things about a more general function (think on a general type u rather than on nats), but my first pass seems to require that I use the witness of an exists hypothesis in the def, which Lean doesn't seem to like. Here's a MWE that produces the error.

lemma exists_not_mem (l : list nat) :  (n : nat), n  l := begin ... end

def cons_not_mem : list nat  list nat
| [] := [1]
| l := have exi :  (n : nat), n  l, from exists_not_mem l,
    exi.w :: l

In cons_not_mem, Lean complains that Exists.w is an unknown. Is there a way to use exi in the def? Or must I try a different route?

Kevin Buzzard (Nov 16 2021 at 21:42):

You need to use classical.some exi because constructively Exists only eliminates into Prop

Kevin Buzzard (Nov 16 2021 at 21:43):

And then classical.some_spec exi is the proof that n is not in l

Cayden Codel (Nov 16 2021 at 21:44):

Great, that's exactly what I needed. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC