Stream: Beginner Questions

Topic: Weird induction scheme


view this post on Zulip Christian Zimmerer (Jun 23 2023 at 13:27):

I'm trying to prove the following induction scheme:

If there is a range of integers and a proposition holds for the bounds, and for the neighbors of any n, it holds for any n in the bounds.

I am trying to prove this by induction over the range, as for the case of only one inner element in the range it trivially holds, and if the range increases by one element, the proposition still holds if either l is decreased or m is increased. However, I struggle to tell Isabelle. How would I formulate the proof in the best way?

view this post on Zulip Mathias Fleury (Jun 23 2023 at 14:01):

can you just do induction on n-l?

view this post on Zulip Mathias Fleury (Jun 23 2023 at 14:03):

my first intuition is however that it does not hold, because proving the case l+1 does not work without proving m-1 and vice-versa

view this post on Zulip Mathias Fleury (Jun 23 2023 at 14:08):

Okay nitpick agrees for natural numbers that it does not hold:

Nitpicking formula...
Nitpick found a counterexample:
  Free variables:
    P = (λx. _)(0 := True, 1 := False, 2 := False, 3 := True)
    l = 0
    m = 3
    n = 2

view this post on Zulip Wolfgang Jeltsch (Jun 23 2023 at 15:16):

Note that there is also dec_induct, which might be helpful in your case.


Last updated: Feb 27 2024 at 08:17 UTC