Umon (Feb 21 2023 at 16:57): Umon (Feb 21 2023 at 16:57):Hey guys, I'm having a lot of trouble proving anything about an object that's gone through my recursive function.
The function works through a termination condition via if else and I've already been able to prove that it terminates.
The easiest example would be something like
fun test:: "nat ⇒ nat" where
"test x = (if x < 5 then x else test ( x- 2))"
When trying to prove that test x <= xI can obviously show that x-2 < x and x<= x, but I'm unable to show how this means that the end result is <= x, despite those being the only two possible cases.
Same goes for properties that don't get changed in either case, like the evenness of x in this case.
Is there some inductive rule for cases like these?
Lukas Stevens (Feb 21 2023 at 17:00):Are you using the induction rule test.induct?
Lukas Stevens (Feb 21 2023 at 17:02):lemma "test x ≤ x"
apply(induction rule: test.induct)
by (metis diff_le_self le_eq_less_or_eq le_trans test.elims)
or
proof(induction rule: test.induct)
case (1 x)
then show ?case
unfolding test.simps[of x]
by (auto simp del: test.simps)
qed
Well, that works, but as far as I can tell test.induct merely shows (¬ x < 5 ⟹ test (x - 2) ≤ x - 2) or more generally, that as long as the termination condition remains unfulfilled, the lemma is true.
Is that really enough to say something about the result after the recursion? "even x ≡ even (test x)" for example can't be proven that way, or at least sledgehammer doesn't find anything. I personally think it only works on the previous lemma because x getting smaller is basically the measure for the termination.
How do I make the jump from "it remains true while looping" to "it remains true for the end result"?
Lukas Stevens (Feb 23 2023 at 12:09):No, you are misunderstanding the induction rule. The above shows test x ≤ x for all x.
Lukas Stevens (Feb 23 2023 at 12:10):It is just the case that you only have an induction hypothesis for the case that x is greater than or equal to 5. If x < 5 you just have to show test x ≤ x without any I.H. available.
Umon (Feb 23 2023 at 13:12):Yeah, you're completely right. I was able to prove my lemmas using cases and .induct.
A lot of my confusion came from how sometimes cases would target other variables than the induction and I ended up with a bunch of orange and blue variables refusing to cooperate.
It turned out that the 'direction' of the "=" mattered. As in, (property) (test x) = (property) x was a lot easier to prove than (property) x= (property) (test x) ?
Thank you very much for your help!
Manuel Eberl (Feb 23 2023 at 14:28):Generally it's a good idea to always tell induct and cases what variables (or, more generally, terms) you want to induct/case distinguish on. The only time when it's safe to omit that information is when you're chaining in some assumption with using that the induction/cases rule consumes, e.g. induction rules that come out of inductive predicates. Otherwise unpredictable things happen.
Last updated: Apr 19 2024 at 04:17 UTC