Stream: Beginner Questions

Topic: ✔ Simplification rules not applying to records

Alex Weisberger (Nov 25 2021 at 14:16):

Hi again,

I've been getting great help here, so here's another problem I've ran into.

I have been working towards proving a behavior that executes an HTTP request, so proving the serialization and deserialization of the data has been a main component of that. What I'm running into now is that a theorem that I've proven for nat is not being used to simplify a record that contains a nat value. Here's what I mean:

type_synonym http_data = string

record order =
  amount :: nat

fun deserialize :: "http_data ⇒ order" where
"deserialize d = ⦇ amount = (nat_of_string d) ⦈"

fun serialize :: "order ⇒ http_data" where
"serialize ord = string_of_nat (amount ord)"

(* This theorem has been successfully proven *)
theorem ser_deser: "nat_of_string (string_of_nat n) = n"

I would then expect to be able to prove this as follows:

lemma "deserialize (serialize order) = order"
  apply(cases order)
  apply(simp add: ser_deser)

This leaves me with the following goal:

 1. ⋀amount.
       order = ⦇amount = amount⦈ ⟹
       nat_of_string (map char_of (digit_list amount)) = amount

The map char_of ... is part of the definition of string_of_nat, but I was hoping that the simplifier would see nat_of_string (string_of_nat amount) and simplify that to amount, especially since I specified ser_deser as a simplification rule.

Is there something obvious to do here to discharge the goal, or are there some gotchas with using records?

Mathias Fleury (Nov 25 2021 at 14:19):

The problem is that string_of_nat is automatically unfolded to "map char_of" by the simplifier before using ser_deser. Not unfolding string_of_nat with "simp del: string_of_nat.simps" should do the trick.

Alex Weisberger (Nov 25 2021 at 14:32):

That is exactly the issue - ok. I'm definitely understanding a bit more what gets automatically applied and what should be added / removed explicitly. Thanks so much!

Notification Bot (Nov 25 2021 at 14:34):

Alex Weisberger has marked this topic as resolved.

Manuel Eberl (Nov 25 2021 at 14:37):

All the rules in the simp set get used for rewriting by the simplifier (i.e. simp, auto, force, fastforce) automatically. The fun and primrec commands add all the definitional rules that they create to the simpset by default. Other definitional commands (like definition, inductive) do not. This is because that is usually the kind of behaviour that you want: If you do a non-recursive definition, you are introducing that definition as a reason (to hide complexity). If you define a recursive function, you usually want the simplifier to break down things automatically.

Alex Weisberger (Nov 25 2021 at 15:08):

That's a great point about a non-recursive function hiding complexity. I went and changed both string_of_nat and serialize to definitions. Then I was able to prove via:

theorem "deserialize (serialize order) = order"
  apply(cases order)
  apply(simp add: serialize_def)
  done

Last updated: Apr 20 2024 at 08:16 UTC