Stream: Beginner Questions

Topic: Proving a lemma by strong induction

Lekhani Ray (Jul 21 2022 at 11:59):

Hello All!
Thank you for your help sp far.

I am trying to prove a lemma in Isabelle,

lemma (in th2) addMeaningF_4 [rule_format]: "⋀m. m ≤ n ⟹ m = (len x + len y) ⟹ (evalBinNum_1 (addBinNum x y) = plus (evalBinNum_1 x) (evalBinNum_1 y))"
apply(induct n rule: nat_less_induct)

My subgoal is basically the same lemma again

⋀n m. ∀m<n. ∀xa≤m.
xa = len x + len y ⟶
evalBinNum_1 (addBinNum x y) =
plus (evalBinNum_1 x) (evalBinNum_1 y) ⟹
m ≤ n ⟹
m = len x + len y ⟹
evalBinNum_1 (addBinNum x y) =
plus (evalBinNum_1 x) (evalBinNum_1 y)

I am worried I might have misunderstood something and hence unable to move forward with the proof.

TIA!

Mathias Fleury (Jul 21 2022 at 12:03):

It is not the same goal again, since you have the "∀xa≤m".

Mathias Fleury (Jul 21 2022 at 12:03):

So the questions is more what did you expect?

Mathias Fleury (Jul 21 2022 at 12:05):

BTW, tend to find this version of the induction lemma more natural than the default version:

lemma nat_less_induct_case[case_names 0 Suc]:
  assumes
    \<open>P 0\<close> and
    \<open>\<And>n. (\<forall>m < Suc n. P m) \<Longrightarrow> P (Suc n)\<close>
  shows \<open>P n\<close>
  apply (induction rule: nat_less_induct)
  by (rename_tac n, case_tac n) (auto intro: assms)

Mathias Fleury (Jul 21 2022 at 12:06):

This version has the case distinction 0/Suc, that I find more natural.

Lekhani Ray (Jul 21 2022 at 12:23):

Mathias Fleury said:

This version has the case distinction 0/Suc, that I find more natural.

This does help, thank you so much.

It breaks the proof into simpler cases, however, the second lemma is still a challenge for me.

lemma (in th2) addMeaningF_4: "n = (len x + len y) ⟹ (evalBinNum_1 (addBinNum x y) = plus (evalBinNum_1 x) (evalBinNum_1 y))"
proof(induction n rule: nat_less_induct_case)
  case 0
  then show ?case
    using len.elims by auto
next
  case (Suc n)
  then show ?case
qed

It gives me a subgoal
⋀n. ∀m<Suc n. m = len x + len y ⟶ evalBinNum_1 (addBinNum x y) = plus (evalBinNum_1 x) (evalBinNum_1 y) ⟹
Suc n = len x + len y ⟹ evalBinNum_1 (addBinNum x y) = plus (evalBinNum_1 x) (evalBinNum_1 y)

I was wondering how this may be approached?

Mathias Fleury (Jul 21 2022 at 12:28):

My guess: you have to generalize over x and y too. Then from Suc n = len x + len y you know that either len x or len y is a Suc. You decompose that list into head/tail. And after some simplification, you can use the induction principle.

Mathias Fleury (Jul 21 2022 at 12:32):

although i am not sure what x and y exactly are

Lekhani Ray (Jul 21 2022 at 12:44):

x and y are Binary Numerals here

Javier Diaz (Jul 23 2022 at 14:44):

I think the easiest way to prove your lemma is not by induction on the combined length of the arguments of addBinNum but by computation induction as follows:

lemma (in th2) addMeaningF_4: "evalBinNum_1 (addBinNum x y) = plus (evalBinNum_1 x) (evalBinNum_1 y)"
  using assoc and commute by (induction rule: addBinNum.induct, auto) (metis arith_1)+

Please note that it's necessary to add both associativity and commutativity lemmas to your definition of plus in th2 as follows (proofs are left as exercises):

lemma (in th2) commute: "plus x y = plus y x"
  sorry

lemma (in th2) assoc: "plus (plus x y) z = plus x (plus y z)"
  sorry

Last updated: Apr 23 2024 at 04:18 UTC