How do you do induction on the members of a structure

Stream: lean4

[Alex Zani]

See for instance

structure NamedNat where
  s : string
  n : Nat

def add (a b : NamedNat) : NamedNat :=
  match b with
  | {n := 0, s := _} => a
  | {n := n+1, s := _} => add {a with n := a.n + 1} {b with n := n}

Now I want to prove:

def add_adds (a b : NamedNat) : (add a b).n = a.n + b.n := by

So I want to do induction on b.n, so that's what I tried:

def add_adds (a b : NamedNat) : (add a b).n = a.n + b.n := by
  induction b.n with
  | zero =>
    unfold add
    simp

I would expect that when I unfold add, the assumption that b.n = 0 would be taken into account, but it's not. So the tactic state is:

case zero
a : NamedNat
b : NamedNat
⊢ (match b with
    | { s := s, n := 0 } => a
    | { s := s, n := n.succ } => add { s := @NamedNat.s a, n := a.n + 1 } { s := @NamedNat.s b, n := n }).n =
  a.n

I'm confused by what is going on and how to address it.

See https://live.lean-lang.org/#codez=M4FwTgrgxiFgpgAgHIEMC28AmaSIO4AW8CAUIosIgFyXgCWAdgObmKM0qoimlbwAzRKixZEAClSIARpzSYc3AJRyM2XDQC8bdNyiEZBeiEJsAPogDeHapsQAGADSUtiAPoBfRJoB8w81Y2dowA1ACMzlS27l6+wqJWUvjGBkHCAHQcIYhhXpayySbsrowevPxCIlhuVVSShrTy6sqckglS0kqZ3hlZMt3R0gCebExY0CD0APYc0t2FphQWAF4kU94+bBQQjAJTADZiVVuU9OgADkA

[Kevin Buzzard]

I don't know much about this sort of thing but my understanding of this is that your expectation is wrong. If you do induction on b.n then Lean will replace all b.ns with 0 in the base case but not change anything else in the goal, including, for example, b. Also note that even if this worked, you would not be able to prove the successor case because you have fixed a and so your inductive hypothesis won't apply to the goal because a will have changed. This works:

def add_adds (a b : NamedNat) : (add a b).n = a.n + b.n := by
  cases b with
  | mk s n =>
    induction n generalizing a with
    | zero =>
      simp [add]
    | succ n IH =>
      simp [add, IH]
      omega

[Robin Arnez]

I mean, this is pretty obvious but you probably don't want to define your own addition - addition on Nats is an optimized case so def (a b : NamedNat) : NamedNat := { a with n := a.n + b.n } would be much faster. That out of the way, then general way how you'd approach something like this instead is
(1) by doing cases or match first or
(2) by doing generalize h : b.n = myval and then induction myval generalizing b ...

[Kevin Buzzard]

I don't think this is the same definition of addition though, because you'll get a different name.

[Alex Zani]

Robin Arnez said:

I mean, this is pretty obvious but you probably don't want to define your own addition - addition on Nats is an optimized case so def (a b : NamedNat) : NamedNat := { a with n := a.n + b.n } would be much faster.

Absolutely, I just needed something of reasonable size to illustrate the problem I'm having.

(1) by doing `cases` or `match` first or
(2) by doing `generalize h : b.n = myval` and then `induction myval generalizing b ...`

Thanks, that works.

[Arthur Adjedj]

You can make use of the induction principle provided by the function add. That principle is called add.induct. The following code works:

structure NamedNat where
  s : String
  n : Nat

def add (a b : NamedNat) : NamedNat :=
  match b with
  | {n := 0, s := _} => a
  | {n := n+1, s := _} => add {a with n := a.n + 1} {b with n := n}
termination_by b.n

def add_adds (a b : NamedNat) : (add a b).n = a.n + b.n := by
  induction a,b using add.induct with
  | case1 a h => simp [add]
  | case2 a s n ih =>
    simp_arith [add,ih] at *

[Alex Zani]

Robin Arnez said:

I mean, this is pretty obvious but you probably don't want to define your own addition - addition on Nats is an optimized case so def (a b : NamedNat) : NamedNat := { a with n := a.n + b.n } would be much faster.

Absolutely, I just needed something of reasonable size to illustrate the problem I'm having.

(1) by doing `cases` or `match` first or
(2) by doing `generalize h : b.n = myval` and then `induction myval generalizing b ...`

Thanks, that works.