Stream: Beginner Questions

Topic: ✔ Proof by induction


view this post on Zulip Lekhani Ray (Jul 15 2022 at 16:56):

Hello,
I am trying to prove a (seemingly simple) lemma, However, I think I may be missing something

lemma len_check [simp]: "n = len (addBinNum x y) ⟹ n ≤ len x + len y"
proof(induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case sorry (*this is where I get stuck*)
qed

The subgoal says : ⋀n. (n = len (addBinNum x y) ⟹ n ≤ len x + len y) ⟹
Suc n = len (addBinNum x y) ⟹ Suc n ≤ len x + len y

My question : Do I need to induct on n further. Simple methods do not work. If I create another lemma "Suc n = len (addBinNum x y) ⟹ Suc n ≤ len x + len y" it possibly needs to refer to the 1st one. I am extremely confused as to how to proceed. Any help is appreciated.

For reference :

fun len :: "BinNum ⇒ nat"
  where
    "len Zero = 1"|
    "len One = 1"|
    "len (JoinZero x) = len x + 1"|
    "len (JoinOne x) = len x + 1"

function (domintros) addBinNum :: "BinNum ⇒ BinNum ⇒ BinNum"
where
  "addBinNum Zero Zero = Zero"|
  "addBinNum Zero One = One"|
  "addBinNum One Zero = One"|
  "addBinNum One One = JoinOne Zero"|
  "addBinNum Zero (JoinZero x) = JoinZero x"|
  "addBinNum One (JoinZero x) = JoinOne x"|
  "addBinNum One (JoinOne x) = JoinZero (addBinNum One x)"|
  "addBinNum Zero (JoinOne x) = JoinOne x"|
  "addBinNum (JoinZero x) Zero = JoinZero x"|
  "addBinNum (JoinZero x) One = JoinOne x"|
  "addBinNum (JoinOne x) Zero = JoinOne x"|
  "addBinNum (JoinOne x) One = JoinZero (addBinNum One x)"|
  "addBinNum (JoinZero x) (JoinZero y) = JoinZero(addBinNum x y)"|
  "addBinNum (JoinZero x) (JoinOne y) = JoinOne(addBinNum x y)"|
  "addBinNum (JoinOne x) (JoinZero y) = JoinOne(addBinNum x y)"|
  "addBinNum (JoinOne x) (JoinOne y) = JoinZero(addBinNum(addBinNum x y) One)"
  by pat_completeness auto

any help is apreciated, thank you

view this post on Zulip Maximilian Schaeffeler (Jul 15 2022 at 18:46):

First, I would simplify the definition of addBinNum:
Swap the arguments in the recursive call in this line: addBinNum (JoinOne x) One = JoinZero (addBinNum One x).
Then you can get rid of function (domintros) and replace it with fun.

Finally for the lemma, get rid of the n, and replace it with addBinNum x y in the conclusion.
Then use computation induction: induction x y rule: addBinNum.induct to prove your goal.

view this post on Zulip Lekhani Ray (Jul 15 2022 at 20:46):

Thank you so much, it did the trick!

view this post on Zulip Notification Bot (Jul 18 2022 at 17:11):

Lekhani Ray has marked this topic as resolved.


Last updated: Feb 27 2024 at 08:17 UTC