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: Dec 20 2023 at 11:08 UTC