CODEWITHSUNDEEP
agdatheorem-provinglean
Oblivier
Oblivier

Reputation: 109

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

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?

Upvotes: 2

Views: 203

Answers (1)

Christopher Hughes
Christopher Hughes

Reputation: 1129

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.

Upvotes: 4

Related Questions