179 lines
6.6 KiB
Markdown
179 lines
6.6 KiB
Markdown
<!--
|
||
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)
|
||
```
|