Zulip Chat Archive

Stream: new members

Topic: proving conjunction


view this post on Zulip Michael Beeson (Feb 24 2021 at 15:08):

Say my goal is A \and B. So I split, and give a long proof of A, and in the course of proving A I prove B. Now I finish the
first branch of my split and I would like to say, OK I'm done now because I already proved B. But that environment is gone.
What's the right way to do this?

view this post on Zulip Eric Wieser (Feb 24 2021 at 15:10):

start off with have : B := ...?

view this post on Zulip Michael Beeson (Feb 24 2021 at 15:12):

If I start with have:B :=
then once I've proved B, that environment will close, and I'll have to repeat the proof of B in order to continue with the proof of A.

view this post on Zulip Michael Beeson (Feb 24 2021 at 15:12):

T

view this post on Zulip Eric Wieser (Feb 24 2021 at 15:13):

Can you give a #mwe?

view this post on Zulip Eric Wieser (Feb 24 2021 at 15:13):

As long as you do the have before the split, then you can use it in both sides

view this post on Zulip Michael Beeson (Feb 24 2021 at 15:14):

I can't just move the split down to where B is deduced because there are a lot of rewrites of the goal above that point.

view this post on Zulip Eric Wieser (Feb 24 2021 at 15:14):

Rewrites will work on an and

view this post on Zulip Eric Wieser (Feb 24 2021 at 15:15):

Although apply will not do what you want

view this post on Zulip Michael Beeson (Feb 24 2021 at 15:16):

The rewrites will mess up the form of B. That might be OK, or work-aroundable, in a specific instance, but I thought maybe there is a standard, normal way to do this. If it requires a MWE to understand the question then it's clearly not the case that there's a standard way to do it that everybody but me already knows.

view this post on Zulip Michael Beeson (Feb 24 2021 at 15:17):

e.g. some command that says "export this result out of the split".

view this post on Zulip Eric Wieser (Feb 24 2021 at 15:20):

Any result that you were able to prove inside one branch of a split could have been proved before you entered the split at all

view this post on Zulip Eric Wieser (Feb 24 2021 at 15:21):

I'm asking for a #mwe because this feels like an #xy problem.

view this post on Zulip Ruben Van de Velde (Feb 24 2021 at 15:47):

You have goal A \and B, and you're doing split, have : B := ..., { prove A from B }, right? Move the have : B := ... bit before the split

view this post on Zulip Mario Carneiro (Feb 25 2021 at 01:56):

Michael Beeson said:

The rewrites will mess up the form of B. That might be OK, or work-aroundable, in a specific instance, but I thought maybe there is a standard, normal way to do this. If it requires a MWE to understand the question then it's clearly not the case that there's a standard way to do it that everybody but me already knows.

The point of the #mwe is to show a version of the problem you are talking about with the necessary features. It can be all foos and bars, it doesn't have to be your real example, but it's a lot easier to understand the exact situation and demonstrate a fix on a concrete problem rather than a prose description of one


Last updated: May 11 2021 at 13:22 UTC