# Zulip Chat Archive

## Stream: Program verification

### Topic: How to deal with exploding number of cases?

#### Daniel Fabian (Jun 27 2020 at 22:37):

I'm trying to port a proof I did about rb-tree earlier in F* to lean as an exercise. (Original)

The main insertion algorithm is this

```
mutual def ins, insB
with ins : Π {h col}, ℤ → rbnode' h col → almost_node h
| ._ ._ x E := V (R E x E)
| ._ ._ x (B a y b) :=
if x < y then
match balance_lb (ins x a) y b with
| HR r := V r
| HB b := V b
end
else if x = y then V (B a y b)
else
match balance_rb a y (ins x b) with
| HR r := V r
| HB b := V b
end
| ._ ._ x (R a y b) :=
if x < y then balance_lr (insB x a) y b
else if x = y then V (R a y b)
else balance_rr a y (insB x b)
with insB : Π {h}, ℤ → rbnode' h black → hidden_tree h
| ._ x E := HR (R E x E)
| ._ x (B a y b) :=
if x < y then balance_lb (ins x a) y b
else if x = y then HB (B a y b)
else balance_rb a y (ins x b)
```

the lemma i solved previously is this:

```
mutual theorem ins_mem, insB_mem
with ins_mem : Π {h c} (x : ℤ) (s : rbnode' h c) (z : ℤ),
mem z s ∨ z = x ↔ almost_node_mem z (ins x s)
...
with insB_mem : Π {h} (x : ℤ) (s : rbnode' h black) (z : ℤ),
mem z s ∨ z = x ↔ hidden_tree_mem z (insB x s)
```

If you need the details, the full file is attached. But I do have a question; the proof is a real 200-line mess of dozens of trivial and semi-trivial cases and it takes half a minute just to typecheck. How are we meant to prove properties about programs realistically? Given that programs routinely have a good degree of cyclomatic complexity.

The equivalent F* proof looks like this:

```
val insB_mem : #h:nat -> x:int -> s:rbnode h Black ->
Lemma (ensures forall y. (mem y s \/ y = x) <==> hiddenTree_mem y (insB x s)) (decreases s)
let rec ins_mem #h #c x = function
| Leaf -> ()
| B a y b ->
if x < y then ins_mem x a
else if x = y then ()
else ins_mem x b
| R a y b ->
if x < y then insB_mem x a
else if x = y then ()
else insB_mem x b
and insB_mem #h x = function
| Leaf -> ()
| B a y b ->
if x < y then ins_mem x a
else if x = y then ()
else ins_mem x b
```

it still captures the relevant cases and shows how to recursively apply the IH and all. Now you'd of course expect a bit more automation from a Z3-backed theorem prover, but I think I'm doing something wrong that it would be 200+ lines.

rbtree_intrinsic.lean

#### Simon Hudon (Jun 27 2020 at 23:14):

I think it's a lot of different habits that would make your proofs shorter. For instance, `simp`

is the swiss knife of Lean. Instead of calling `unfold`

several times, you can use `simp`

to unfold all of them (in one call). Actually you could also make only one `unfold`

call. `simp`

also does some rewriting using its arguments and with the `simp`

list which is a good thing to cultivate. Tag some of your lemmas with `simp`

to make your future proofs simpler

#### Simon Hudon (Jun 27 2020 at 23:16):

For propositional reasoning, `tauto!`

might be the first thing to consider but `finish`

and `solve_by_elim`

can also be useful. `solve_by_elim`

does a more limited kind of reasoning but, unlike `tauto`

, it brings in theorems

#### Daniel Fabian (Jun 27 2020 at 23:35):

interesting, I usually was trying to avoid calling `simp`

on intermediate steps because I read it's meant to make proofs brittle. Would it be fine to do something like `simp`

,..., `simp`

, ..., `simp`

?

#### Simon Hudon (Jun 27 2020 at 23:42):

I am sometimes a bit reckless with `simp`

but I think the accepted practices is to write:

```
suffices : _, by simp,
```

#### Simon Hudon (Jun 27 2020 at 23:43):

I think already `simp only`

(for which `squeeze_simp`

can help you come up with the right list of lemmas) makes things more robust.

#### Daniel Fabian (Jun 27 2020 at 23:44):

ah yes, that's better. thx

#### Simon Hudon (Jun 28 2020 at 18:07):

It might also be that `by {[smt] eblast }`

could be useful. We should ask @Jesse Michael Han to write us a tutorial about how to choose `ematch`

lemmas

Last updated: May 08 2021 at 21:09 UTC