Stream: Beginner Questions

Topic: Why does simp fail?

Jamie Jorgensen (May 18 2023 at 16:00):

Hi folks. I'm very new to Isabelle, and trying to get started by proving some very basic things about 32-bit words. In the following code I prove a lemma, and then try to use the simp tactic to rewrite using my lemma.

 theory Wordplay
  imports Main "Word_Lib.Word_32" "Word_Lib.Hex_Words"
begin
context
  includes bit_operations_syntax
begin

fun ith_and :: "word32 ⇒ word32 ⇒ nat ⇒ bool" where
"ith_and x y i = ((bit x i) ∧ (bit y i))"

lemma to_bl_and : "to_bl(x && y) = rev (map (ith_and x y) [0 ..<32])"
  apply(simp add: to_bl_eq_rev word_size rev_map)
  apply(auto)
  using bit_and_iff apply blast
  using bit_and_iff apply blast
  using bit_and_iff apply blast
  done

lemma and_leq : "∀x y. pop_count (x AND y) ≤ pop_count x"
  apply (simp add: pop_count_def)
  apply(simp add: to_bl_and)

end
end

That last apply(simp add:to_bl_and) fails, even though the goal looks like it could be simplified.

proof (prove)
goal (1 subgoal):
 1. ∀x y. length (filter id (to_bl (x && y)))
          ≤ length (filter id (to_bl x))
Failed to apply proof method⌂:
goal (1 subgoal):
 1. ∀x y. length (filter id (to_bl (x && y)))
          ≤ length (filter id (to_bl x))

Jamie Jorgensen (May 18 2023 at 16:40):

Oh! I think I got it! I guess I need to explicitly declare the types of x and y in this lemma. Sorry to post a question, and then immediately get to the answer. Isn't that always the way it goes? I had been tearing my hair out on this one for a while.

lemma and_leq : "∀x y :: word32. pop_count (x AND y) ≤ pop_count x"
  apply (simp add: pop_count_def)
  apply(simp add: to_bl_and)

(Still not sure if this is the right way to prove this lemma, but I'm making progress at least)

Mathias Fleury (May 19 2023 at 05:11):

You could for

lemma and_leq : "pop_count (x AND y) ≤ pop_count x" for x y :: word32

Generally, writing ∀ for variables in a lemma is a bad idea (if you don't have to give a type, you can drop the for completely).

Mathias Fleury (May 19 2023 at 05:11):

And for words, expect to write a lot of types

Mathias Fleury (May 19 2023 at 05:12):

including in intermediate steps if you work on extracting parts of the word

Jamie Jorgensen (May 22 2023 at 02:51):

Mathias Fleury said:

You could for

lemma and_leq : "pop_count (x AND y) ≤ pop_count x" for x y :: word32

Generally, writing ∀ for variables in a lemma is a bad idea (if you don't have to give a type, you can drop the for completely).

Thank you! Very helpful!

Last updated: Apr 28 2024 at 08:19 UTC