Propagate proof state in match?

Stream: new members

[Daniel Fabian]

As an exercise, I'm working on an red-black-tree. And I'm trying to show, that the re-balancing doesn't change the interpretation as a set.

universes u
variables α : Type u

inductive color
| red
| black

inductive node (α)
| leaf {} : node
| tree {} (color : color) (left : node) (val : α) (right : node) : node

def to_set {α} : node α → set α
| node.leaf := ∅
| (node.tree _ l y r) := to_set l ∪ {y} ∪ to_set r

instance node_to_set_coe : has_coe (node α) (set α) := ⟨to_set⟩

def balance {α} : color → node α → α → node α → node α
| color.black (node.tree color.red (node.tree color.red a x b) y c) z d :=
    node.tree color.red (node.tree color.black a x b) y (node.tree color.black c z d)
| color.black (node.tree color.red a x (node.tree color.red b y c)) z d :=
    node.tree color.red (node.tree color.black a x b) y (node.tree color.black c z d)
| color.black a x (node.tree color.red (node.tree color.red b y c) z d) :=
    node.tree color.red (node.tree color.black a x b) y (node.tree color.black c z d)
| color.black a x (node.tree color.red b y (node.tree color.red c z d)) :=
    node.tree color.red (node.tree color.black a x b) y (node.tree color.black c z d)
| color a x b := node.tree color a x b

lemma balance_mem {α} :
∀ c l (v : α) r, (node.tree c l v r : set α) = (balance c l v r : set α) :=
begin
    intros,
    from match c, l, v, r with
    | color.black, node.tree color.red (node.tree color.red a x b) y c, z, d :=
        begin
            unfold balance,
            sorry
        end
    | color.black, node.tree color.red a x (node.tree color.red b y c), z, d := begin sorry end
    | color.black, a, x, node.tree color.red (node.tree color.red b y c) z d := begin sorry end
    | color.black, a, x, node.tree color.red b y (node.tree color.red c z d) := begin sorry end
    | _, _, _, _ := begin sorry end
    end
end

Initially, I was thinking to just do it using cases by each variable, but it turns into 100s of cases and doesn't scale at all. What I really want to do is pattern match exactly the right cases and then unfold the definition of balance.

I'm a bit confused here. The goal inside the begin looks right, it wants me to prove

⊢ ↑(node.tree color.black (node.tree color.red (node.tree color.red a x b) y c) z d) =
    ↑(balance color.black (node.tree color.red (node.tree color.red a x b) y c) z d)

so balance should be happy to unfold into:

node.tree color.red (node.tree color.black a x b) y (node.tree color.black c z d)

However the tactic fails, any idea what I'm doing wrong?

[Mario Carneiro]

Use #print prefix balance and look for the _eqn_* theorems to see the actual equations lean will rewrite with

[Mario Carneiro]

Most likely, lean has done an additional case split on one of the other variables, and you will have to do that same split in the proof of properties of it

[Mario Carneiro]

looks like lean did quite a lot of case splitting - there are 122 equations for the definition

[Mario Carneiro]

I suggest rewriting balance with explicit cases applications so that you don't get so many superfluous splits

[Mario Carneiro]

Or make an intermediate definition or two

[Daniel Fabian]

oh wow, that's a lot of equations. I'll look into reducing the number of them by the strategy suggested.

[Daniel Fabian]

this is interesting: when I change the definition of balance to one w.r.t. to match, it's much happier. Consider these two (I believe) equivalent formulations

def balance {α} : color → node α → α → node α → node α
:=
begin
    intros c l v r,
    from match c, l, v, r with
    | color.black, node.tree color.red (node.tree color.red a x b) y c, z, d :=
        node.tree color.red (node.tree color.black a x b) y (node.tree color.black c z d)
    | color.black, node.tree color.red a x (node.tree color.red b y c), z, d :=
        node.tree color.red (node.tree color.black a x b) y (node.tree color.black c z d)
    | color.black, a, x, node.tree color.red (node.tree color.red b y c) z d :=
        node.tree color.red (node.tree color.black a x b) y (node.tree color.black c z d)
    | color.black, a, x, node.tree color.red b y (node.tree color.red c z d) :=
        node.tree color.red (node.tree color.black a x b) y (node.tree color.black c z d)
    | color, a, x, b := node.tree color a x b
    end
end
-- | color.black (node.tree color.red (node.tree color.red a x b) y c) z d :=
--     node.tree color.red (node.tree color.black a x b) y (node.tree color.black c z d)
-- | color.black (node.tree color.red a x (node.tree color.red b y c)) z d :=
--     node.tree color.red (node.tree color.black a x b) y (node.tree color.black c z d)
-- | color.black a x (node.tree color.red (node.tree color.red b y c) z d) :=
--     node.tree color.red (node.tree color.black a x b) y (node.tree color.black c z d)
-- | color.black a x (node.tree color.red b y (node.tree color.red c z d)) :=
--     node.tree color.red (node.tree color.black a x b) y (node.tree color.black c z d)
-- | color a x b := node.tree color a x b

the first one works fine and the second one has the problem. Is this some kind of subtlety of the equation compiler here?

[Daniel Fabian]

upon further investigation, the second version has about twice as many equations as the first one...