Email Gateway (Aug 22 2022 at 16:03): Email Gateway (Aug 22 2022 at 16:03):From: "C. Diekmann" <diekmann@in.tum.de>
Dear Makarius,
I experienced some unexpected behavior of the automatic indentation when
used together with the subgoal command.
Here is a minimal example where the auto indenter does great work:
lemma "A ⟹ B ⟹ A ∧ B"
apply(rule conjI)
apply(simp)
by(assumption)
After the conjI rule is applied, we have two subgoals and the following
simp is indented by one additional space. This is how it should be. If I
want to specifically indicate that simp solves the subgoal, I can use the
subgoal command. This is what the auto indenter gives me:
lemma "A ⟹ B ⟹ A ∧ B"
apply(rule conjI)
subgoal by (simp)
by(assumption)
The "subgoal by (simp)"-step does not get indented. I don't know if this is
the expected behavior, but I would expect the following:
lemma "A ⟹ B ⟹ A ∧ B"
apply(rule conjI)
subgoal by (simp)
by(assumption)
This report is not about simp. For this particular example, I could use the
apply(simp; fail) pattern, which the indenter handles fine. This report is
about -- from my point of view -- a bad interaction of the indenter and the
subgoal command.
This is what the indenter does if the subgoal is solved by a longer apply
script:
lemma "A ⟹ B ⟹ A ∧ B"
apply(rule conjI)
subgoal apply -
apply -
apply(insert TrueI)
apply blast
done
by(assumption)
My points of criticism are:
the first line where subgoal appears is not additionally indented,
though the previous line produced a new subgoal.
The apply script of the subgoal is indented by two additional spaces,
though no new subgoals appeared.
Best Regards,
Cornelius
Email Gateway (Aug 22 2022 at 16:03):From: Makarius <makarius@sketis.net>
The idea behind this: 'subgoal' enforces a certain structure on its own,
and extra indentation is not required to indicate that in the text: it
always solves one subgoal and always requires a complete subproof. Thus
it is the analogue of 'show'. For example:
lemma A B C
proof -
show A \<proof>
show B \<proof>
show C \<proof>
qed
lemma A B C
subgoal A \<proof>
subgoal B \<proof>
subgoal C \<proof>
done
At least that is the idea from some years ago, when subgoal emerged as
spin-off from Eisbach. Since it is relatively new, it might require
further iterations of refinement, but that requires some real-world
examples to look at. (So far I've done this sporadically in various
library sessions, using the above scheme.)
Apropos 'using' (as a command): it is always indented like a structured
command, even though it might float freely within an apply script and
thus would require the same indentation as 'apply'. Luckily, we no
longer need that and may use the "use" proof method instead:
using facts apply method
becomes:
apply (use facts in method)
Makarius
Email Gateway (Aug 22 2022 at 16:09):From: Gerwin.Klein@data61.csiro.au
As a an additional data point (maybe not for this release any more):
We do have some large apply scripts that use subgoal to good advantage, and in those an indentation similar to apply would work quite well. That use is slightly different to the originally intended analogy to "show", but still has some connection:
For instance, we have things like:
lemma X
apply ..
apply ..
apply ..
subgoal
by ...
subgoal
apply ..
apply ..
done
apply ..
...
The current auto indent would turn this into
lemma X
apply ..
apply ..
apply ..
subgoal
by ...
subgoal
apply ..
apply ..
done
apply ..
which is a bit jarring and confers less information to the reader.
Cheers,
Gerwin
Last updated: Apr 27 2024 at 04:17 UTC