In lean4 why is induction only rewriting the goal, and not the known facts?

Question

When I do induction over a variable $x$ in lean 4, why isn't $x=0$ available as a fact in the base case of the induction? Without this fact, I can't rewrite other facts in order to make the induction work.

For example, if I run this:

structure Odds where
  lose : Nat
  win : Nat
def odds_leq (a b : Odds) : Bool := a.win * b.lose <= b.win * a.lose
infixl:45 " ≤ " => odds_leq
infixl:45 " <= " => odds_leq

theorem odds_leq_transitive (a b c: Odds) (ab : a <= b) (bc : b <= c) : a <= c := by
  unfold odds_leq
  unfold odds_leq at ab
  unfold odds_leq at bc
  simp
  simp at ab
  simp at bc
  induction a.win
  sorry

I get this proof state:

Which is notably lacking a line like h : a.win = 0 in case zero. It also didn't rewrite ab : a.win + b.lose <= b.win * a.lose into ab : 0 + b.lose <= b.win * a.lose.

Answer 1

First a comment about your definition. By defining odds_leq to map into Bool rather than Prop you are making your life difficult unecessarily, because you will have to prove things like (odds_leq x y) = true instead of just odds_leq x y. So I am going to change Bool to Prop on the assumption that you're just not paying attention, or are unfamiliar with the difference between Prop and Bool.

The induction tactic does not seem to be very good at inducting on a non-variable, in your case a.win. If you first take apart a so that it becomes {lose := a₁, win := a₂} then induction a₂ will work as expected.

This should get you going:

structure Odds where
  lose : Nat
  win : Nat

def odds_leq (a b : Odds) : Prop := a.win * b.lose <= b.win * a.lose

infixl:45 " ≤ " => odds_leq

theorem odds_leq_transitive (a b c : Odds) (ab : a ≤ b) (bc : b ≤ c) : a ≤ c := by
  -- unfold odds_leq everywhere in one go
  unfold odds_leq at *
  -- we decompose a into {lose := a₁, win := a₂} to help induction
  cases a with | mk a₁ a₂ =>
    simp at * -- simplify everywhere
    induction a₂ -- now it works as expected
    case zero => simp
    case succ k IH => sorry -- you're on your own here