Stream: Beginner Questions

Topic: How to "clean up" assumptions for related free variables?

Alex Weisberger (Nov 27 2021 at 20:13):

I have a theorem where the assumption is that certain values are related to each other. To elaborate, here are a few relevant records, type synonyms, and function types:

record order =
  amount :: nat

type_synonym orders = "order set"

record order_view = order +
  amount_view :: string

type_synonym state = orders

type_synonym view_state = "(order_view list * state)"

fun place_order_view :: "view_state ⇒ order_view ⇒ view_state"
fun place_order :: "orders ⇒ order ⇒ orders"
definition project :: "view_state ⇒ state

The theorem is then:

theorem "project (place_order_view (ovs, os) ov) = place_order os order"

And in order for this to hold, (amount ov) = (amount order) must be true. This is because I'm testing for semantic equivalence between place_order_view and place_order, so the input values must be the same. I encoded this as a proof assumption:

theorem
  assumes "(amount ov) = (amount order)"
  shows "project (place_order_view (ovs, os) ov) = place_order os order"

This isn't so bad in this tiny example, but I can imagine it getting unwieldy when there's a bunch of these relationships, or if the relationships involve some nested data. Are there any tips to improve this? I was thinking about explicitly writing out the quantification of variables, but that is discouraged in this post: https://proofcraft.org/blog/isabelle-style-part2.html. Maybe that's only true if the quantifications can be inferred correctly in simple cases?

If it helps, here's the full theory here: https://github.com/amw-zero/bakery_refinement/blob/master/FullstackBakery.thy. It's just something I've been playing around with, my goal is to model a typical web application as a refinement from a simple specification of the behavior. So the theorem I'm sharing here is relating an operation taken in the view layer to the abstract specification (the idea of "projecting" the view state to the abstract specification state type was taken from this paper on refinement in sel4.

Last updated: Apr 24 2024 at 04:17 UTC