Stream: Beginner Questions

Topic: induction rule from `fun`

Alexandre Soares (Sep 23 2024 at 19:34):

I learned from "Programming and Proving" that when we create a function with fun we get a custom induction rule to be used with the induction method. So I create the following function, which is supposed to be the less-than-or-equal relation.

fun lesseq :: "nat => nat => nat" where
    "lesseq 0 _ = True"
|   "lesseq (Suc _) 0 = False"
|   "lesseq (Suc m) (Suc n) = lesseq m n"

Now if I try

lemma "lesseq 0 n"
  apply (induction n rule: lesseq.induct)

I get three goals, the second of which is obviously unprovable.

proof (prove)
goal (3 subgoals):
 1. ⋀uu_. lesseq 0 uu_
 2. ⋀uv_. lesseq (Suc uv_) 0
 3. ⋀m n. lesseq m n ⟹ lesseq (Suc m) (Suc n)

and indeed if I apply simp twice the first goal gets solved but the second goal reduces to False. The lemma is certainly true. What am I missing?

Jonas Stahl (Sep 23 2024 at 20:38):

The induct schema of lesseq is for 2 variables. You could use it for something like this:

lemma "n ≤ m ⟹ lesseq n m"
  apply (induction n rule: lesseq.induct)
  by auto

For the 1 variable of your example you can just induct over the variable without special induction schema.

Alexandre Soares (Sep 24 2024 at 18:28):

@Jonas Stahl thank you. I did notice that plain induction was enough, I was just wondering why the scheme was requiring that I prove something that was false.

Jonas Stahl (Sep 24 2024 at 19:01):

That's actually a thing of induction schemas. Not every schema can be used for every proof and sometimes they generate you those "dead" goals. Here it's actually up to you to choose the correct schema.

Last updated: Dec 21 2024 at 16:20 UTC