0
$\begingroup$

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:

enter image description here

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.

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

1 Answer 1

1
$\begingroup$

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
$\endgroup$
1
  • $\begingroup$ Thanks, the bool->prop advice is helpful. $\endgroup$ Dec 4, 2023 at 11:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.