## Stream: Beginner Questions

### Topic: ✔ Proof by induction

#### 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 One One = JoinOne Zero"|
"addBinNum Zero (JoinZero x) = JoinZero x"|
"addBinNum One (JoinZero x) = JoinOne 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"|
by pat_completeness auto
``````

any help is apreciated, thank you

#### 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.

#### Lekhani Ray (Jul 15 2022 at 20:46):

Thank you so much, it did the trick!

#### Notification Bot (Jul 18 2022 at 17:11):

Lekhani Ray has marked this topic as resolved.

Last updated: Dec 07 2023 at 20:16 UTC