Stream: Beginner Questions

Topic: ✔ Where to put assumptions in Isar proof

Alex Weisberger (Nov 21 2021 at 00:46):

Hello,

I am trying to prove the following lemma to aid in a later theorem:

lemma char_of_symmetric: "((of_char (char_of n))::nat) = n" (is "?P n")
proof (induction n)
  case 0
  show ?case by auto
next
  fix n assume "?P n"
  thus "?P (Suc n)" by simp
qed

(of_char and char_of come from the Show.Show_Instances theory)

After this, the proof state has 1 subgoal remaining:

1. n mod 256 = n ⟹ Suc n mod 256 = Suc n

I believe this mod 256 is coming from the fact that the Isabelle char and string implementation implements UTF-8, which sets this limit on character code digits (I'm not a UTF-8 expert, but this seems plausible).

In my case, I am serializing single digits, so I know that n here will always be < 10. Where can I put this assumption to hopefully get this proof goal to be discharged?

I have tried fix n assume "n < 10 /\ (?P n)", and I've tried assume "n < 10" at the beginning of the proof, before all case analyses. I am always met with a syntax error, or the errors: "Illegal application of proof command in "state" mode."

Any tips here?

Alex Weisberger (Nov 21 2021 at 04:34):

I made some progress by re-reading the "Structured Lemma Statements" section of Concrete Semantics:

lemma char_of_symmetric:
  assumes single_digit: "(n::nat) < 10"
  shows "((of_char (char_of n))::nat) = n" (is "?P n")
proof (induction n)
  case 0
  show ?case by auto
next
  fix n assume "(?P n)"
  with single_digit show "?P (Suc n)" by simp
qed

I think adding the assumption single_digit at the top level makes sense, though it doesn't seem to actually apply the assumption unless I use with single_digit_show (which is slightly surprising). Even still, I'm left with this final proof goal:

1. n < 10 ⟹ n mod 256 = n ⟹ Suc n mod 256 = Suc n

This looks to me like a true statement - n mod 256 = n if n < 10. I even proved that in a separate lemma to double check, though it required some casting which might be the source of the issue:

lemma "(n::nat) < 10 ⟹ n mod 256 = n"
  by auto

(* This is correctly proven *)

So, I'm not sure how to discharge this final goal.

Mathias Fleury (Nov 21 2021 at 06:58):

you are missing an using assms before the proof (induction n)

Wenda Li (Nov 21 2021 at 11:19):

Assuming the constantsof_char and char_of come from HOL.String, a relevant lemma can be found through find_theorems of_char char_of:

String.unique_euclidean_semiring_with_bit_shifts_class.of_char_of:
    of_char (char_of ?a) = ?a mod 256

In particular, this lemma has been declared as a simplification rule, so that we don't need to invoke it explicitly. Your intended lemma should be provable without induction:

lemma
  assumes "n<256"
  shows "((of_char (char_of n))::nat) = n"
  using assms by auto

Alex Weisberger (Nov 21 2021 at 13:09):

using assms worked - here is the final proof:

lemma char_of_symmetric:
  fixes n :: nat
  assumes "n < 10"
  shows "of_char (char_of n) = n"
  using assms
proof (induction n)
  case 0
  show ?case by auto
next
  case (Suc n)
  then show ?case by auto
qed

I also didn't know about find_theorems, so that is very helpful. I just wanted to carry the proof out myself for learning purposes, but obviously I want to use existing theorems as much as possible.

Thanks everyone!

Notification Bot (Nov 21 2021 at 13:34):

Alex Weisberger has marked this topic as resolved.

Last updated: Dec 21 2024 at 16:20 UTC