Stylistic advice for logic involving partial functions · General

I'm finding that working with partial functions (Maps) is convenient, because I can place constraints on the domain and range of the functions via Map.graph, e.g. I've defined well-typedness of a step function on a permissive state type as:

definition "well_typed stp = (∀(s, s') ∈ Map.graph stp. dom s = dom s')"

One issue that comes up is that working with partial functions leads to a lot of case statements in the logic, which corresponds to a lot of nested cases applications in proofs. While this works, it feels like I'm brute-forcing things, and seems inelegant. case_option cleans things up a little bit, but still leads to a lot of nesting.

So, I was wondering if there was any helper functions / proof methods for this that I'm not aware of.

definition "local_simulates afl am_i am_m e s = (
  let istp = step (am_i e) in
  let mstp = step (am_m e) in
  let impl_start = (Get (lens (am_i e))) s in

  case_option True (λms.
    let model_start = (Get (lens (am_m e))) ms in
    (case_option True (λir.
      (case_option True (λmr.
        afl ir  = Some mr)
        (mstp model_start)))
    (istp impl_start)))

    (afl impl_start))"

I'm working on some state machine simulation proofs and here the step functions of two SMs are partial functions, and the abstraction function between states is also partial. So there's three nested case_options and three corresponding cases method application in the proof.

Lukas Stevens (Oct 08 2023 at 13:48):

Alex Weisberger (Oct 08 2023 at 13:56):

How does that work with Options? Because a default value needs to be specified for the None case.

Lukas Stevens (Oct 08 2023 at 13:58):

You can use a function such as the_default a opt = (case opt of None => a | Some b => b)

Lukas Stevens (Oct 08 2023 at 13:59):

Lukas Stevens (Oct 08 2023 at 14:00):

Alex Weisberger (Oct 08 2023 at 23:02):

Do you have a link to any theories that use the monad syntax? I'm having trouble getting mine to parse after importing the HOL-Library.Monad_Syntax theory.

Lukas Stevens (Oct 09 2023 at 09:09):

I don't have a good example at hand. In general you replace let _ = _ in with let _ = _; and case_option True (λx. t) s with x ← s; t; and then wrap the whole thing in the_default True in the end.

Stream: General

Topic: Stylistic advice for logic involving partial functions