Most conventional way to match nonzero natural numbers

Stream: new members

[Plamen Dimitrov]

Hi all, I had to come up with this termination proof for conversion to binary numbers

def ofNat : Nat → Binary
| n => (ofNatReversed n).reverse
where
  ofNatReversed : Nat → Binary
  | .zero => []
  | .succ n => (if (.succ n) % 2 == 0 then Bit.zero else Bit.one) :: ofNatReversed ((.succ n) / 2)
  termination_by n => n
  decreasing_by
    apply Nat.div_lt_self
    · apply Nat.pos_of_ne_zero
      intro h
      contradiction
    · decide

where the proof would require that n \ne 0 in the recursive case if I were to perform a simpler matching like

 ofNatReversed : Nat → Binary
  | 0 => []
  | n => (if n % 2 == 0 then Bit.zero else Bit.one) :: ofNatReversed (n / 2)

I would like to have something simpler like this but the problem is that n would also match zero as a natural number and the terminal proof cannot proceed. Lean is not aware of any order of matching to conclude that when we match n we would have already matched 0 before if ever and thus n should not be zero. Is there a better established way to match nonzero natural numbers or a more conventional way to do this terminal proof using only the simpler n match?

[Robin Arnez]

just do

inductive Bit where
  | zero | one

def Binary := List Bit

def ofNat : Nat → Binary
| n => (ofNatReversed n).reverse
where
  ofNatReversed (n : Nat) : Binary :=
    if n = 0 then []
    else
      (if n % 2 = 0 then Bit.zero else Bit.one) :: ofNatReversed (n / 2)

[Plamen Dimitrov]

Hi @Robin, I thought about the if-else-then function but matching a constructor seems more natural to me as something I would prefer to use. Do you think there is any way this can be achieved using the more inductive-type-friendly matching approach?