Stream: Beginner Questions

Topic: Simplification rules not applying to records

view this post on Zulip 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?

Last updated: Jul 15 2022 at 23:21 UTC