How to deal with exploding number of cases?

Stream: Program verification

[Daniel Fabian]

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]

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]

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]

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]

I am sometimes a bit reckless with simp but I think the accepted practices is to write:

suffices : _, by simp,

[Simon Hudon]

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]

ah yes, that's better. thx

[Simon Hudon]

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