Witness of existential hypothesis

Stream: new members

[Chase Norman]

I have a hypothesis with an existential statement. What tactic can I use to generate a witness for this?

Also my proof is a proof by contradiction - is it normal to have the goal be just "false" for the entirety of the proof? It's making it hard to use tools like library_search, hint, etc. How do you discover the tactics you need to prove something?

[Heather Macbeth]

Chase Norman said:

I have a hypothesis with an existential statement. What tactic can I use to generate a witness for this?

Try cases (basic), or obtain (advanced).

[Adam Topaz]

rcases should be mentioned too if you have more things to split up, and because it's awesome!

[Heather Macbeth]

Chase Norman said:

Also my proof is a proof by contradiction - is it normal to have the goal be just "false" for the entirety of the proof? It's making it hard to use tools like library_search, hint, etc. How do you discover the tactics you need to prove something?

Yes, it's normal (but as you note, makes things tricky). If you have in mind proving both P and ¬P for some P, try setting up have statements for each of these (and then working on these subgoals).

[Kevin Buzzard]

Even if the goal is false and you're in the middle of a long proof, you can still use library_search. Say you're convinced that various hypotheses you have should imply some proposition P using just one result in the library. Then you can write have hP : P, library_search,

[Kevin Buzzard]

The have creates a new goal and subsequent tactics work on that new goal

[Chase Norman]

Thank you so much for these pieces of advice, they are all incredibly useful!

[Chase Norman]

This failed for me on a more complex example.

d: ∃ (x : ℕ) (H : x ∈ finset.Ico 0 (c.length - 1)), ∀ (x' : ℕ), x' ∈ finset.Ico 0 (c.length - 1) → (λ (x : ℕ), margin_graph P (c.nth_le x _) (c.nth_le (x + 1) _)) x ≤ (λ (x : ℕ), margin_graph P (c.nth_le x _) (c.nth_le (x + 1) _)) x' := a b
⊢ false

was my hypothesis and goal. I ran cases d:

d_w: ℕ
d_h: ∃ (H : d_w ∈ finset.Ico 0 (c.length - 1)), ∀ (x' : ℕ), x' ∈ finset.Ico 0 (c.length - 1) → (λ (x : ℕ), margin_graph P (c.nth_le x _) (c.nth_le (x + 1) _)) d_w ≤ (λ (x : ℕ), margin_graph P (c.nth_le x _) (c.nth_le (x + 1) _)) x'
⊢ (let d : ∃ (x : ℕ) (H : x ∈ finset.Ico 0 (c.length - 1)), ∀ (x' : ℕ), x' ∈ finset.Ico 0 (c.length - 1) → (λ (x : ℕ), margin_graph P (c.nth_le x sorry) (c.nth_le (x + 1) sorry)) x ≤ (λ (x : ℕ), margin_graph P (c.nth_le x sorry) (c.nth_le (x + 1) sorry)) x' := a b in false) (Exists.intro d_w d_h)

as you can see, it modified my goal. How do I achieve a witness of what d provides?

[Kyle Miller]

In this case, I think it would be helpful to see a #mwe if you could create one. I'm guessing you have some dependencies between hypotheses of some kind. (Answering your direct question, d.1 might give you a witness. Does let x := d.1 work, or does it cause an error?)

[Alex J. Best]

d is a proposition, so there shouldn't be a := at the end, did you do let d := blah at some point instead of have d := blah?

[Chase Norman]

Alex J. Best said:

d is a proposition, so there shouldn't be a := at the end, did you do let d := blah at some point instead of have d := blah?

Yeah, this is exactly what I did. Thanks so much.

[Jeff Petkau]

Try cases (basic)

Aha! I came here because I was stuck on inequality world 5/17. There's no documentation (at least up to that point) of how to do anything with an existential hypothesis, and searching the lean docs doesn't help because of the differences in the numbers game syntax. I was looking for a way to use the existential eliminator. I tried all the things I could think of, but did not try 'cases'.