Partial unfolding

Stream: new members

[Yiftach S]

Hello. I'd like to use the 'unfold' tactic, only on the second occurance:

inductive Tree where
  | leaf
  | node (left : Tree) (key : Nat) (right : Tree)


def Tree.sizeOf : Tree → Nat
  | .leaf => 0
  | .node l _ r => 1 + l.sizeOf + r.sizeOf

Later I have:

have _ : left.sizeOf < t.sizeOf := by sorry

If I use "unfold Tree.sizeOf" it unfolds it both on the left and the right, but I only need it on the right.

Thanks!

[Kevin Buzzard]

(#backticks to make your code more readable -- you can edit your post)

[Yiftach S]

Kevin Buzzard said:

(#backticks to make your code more readable -- you can edit your post)

Thanks, done

[Kevin Buzzard]

There might be more elegant ways to do it but I would explicitly write equation lemmas for sizeOf and use nth_rewrite to do this (ie use rewrite rather than unfold)

[Yiftach S]

Kevin Buzzard said:

There might be more elegant ways to do it but I would explicitly write equation lemmas for sizeOf and use nth_rewrite to do this

I don't quite understand. What lemmas should I use? And how do I get nth_rewrite to become known? Thanks

[Damiano Testa]

Is this what you are looking for?

example {left t : Tree} : true := by
  have _ : left.sizeOf < t.sizeOf := by
    conv in Tree.sizeOf left =>
     unfold Tree.sizeOf
    sorry

[Yiftach S]

Damiano Testa said:

Is this what you are looking for?

example {left t : Tree} : true := by
  have _ : left.sizeOf < t.sizeOf := by
    conv in Tree.sizeOf left =>
     unfold Tree.sizeOf
    sorry

Thanks, that seems to do the trick! After:

match ht : t with
  | .node left key right =>
    -- used to prove termination
    have _ : left.sizeOf < t.sizeOf := by
      conv in Tree.sizeOf t => unfold Tree.sizeOf
      simp [ht]
      sorry

The goal becomes:

Tree.sizeOf left < 1 + Tree.sizeOf left + Tree.sizeOf right

Which should be trivial. How do I go about finding the right tactics to complete the proof?

[Kevin Buzzard]

omega and linarith will both do this, but they require a mathlib import, although omega just migrated to somewhere higher (std?) yesterday.

[Yiftach S]

Kevin Buzzard said:

omega and linarith will both do this, but they require a mathlib import, although omega just migrated to somewhere higher (std?) yesterday.

linarith worked like a charm! Thanks

[Patrick Massot]

Kevin, omega has always be in std, it migrated to core but you won’t see it before the next release.