Stream: Beginner Questions

Topic: ✔ div2 induction example

waynee95 (Dec 11 2021 at 20:39):

In prog-prove the following example is used to introduce rule: something.induct:

fun div2 :: "nat ⇒ nat" where
"div2 0 = 0" |
"div2 (Suc 0) = 0" |
"div2 (Suc (Suc n)) = Suc (div2 n)"

And with apply (induction n rule: div2.induct) we can finish the proof with auto compared to apply (induction n) where the tutorial says that it needs further case analysis in the induction step.

I was wondering how that would look like. At this point there were not many (if any) examples that use case analysis in apply proofs and I could not figure it out myself so far.

Thanks!

Maximilian Schaeffeler (Dec 13 2021 at 07:35):

Hi,

after apply (induction n) the n in the second subgoal is under a quantifier, so you do a direct case analysis.
You can use subgoal for m to focus on that subgoal and introduce a new variable m that you can split on.

lemma "div2 n = n div 2"
  apply (induction n)
  subgoal by simp
  subgoal for m
    apply (cases m)
     apply simp
    sorry
  done

Still in this case you will not be able to complete the proof, as the induction hypothesis only gives you information about div2 m but you need information about div2 (m-1). You may instead prove following stronger theorem:

lemma "div2 n = n div 2 ∧ div2 (Suc n) = (Suc n) div 2"
  apply (induction n)
   apply auto
  done

or use a stronger induction rule:

lemma "div2 n = n div 2"
  apply (induction n rule: less_induct)
  subgoal for n
    apply (cases n)
    subgoal by simp
    subgoal for n'
      apply (cases n')
      by auto
    done
  done

However, all these proofs can be expressed much better using the Isar language (Chapter 4). I would strongly advise against using such nested apply style proofs.

lemma "div2 n = n div 2"
proof (induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case
  proof (cases n)
    case 0
    then show ?thesis by simp
  next
    case (Suc m)
    then show ?thesis sorry
  qed
qed

Notification Bot (Dec 14 2021 at 16:55):

waynee95 has marked this topic as resolved.

Last updated: Dec 21 2024 at 16:20 UTC