Stream: Beginner Questions

Topic: Why not possible to concluce n = 0 here?


view this post on Zulip waynee95 (Dec 13 2022 at 19:24):

I have the following situation:

lemma lapprox_tm0_stays_stable:
  assumes "lapprox_tm0 η0 η1 d φ x ⊥ n = lapprox_tm0 η0 η1 d φ x ⊥ (Suc n)"
    and "m ≥ n"
  shows "lapprox_tm0 η0 η1 d φ x ⊥ m = lapprox_tm0 η0 η1 d φ x ⊥ n"
proof (induction m)
  case 0
  with assms(2) have "n = 0"
    sorry

  have "lapprox_tm0 η0 η1 d φ x ⊥ 0 = (⊥, η1, d)"
    by simp
  with ‹n = 0› show ?case
    by simp
next
  case (Suc m)
  then show ?case
    by (metis assms(1) lapprox_tm0.simps(2))
qed

Why is it not possible to conclude that "n = 0" given that "m = 0" here and "m \geq n" from the assumption?

view this post on Zulip Simon Roßkopf (Dec 13 2022 at 20:00):

If you need to use an assumption in the induction, it needs to be part of the proof state before you use induction, otherwise it will not be available.

You can add them by adding using assms before starting your proof.


Last updated: Mar 28 2024 at 16:17 UTC