Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Auto-indenter and "subgoal"

Email Gateway (Dec 02 2022 at 08:30):

From: Tobias Nipkow <nipkow@in.tum.de>
In an apply script, the auto-indenter tries to indicate the nesting of subgoals.
But the subgoal command seems to disturb that:

lemma assumes P Q R shows "(P & Q) & R"
apply(rule conjI)
apply(rule conjI)
subgoal
apply(fact ‹P›)
done
subgoal
apply(fact ‹Q›)
done
subgoal
apply(fact ‹R›)
done
done

The first subgoal is exdented and all three subgoals look like they are on the
same level. I (probably) understand why this happens, but could it be improved?

Tobias
smime.p7s

Email Gateway (Dec 02 2022 at 10:16):

From: Peter Lammich <lammich@in.tum.de>
I think that the indentation of subgoals (as well as the whole
indentation style) is pretty subjective.

IMHO, a proof structure like

subgoal by ...
subgoal by ...
subgoal by ...
done

clearly indicates that there are 3 subgoals, that are solved one after
the other. No need for indentation.

Indenting would be be similar to indenting the following:

proof (cases)
case 1 thus ?case by auto
next
case 2 thus ?case by auto
next
case 3 thus ?case by auto
qed

Email Gateway (Dec 06 2022 at 08:21):

From: Gerwin Klein <kleing@unsw.edu.au>

On 2 Dec 2022, at 21:15, Peter Lammich <lammich@in.tum.de> wrote:
I think that the indentation of subgoals (as well as the whole indentation style) is pretty subjective.

Sure is, otherwise there'd be no need to talk about it. But: whatever it is, it should be consistent, and what Tobias showed clearly is not consistent with existing practice.

IMHO, a proof structure like
subgoal by ...
subgoal by ...
subgoal by ...
done

clearly indicates that there are 3 subgoals, that are solved one after the other. No need for indentation.

Neither would there be in an apply script that is

apply fastforce
apply fastforce
apply fastforce

yet we do still want to indent it. Why? Because it doesn't make sense to indent one part of a script one way and another part of the same script another way.

You also conveniently left out the part that is the actual problem. Namely the rest of indentation in the middle of an apply script that Tobias showed:

apply(rule conjI)
apply(rule conjI)
apply(rule conjI)
subgoal by ...
apply fastforce

This is clearly inconsistent.

In the middle of a script you do not know how many subgoals there are if you don't indent, you just know how many subgoal commands you have used.

To come back to the example of 3 subgoals: in a proof with 3 subgoals it doesn't matter much what you do anyway. Try a proof with 12 subgoals. Do you really want to say that we should count those manually? I have not seen any serious proofs that do that. I don't wonder why.

Indenting would be be similar to indenting the following:
proof (cases)
case 1 thus ?case by auto
next
case 2 thus ?case by auto
next
case 3 thus ?case by auto
qed

This is a strawman argument. Nobody is suggesting that Isar-style indentation needs adjustment and Tobias has not suggested that apply-style indentation has any problems. He is merely pointing out that the subgoal command should use the apply-style indentation, not the structured proof indentation, because apply scripts are where the subgoal command is used.

And I strong agree.

Cheers,
Gerwin

Last updated: Apr 26 2024 at 04:17 UTC