command to unpack an existential with classical.some

[robertylewis]

I've recently found myself repeating this pattern a bunch:

lemma it_exists (a b c d) : ∃ x : T, property x :=
long proof

def it (a b c d) : T := classical.some (it_exists a b c d)

lemma it_spec (a b c d) : property (it a b c d) := classical.some_spec (it_exists a b c d)

It would be relatively easy to write a metaprogram that automatically generates it and it_spec from it_exists. This could be run with an atribute on it_exists and/or a command afterward:

@[make_a_thing it it_spec]
lemma it_exists (a b c d) : ∃ x : T, property x :=
long proof

lemma it_exists (a b c d) : ∃ x : T, property x :=
long proof

make_a_thing it_exists it it_spec

Note: the type of it_spec is defeq, but not syntactically equal, to the type of classical.some_spec (it_exists a b c d).

[fpvandoorn]

If I can extend your feature request: it would be nice if it could also deal with statements like ∃ (x : T) (y : S), P x y ∧ Q y x and make more than 2 declarations (in this case 4).

[fpvandoorn]

Note: the implementation of tactic.choose is very likely to be helpful to implement this.

[ericrbg]

@fpvandoorn what declarations would you expect it to make? I feel like I'm missing something fairly obvious here

[fpvandoorn]

If I prove it_exists : (list_of_variables : list_of_types) : ∃ (x : T) (y : S), P x y ∧ Q y x I want something like the following (probably with customizable names)

def it1 (l : _) : T := classical.some $ it_exists l
def it2 (l : _) : S := classical.some $ classical.some_spec $ it_exists l
lemma it_spec1 (l : _) : P (it1 l) (it2 l) := (classical.some_spec $ classical.some_spec $ it_exists l).1
lemma it_spec2 (l : _) : Q (it2 l) (it1 l) := (classical.some_spec $ classical.some_spec $ it_exists l).2

Here is an example where that would be useful (though in that code I also did some other things that weren't purely "use classical.some[_spec]")

[0x182d4454fb211940]

I have an implementation. Do I need to ask on zulip to open a PR?

[fpvandoorn]

I sent you an invitation so that you can push to a branch of mathlib. Please read https://leanprover-community.github.io/contribute/index.html and open an PR.