unfolding definition on just lhs of equality

Stream: new members

[Richard Kiss]

I'm trying to prove something about a recursive function that is almost exactly the definition, but not quite. It would be easy to do if I could use unfold on just the left hand side. But unfold replaces the definition on both the left and the right. How can I limit unfolding to just the left?

[Eric Wieser]

It's very hard to answer this kind of question without a #mwe

[Eric Wieser]

It's very hard to answer this kind of question without a #mwe

[Eric Wieser]

Though perhaps you're looking for conv_lhs => unfold foo

[Richard Kiss]

good point, I'll produce one

[Richard Kiss]

it's quite large because I am too inexperienced to produce a more concise proof of termination.

import Mathlib

abbrev Atom := Array UInt8

-- the next two theorems are just to help prove `nat_to_atom` terminates
-- almost certainly there's a better way to do this

theorem shift_as_division { k: Nat }: n >>> k = n / (2 ^ k) := by
  unfold HShiftRight.hShiftRight
  unfold instHShiftRight
  unfold ShiftRight.shiftRight
  unfold Nat.instShiftRightNat
  simp
  induction k with
  | zero =>
      simp
  | succ k ih =>
      unfold HShiftRight.hShiftRight
      unfold instHShiftRight
      unfold Nat.shiftRight
      unfold ShiftRight.shiftRight
      unfold Nat.instShiftRightNat
      unfold Nat.shiftRight
      simp
      rw [ih]
      rw [Nat.div_div_eq_div_mul n (2^k) 2]
      rfl


theorem shift_decreasing : n>0 → n >>> 8 < n := by
  intro h
  rw [shift_as_division]
  exact Nat.div_lt_self h (by decide)


def nat_to_atom (n: Nat) : Atom :=
  let rec inner_func (n: Nat) : Atom :=
    if h256: n >= 256 then
      have h0: n > 0 := Nat.zero_lt_of_lt h256
      have : n >>> 8 < n := shift_decreasing h0
      (inner_func (n >>> 8)) ++  #[n.toUInt8]
    else
      #[n.toUInt8]
  if n = 0 then
    #[]
  else
    inner_func n


theorem nat_to_atom_prefix: n>0 → ∃ k, (nat_to_atom.inner_func n) = (nat_to_atom.inner_func (n >>> 8)) ++ #[k] := by
  intro h_n
  use (n % 256)
  unfold nat_to_atom.inner_func
  sorry

[Richard Kiss]

anyway, the unfold at the bottom unfolds both sides, which is not what I want. If I could find a way to unfold just the left, I believe the proof would be straightforward after that

[Eric Wieser]

Eric Wieser said:

Though perhaps you're looking for conv_lhs => unfold foo

Did you try this?

[Richard Kiss]

that looks like it should do exactly what I want, thank you!!

[Richard Kiss]

is there something I should be using besides unfold? I notice sometimes simp is helpful and other times it isn't, although I haven't been able to figure out exactly when. Maybe something to do with include statements (maybe unfold does transitive includes and simp doesn't?)

[Richard Copley]

Lean 3 had include and omit declarations, but I don't think they are implemented in Lean 4.
When the thing that you intend to do is unfold a definition, using unfold is the straightforward, expressive way to say so. Using simp only [xxx] to unfold the definition of xxx can be useful because it can also expand match statements and do beta-reduction. You can also do rw [xxx], which might be convenient if you're doing other rewrites at the same time.

[Ruben Van de Velde]

Correct, there's no more include and omit. I also don't have a clear idea of when unfold and simp work for definitions, but usually one of them does

[Matt Diamond]

@Richard Kiss btw shift_as_division is docs#Nat.shiftRight_eq_div_pow

[Richard Kiss]

I knew it had to exist somewhere

[Richard Kiss]

exact? didn't find it though, I suppose because I hadn't imported Init.Data.Nat.Lemmas

[Richard Kiss]

oh wait, things in Init are built-ins

[Matt Diamond]

you can often find these things by searching the mathlib web docs using relevant terms... when you type in "shift right div" it's the first result

[Raunak Chhatwal]

Richard Kiss said:

    if h256: n >= 256 then
      ...
    else
     ...

Is there documentation for this syntax and how it is desugared? In particular, I want to know how the then clause can be unlocked with a proof of n >= 256 and vice versa for the else clause.

[Matt Diamond]

I think it's just docs#ite and docs#dite

also I think your "unlocking" question is about docs#if_pos / docs#if_neg / docs#dif_pos / docs#dif_neg

[Richard Kiss]

I've used split or by_cases but both seem to have archaic lean 3 smell because they don't play nice with adding additional whitespace. I'm not sure what the modern lean 4 alternatives are. I can't figure out how to get cases to work every time

[Richard Kiss]

split can be frustrating because it often creates unnameable hypotheses and I can't figure out how to manipulate them

[Kevin Buzzard]

I have also never worked out how to name hypotheses after split; for me a very common idiom with Lean 3 split_ifs was split_ifs with AAA BBB CCC DDD EEE FFF GGG HHH III JJJ KKK and then go back and rename the variables correctly once I see their types (some would always be mysteriously missing, I never got to the bottom of this). But in Lean 4 we do have the smelly rename_i (which I can use) and then there are things like next and case which I can never get working, not least because I can never remember the names of any constructors; I don't know if they help you here.

[Mario Carneiro]

split does not have syntax to rename the variables, I use split <;> rename_i AAA BBB CCC instead

[Mario Carneiro]

or next AAA BBB CCC => if I want to name the variables differently in each case (you don't need to know the name of the constructor to use next, it's equivalent to case _)

[Kevin Buzzard]

Does next work after a \.? I don't use |, it's too CS for my liking (and I'm always in tactic mode)

[Kevin Buzzard]

For some reason I'm still always struggling with these sorts of silly things

[Mario Carneiro]

I prefer to use both . and next even though it's redundant because it looks more regular if you are already using . for subgoals everywhere else

[Mario Carneiro]

def foo : Nat → Nat
  | 0 => 0
  | n+1 => 1 + n

example (n : Nat) : foo n = n := by
  unfold foo; split
  · rfl
  · next n =>
    rw [Nat.add_comm 1 n]

[Mario Carneiro]

you can't use | either with split. Might be nice if you could

[Mario Carneiro]

TBH it's a pretty bare bones interface

[Mario Carneiro]

"it's redundant" meaning that this has the same effect:

example (n : Nat) : foo n = n := by
  unfold foo; split
  · rfl
  next n =>
    rw [Nat.add_comm 1 n]

but the asymmetric handling of subgoals here bugs me