lh-l4v/docs/compacting-proofs.md

<!--
     Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)

     SPDX-License-Identifier: CC-BY-SA-4.0
-->

# Compacting proofs

Not all proofs are equal. After finishing a proof (especially a long, tricky
one), look over the proof and try to *compact* it. This includes

- removing or refactoring redundant steps; and
- replacing fragile methods by more robust methods.

For example, a proof like

```isabelle
apply (drule ac_corres_ccorres_underlying)
apply (clarsimp simp: ccorres_underlying_def corres_underlying_def rf_sr_def Ball_def liftE_def)
apply (erule allE, erule allE, erule_tac P="cstate_relation _ _" in impE, assumption)
apply clarsimp
apply (erule allE, erule impE, rule_tac P="arg_rel _" and Q="¬snd _" in conjI, assumption, assumption)
apply (erule allE, erule allE, erule_tac P="Γ⊢⇩h ⟨_, _⟩ ⇒ _" in impE, assumption)
apply (rename_tac s s' n ret)
apply (case_tac ret; (simp; fail)?)
apply (clarsimp simp: in_liftE[simplified liftE_def])
apply (erule allE, erule allE, erule_tac P="_ ∈ fst _" in impE, assumption)
apply (auto simp: unif_rrel_def)
```

could be better written as

```isabelle
by (fastforce simp: ccorres_underlying_def corres_underlying_def rf_sr_def Ball_def liftE_def
                       unif_rrel_def in_liftE[simplified liftE_def]
              split: xstate.splits dest!: ac_corres_ccorres_underlying)
```

Another example from
[Hoare](https://isabelle.in.tum.de/library/HOL/HOL-Hoare/Pointer_Examples.html) is the proof

```isabelle
apply clarify
apply(rename_tac ps b qs)
apply clarsimp
apply(rename_tac ps')
apply(rule_tac x = ps' in exI)
apply simp
apply(rule_tac x = "b#qs" in exI)
apply simp
```

It was rewritten to

```isabelle
apply(fastforce intro:notin_List_update[THEN iffD2])
```

## Rationale

When proving a non-trivial theorem, the first attempt usually explores
various possibilities, e.g. using `erule` and `drule` on assumptions and
using `clarsimp` every other line. Similarly, program verification proofs
tend to use `wp` for single steps, proofs of identities have many `subst`
steps, and so on. Compacting such proofs usually improves them:

- Removing the noise of many small steps makes proofs easier to read.
- Proofs are less likely to break due to trivial definitional changes.
- Sometimes, compacted proofs run faster.

Of course, while compacted proofs break less often, they may be harder
to fix once they do break. Thus proofs should not be over-compressed to
the point where the overall proof strategy becomes incomprehensible.

## Example: classical reasoning

Worked example of how to shrink an erule-heavy first proof. The source was
[proof/crefine/AutoCorresTest](https://github.com/seL4/l4v/blob/master/proof/crefine/autocorres-test/AutoCorresTest.thy), but the proof there has changed in the meantime.

This was the original fragment:

```isabelle
apply (drule ac_corres_ccorres_underlying)
apply (clarsimp simp: ccorres_underlying_def corres_underlying_def rf_sr_def Ball_def liftE_def)
apply (erule allE, erule allE, erule_tac P="cstate_relation _ _" in impE, assumption)
apply clarsimp
apply (erule allE, erule impE, rule_tac P="arg_rel _" and Q="¬snd _" in conjI, assumption, assumption)
apply (erule allE, erule allE, erule_tac P="Γ⊢⇩h ⟨_, _⟩ ⇒ _" in impE, assumption)
apply (rename_tac s s' n ret)
apply (case_tac ret; (simp; fail)?)
apply (clarsimp simp: in_liftE[simplified liftE_def])
apply (erule allE, erule allE, erule_tac P="_ ∈ fst _" in impE, assumption)
apply (auto simp: unif_rrel_def)
```

We will try to compact this proof using the simplification and classical
logic methods. The most commonly used are `clarsimp`, `force`, `fastforce` and
`auto`, which are all part of the "clasimp" toolbox. These methods can
subsume:

- `simp`: by default
- `drule`: `dest` attribute
- `erule`: `elim` attribute
- `rule`: `intro` attribute
- `case_tac`: `split` attribute

When working with a sequential forward-deduction proof such as this,
it's often a good idea to start from the end. First, let's see if the
classical-simp methods can solve the last forward step:

```diff
  apply (clarsimp simp: in_liftE[simplified liftE_def])
+ try0 simp: unif_rrel_def
- apply (erule allE, erule allE, erule_tac P="_ ∈ fst _" in impE, assumption)
- apply (auto simp: unif_rrel_def)
```

We immediately get

```diff
  try0 simp: unif_rrel_def
+ by (fastforce simp: unif_rrel_def)
```

and even

```diff
  apply (case_tac ret; (simp; fail)?)
- apply (clarsimp simp: in_liftE[simplified liftE_def])
- try0 simp: unif_rrel_def
- by (fastforce simp: unif_rrel_def)
+ by (fastforce simp: unif_rrel_def in_liftE[simplified liftE_def])
```

The `case_tac` can often be replaced with a `split` rule. In this
case, `ret` has type `xstate`, so we use `xstate.splits`:

```diff
  apply (rename_tac s s' n ret)
-  apply (case_tac ret; (simp; fail)?)
-  by (fastforce simp: unif_rrel_def in_liftE[simplified liftE_def])
+  by (fastforce simp: unif_rrel_def in_liftE[simplified liftE_def] split: xstate.splits)
```

Now that our proof does not need the names, we can also remove the `rename_tac`.

At this point, we have the forward instantiations

```isabelle
  apply (erule allE, erule impE, rule_tac P="arg_rel _" and Q="¬snd _" in conjI, assumption, assumption)
  apply (erule allE, erule allE, erule_tac P="Γ⊢⇩h ⟨_, _⟩ ⇒ _" in impE, assumption)
```

the original proof added explicit terms to document what was being
instantiated. However, looking at the proof state and the assumption
steps, we can conclude that the instantiations in this proof are rather
trivial and do not need documentation. `fastforce` has no problem doing
them automatically:

```diff
  apply (clarsimp simp: ccorres_underlying_def corres_underlying_def rf_sr_def Ball_def liftE_def)
- apply (erule allE, erule allE, erule_tac P="cstate_relation _ _" in impE, assumption)
- apply clarsimp
- apply (erule allE, erule impE, rule_tac P="arg_rel _" and Q="¬snd _" in conjI, assumption, assumption)
- apply (erule allE, erule allE, erule_tac P="Γ⊢⇩h ⟨_, _⟩ ⇒ _" in impE, assumption)
+ by (fastforce simp: unif_rrel_def in_liftE[simplified liftE_def] split: xstate.splits)
```

If we want, we can go all the way and convert this proof to a one-liner:

```diff
- apply (drule ac_corres_ccorres_underlying)
- apply (clarsimp simp: ccorres_underlying_def corres_underlying_def rf_sr_def Ball_def liftE_def)
- by (fastforce simp: unif_rrel_def in_liftE[simplified liftE_def] split: xstate.splits)
+ by (fastforce simp: ccorres_underlying_def corres_underlying_def rf_sr_def Ball_def liftE_def
+                     unif_rrel_def in_liftE[simplified liftE_def]
+               split: xstate.splits dest!: ac_corres_ccorres_underlying)
```