extract_goal when the goal is False

Stream: mathlib4

[Bhavik Mehta]

It is useful that extract_goal tries to remove irrelevant hypotheses, except in the case where I'm in a contradiction proof and the goal is False, in which case it gives me something entirely useless. Would it be sensible for extract_goal to behave like extract_goal* in the case where the goal is (syntactically equal to) False?

[Kyle Miller]

That's funny how useless it is for contradiction proofs. That seems reasonable to me, and I'll make a PR

[Bhavik Mehta]

Thanks!

[Kyle Miller]

#8250

[Junyan Xu]

I suppose you could also manually revert some relevant hypotheses before extract_goal?

[Kyle Miller]

Indeed, and that would turn this False feature off and go back to the old behavior. Maybe the documentation should suggest this.

[Kyle Miller]

extract_goal could also take a with clause of hypotheses to definitely include.

[Bhavik Mehta]

Yeah this would be nice, and * would then carry the same meaning as it does in simp: include everything, not just the ones I told you to include

[Yaël Dillies]

Could we change the syntax to extract_goal with * so that the analogy is perfect?

[Kyle Miller]

I've updated the PR with this new feature. Here's an excerpt from the PR description:

changes the extract_goal syntax to

"extract_goal" ("*" <|> ident*) ("using" ident)?

The "using" clause replaces the autogenerated name for the extracted theorem/def. The extract_goal tactic has the same behavior as before, extract_goal * extracts the entire local context like before, and extract_goal a b c ... removes everything from the local context except for fvars a, b, c, ... and their (and the goal's) dependencies. This last form does not automatically include prop variables that depend on preserved fvars, unlike extract_goal, which does. The thought is that including prop variables is useful in the default case, but if you are configuring which variables to take you can always take them manually.

[Kyle Miller]

#8250 is still open, if any meta enthusiasts want to take a look

[Patrick Massot]

Among the tests I see nothing that seem to check there is no missing withContext or instantiateMvar.