Simple refl-based proof problem in Lean (but not in Agda)

Question

In an attempt to define skew heaps in Lean and prove some results, I have defined a type for trees together with a fusion operation:

inductive tree : Type
| lf : tree
| nd : tree -> nat -> tree -> tree

def fusion : tree -> tree -> tree
| lf t2 := t2
| t1 lf := t1
| (nd l1 x1 r1) (nd l2 x2 r2) :=
    if x1 <= x2
    then nd (fusion r1 (nd l2 x2 r2)) x1 l1
    else nd (fusion (nd l1 x1 l1) r2) x2 l2

Then, even for an extremely simple result such as

theorem fusion_lf : ∀ (t : tree), fusion lf t = t := sorry

I'm stuck. I really have no clue for starting to write this proof. If I start like this:

begin
  intro t,
  induction t with g x d,
  refl,
end

I can use refl for the case where t is lf, but not if it is a nd.

I'm a bit at a lost, since in Agda, it is really easy. If I define this:

data tree : Set where
  lf : tree
  nd : tree -> ℕ -> tree -> tree

fusion : tree -> tree -> tree
fusion lf t2 = t2
fusion t1 lf = t1
fusion (nd l1 x1 r1) (nd l2 x2 r2) with x1 ≤? x2
... | yes _ = nd (fusion r1 (nd l2 x2 r2)) x1 l1
... | no  _ = nd (fusion (nd l1 x1 r1) r2) x2 l2

then the previous result is obtained directly with a refl:

fusion_lf : ∀ t -> fusion lf t ≡ t
fusion_lf t = refl

What I have missed?

Have you tried using simpl (or simp) ? I don't know much about lean but if it's anything like coq (which it looks like) it should work. I tried testing it on the web version of lean but your code is not accepted for some reason. — MrO
This doesn't work. If I try it, I get the frustrating simplify tactic failed to simplify. — Oblivier
Can you confirm that the code you provided works directly ? Can you try and use this website : leanprover.github.io/live/latest . I would very much like to see if your code works fine there. — MrO
Yes, the definitions of a tree and of the fusion function do work there (just add an open tree before defining fusion). — Oblivier

Christopher Hughes Christopher Hughes · Accepted Answer · 2019-12-02T15:03:31

This proof works.

theorem fusion_lf : ∀ (t : tree), fusion lf t = t := 
λ t, by cases t; simp [fusion]

If you try #print fusion.equations._eqn_1 or #print fusion.equations._eqn_2 and so on, you can see the lemmas that simp [fusion] will use. The case splits are not exactly the same as the case splits in the pattern matching, because the case splits in the pattern matching actually duplicate the case lf lf. This is why I needed to do cases t. Usually the equation lemmas are definitional equalities, but this time they are not, and honestly I don't know why.

Simple refl-based proof problem in Lean (but not in Agda)

1 Answers