5

TL;DR: Are there any coding conventions for the Isar language? Is it necessary to respect jEdit's folding strategy?

My team is working on the formalization of mathematics, so one of our main purposes is to obtain readable proofs. Looking into that, we tried to code proofs in a way that intermediate facts (and labels, if any) stand out:

from fact1 have
  1: "Foo"
  using Thm1 Thm2 by auto
then have
  2: "Bar = FooBar"
  by simp
also from 1 have
  " ... = BarFoo"
  by blast

etc. Apart from the fact that sometimes this produces a proliferation of "short lines" (btw, I don't know if this is really a problem), it is somehow not compatible with jEdit folding strategy; after folding, the previous code block would look like this:

from fact1 have
then have
also from 1 have

completely obscuring the argument. The following format perhaps is better:

from fact1
have 1: "Foo"
  using Thm1 Thm2 by auto
then 
have 2: "Bar = FooBar"
  by simp
also from 1 
have " ... = BarFoo"
  by blast

And, after folding,

from fact1
have 1: "Foo"
then 
have 2: "Bar = FooBar"
also from 1 
have " ... = BarFoo"

which makes the flow of the argument explicit.

In any case, before I come up with 5 new formatting conventions, I'd definitely like to know if there is some de facto standard, or at least if someone thought about this.

Pedro Sánchez Terraf
  • 231
  • 1
  • 7
  • 4
    Well, there is this: https://proofcraft.org/blog/isabelle-style.html – Manuel Eberl Feb 16 '19 at 17:47
  • 2
    Other than that I don't really know. I usually make a line break to separate the statement from the method used to prove it; apart from that, I only make line breaks when the lines get too long. I also don't think I've seen many people actually use jEdit's folding. I certainly don't, although it might actually be useful. It's just not in my workflow somehow. – Manuel Eberl Feb 16 '19 at 17:49
  • 3
    I’m not aware of a syntax style guide either. We’re thinking of writing one, along the lines of what you have under ‘the following format perhaps is better’, but it will take a while to come out. It’s usually a good idea to not fight jedit, and to go with what works well with folding, default indentation etc, which still leaves a lot of freedom. – lsf37 Feb 16 '19 at 20:09
  • 1
    Thank you both for your comments. Both count as upvotable answers to me. – Pedro Sánchez Terraf Feb 16 '19 at 22:58
  • 1
    @lsf37 another idea going around, implicit in the examples above, is first to quote local facts (from, with) and later theorems and lemmas (using). I believe this also contributes to readability. – Pedro Sánchez Terraf Feb 16 '19 at 23:02

0 Answers0