Zulip Chat Archive

Stream: new members

Topic: Propagate proof state in match?


view this post on Zulip Daniel Fabian (Aug 24 2019 at 11:26):

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?

view this post on Zulip Mario Carneiro (Aug 24 2019 at 12:12):

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

view this post on Zulip Mario Carneiro (Aug 24 2019 at 12:13):

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

view this post on Zulip Mario Carneiro (Aug 24 2019 at 12:15):

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

view this post on Zulip Mario Carneiro (Aug 24 2019 at 12:16):

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

view this post on Zulip Mario Carneiro (Aug 24 2019 at 12:16):

Or make an intermediate definition or two

view this post on Zulip Daniel Fabian (Aug 24 2019 at 13:48):

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

view this post on Zulip Daniel Fabian (Aug 24 2019 at 14:01):

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?

view this post on Zulip Daniel Fabian (Aug 24 2019 at 14:14):

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


Last updated: May 16 2021 at 05:21 UTC