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

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.

• Why did you define odd_leq to be in Bool rather than Prop? Commented Dec 4, 2023 at 10:07
• @AndrejBauer Due to not knowing better. Commented Dec 4, 2023 at 11:59

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

• Thanks, the bool->prop advice is helpful. Commented Dec 4, 2023 at 11:59