Zulip Chat Archive

Stream: new members

Topic: Witness of existential hypothesis


Chase Norman (Oct 10 2020 at 23:17):

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 (Oct 10 2020 at 23:18):

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 (Oct 10 2020 at 23:19):

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

Heather Macbeth (Oct 10 2020 at 23:19):

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 (Oct 10 2020 at 23:21):

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 (Oct 10 2020 at 23:21):

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

Chase Norman (Oct 10 2020 at 23:25):

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

Chase Norman (Oct 17 2020 at 04:23):

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 (Oct 17 2020 at 04:38):

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 (Oct 17 2020 at 04:38):

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 (Oct 17 2020 at 04:46):

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 (Oct 26 2020 at 23:48):

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'.


Last updated: Dec 20 2023 at 11:08 UTC