Gerwin's Style Guide for Isabelle/HOL. Part 1: Good Proofs.

The dos and don’ts of Isabelle proofs: guidelines for making your proofs more readable, maintainable and enjoyable.

With examples and rationale.

This is Part 1 of my personal style guide for Isabelle/HOL. Part 1 is about content and how to keep proofs maintainable. More requirements than style, really. Part 2 is about good style and advanced rules, and part 3 will be about layout and looks.

Most of these guidelines encode what is followed in the Isabelle distribution. Such rules used to be less enforced in the Archive Of Formal Proofs, but will be more so in the future to keep it maintainable over time. These guidelines are also used to various degrees in some of the large proofs of the L4.verified project, at least on good days. You can observe there how messy it can get when they are not.

Always Do

This first set of rules, you should always follow. At least, if you ever intend to show your proofs to somebody else. Obviously, they are Ok to break in interactive use and proof search, but proofs that break these rules would not be accepted at the Archive Of Formal Proofs.

Do not use sorry

Should go without saying that your proofs should be finished before you call them proofs, but it’s worth checking if you forgot one somewhere.

You should not leave old experiments sitting around as sorry lemmas. Use oops to make sure they are not used accidentally, or make them explicit assumption of a locale if you need them, but do not intend to prove them.
Do not use back

This command single-steps Isabelle’s backtracking mechanism. It is occasionally nice for debugging low-level rule applications, but it can be a real headache for maintenance, because backtracking occurs over many different places in Isabelle and its internal order can change. When it does change, it can be very hard to figure out what the proof script was trying to achieve. It should always be eliminated in final proofs, either by using implicit backtracking or by using explicit instantiations.

Bad:
```
apply (erule allE) back back
apply (erule impE) back
 apply assumption
apply clarsimp
...
```
Good:
```
apply (erule allE, erule (1) impE)
apply clarsimp
...
```
Also Ok, but neater if you don’t need to instantiate:
```
apply (erule allE [where x="37"])
apply (erule (1) impE)
apply clarsimp
...
```
Indent apply scripts by subgoal.

If an apply command is applied to a state with n+1 subgoals, it must be indented by n spaces relative to the first apply in the sequence (see the Isabelle distribution for many examples). This indicates textually which line solved a subgoal and how many new subgoals where generated. Invaluable information when something goes wrong because something changed somewhere. Also, it gives a nice visual indication of the nesting depth of your proof.

The usual indentation for 0 subgoals is 2 spaces for a top-level proof.

There is an experimental bean shell macro available for jEdit that will indent apply scripts by subgoal.

Bad:
```
  apply (erule impE)
apply (clarsimp split: split_if_asm)
apply assumption
apply fastforce
apply simp
apply clarsimp
apply fastforce
...
```
Good:
```
apply (erule impE)
 apply (clarsimp split: split_if_asm)
   apply assumption
  apply fastforce
 apply simp
 apply clarsimp
apply fastforce
...
```
In the bad version, it is impossible to tell which of the simp and clarsimp tactics were supposed to solve a goal, and how many new subgoals the (clarsimp split: split_if_asm) produced. In the good version, it is easy to see.

From Isabelle2015 it will be easy to indicate that a tactic should solve its goal. This is not mandatory, but often a good idea. It will be covered in Part 2 of the style guide, but it does not absolve you from indentation.
Never give an unnamed lemma a global attribute for automated methods

Bad:
```
lemma [simp]: "(A ∧ B) = (B ∧ A)"
```
It is much too hard to remove such lemmas from the (in this case) simp set again. Instead, give the lemma a name.

Good Reasons

This second set of rules will make your life easier down the track, in maintenance and readability. There can be good reasons for exceptions, but you should know what you are doing when you are breaking them. The AFP makes some of these mandatory.

Instantiations must not use Isabelle-generated names such as xa.

These names change as Isabelle releases go by (in Isabelle2015, for instance, names generated by the datatype command changed drastically). When that has happened, trying to figure out what ba17 meant can drive the strongest mind insane. Use Isar or rename_tac to avoid such names.

Bad:
```
apply (cases n)
apply clarsimp
apply (rule_tac x="ba17" in exI)
```
Good:
```
apply (cases n)
apply (rename_tac x y)
apply clarsimp
apply (rule_tac x="x" in exI)
```
rename_tac works from right to left, so if the goal shows the parameters ⋀a b xa., apply (rename_tac x y) will change them to ⋀a x y.. The idea is that new names are introduced on the right and that it is more likely that you will want to rename something new.

Better:
```
proof (cases n)
  fix x y
  assume "P x y"
  have "Q x" by clarsimp
  thus ?thesis ..
qed
```
Do not use axiomatization

This command can introduce inconsistency into the logic. While you may not knowingly make use of any introduced inconsistency, automated tools may do so on your behalf. Unless you are bootstrapping a new logic in Isabelle or are extending the basic axioms of Higher-Order Logic, you should use safer commands such as locale instead, or use explicit assumptions.

If the axiomatization command is not used to state any properties, but to merely introduce the existence of a constant, it is safe to use.

Bad:
```
axiomatization
  P :: "'a ⇒ bool"
where
  all_true: "∀x. P x" and
  all_false: "∀x. ¬P x"
```
Ok:
```
axiomatization P :: "'a ⇒ bool"
```
The second example only states that a P of type 'a => bool exists, which is safe in HOL, because all types are inhabited.
If there are proof steps that take significant time, i.e. longer than roughly 1 min, add a short comment to that step.

If you maintain these proofs in the future you will know what to expect instead of wondering whether something broke. Proof maintainers are impatient people.

Good:
```
by (auto simp: some_rule split: split_if_asm)  (* takes long *)
```
In Isar proofs, it is better to use by for long-running terminal proof methods, because by is run asynchronously (so you can continue working), whereas apply is not.
Use unrestricted auto only as a terminal proof method

auto works on all subgoals simultaneously and when its internal composition changes, it is very hard to tell what the resulting proof state used to be. It’s perfectly fine if the resulting proof state is documented, for instance in a structured proof, or when auto solves its goals completely, e.g. as terminal proof method.

Bad:
```
apply (auto simp: some_rules)
  apply (clarsimp simp: x)
 apply (rule_tac x="xa" in exI, simp)
...
```
Good:
```
apply (auto simp: some_rules x)
done
```
Also Good:
```
apply ...
  apply (auto simp: some_rules)[2]
apply ...
done
```
In the example above, auto is restricted to 2 goals, and solves them.

In general, most proof methods in Isabelle work on a single goal, and don’t have that potentially globally devastating effect of auto. Consider replacing an initial auto with a more predictable clarsimp or similar tactics. Then potentially use auto in goal-restricted form, e.g. apply (auto: ..)[n] to solve subgoals that the unconstrained initial auto would have solved, but clarsimp didn’t.

Larry Paulson points out that the initial purpose of auto was to be used at the start of proofs to solve the easy parts of the problem and leave over the difficult ones. He also has a solution: use auto to start the proof, but regard the resulting subgoals as separate lemmas that need to be proved first. Combining these proved lemmas with “auto” should solve the problem outright, and you have created a structured proof.
Do not switch from apply into proof in the middle of a proof

In proofs such as the following

Bad:
```
apply clarsimp
apply (rule my_rule)
 apply (fastforce simp: foo)
proof safe
  fix new
  assume "something surpising"
  show "unforeseen"
  ...
```
it is very hard for the reader to tell what is going on without running Isabelle, and the proof will break if the output of the initial apply script changes even slightly.

It is easier on the eye to use apply inside a structured proof, i.e. to turn the proof around.

(Somewhat) better:
```
proof -
  { fix new
    assume "something surprising"
    have "unforeseen"
    ...
  } note 1 = this

  show ?thesis
    apply clarsimp
    apply (rule my_rule)
     apply (fastforce simp: foo)
    apply safe
    apply (rule 1)
    done
```
This at least has some chance against small changes in the outcome of the apply script, and you may be able to compress the final apply sequence into a single method invocation such as by (auto simp: foo intro: my_rule 1).

Even better would be a fully structured proof that breaks up the apply part into readable fragments, or at least those initial parts of the proof.

Keep initial proof methods simple in structured proofs

Bad:

proof (auto simp: complex_rule intro!: more_complex_rule)
  fix x y
  assume "Q x"
  show "P x y"
...

This makes it hard for the reader to figure out how the rest of the proof connects. There can be exceptions to this rule, especially when the outcome of the complex method is simple.

Instead, keep the initial proof method simple. Do less there, and shift work into the show ?thesis part of the proof.

Better:

proof -
  { fix x y
    assume "Q x"
    have "P x y"
  }
  thus ?thesis by (auto simp: complex_rule intro!: more_complex_rule)
qed

Or potentially possible:

proof (rule more_complex_rule)
  fix x y
  assume "Q' x"
  have "P' x y"
  thus ?thesis by (auto simp: complex_rule)
qed

Do not use the implicit apply rule

Bad
```
apply rule
 apply rule
 apply rule
 apply clarsimp
```
When you’re writing it, the rule Isabelle picks will make perfect sense to you, and when that rule changes in two years, you will have no idea which one it was and what it was called.

Good
```
apply (rule conjI)
 apply (rule ballI)
 apply (rule exI)
 apply clarsimp
```
Ok to use in an Isar proof block where the rest of the text statically makes clear what is going on. For example:

Good
```
lemma "A ∧ B"
proof
   show "A"
   ...
next
   show "B"
   ....
```
The proof without arguments in this example is equivalent to proof rule, which does the same thing as apply rule.

This concludes part 1 of my style guide for Isabelle/HOL.

If you have feedback, strong opinions, or just liked what you read, get in touch by email or if you think it is of wider interest, even on the isabelle-users mailing list (subscribe here). I might even update this style guide based on feedback.

Read on for Part 2 with more advanced material.

[24 May 2015: updated with feedback from Daniel Matichuk and Lars Noschinski]
[25 May 2015: updated with feedback from Peter Gammie]
[29 May 2015: updated with feedback from Larry Paulson]
[04 Aug 2019: removed no-smt, because failures are so rare that even the AFP now allows it]

Posted by Gerwin Klein on May 23, 2015.

Follow @lsf37

proofcraft.org