Stream: Equations devs & users

Topic: Use `with` matching conditions when proving obligations

view this post on Zulip Traian Florin Șerbănuță (Jul 20 2022 at 14:29):

I have a working Function definition and I'm having trouble converting it to using Equations. Any help is much appreciated.

Here is the original Function definition:

Function state_to_trace (s' : vstate X)
  { measure state_size } : vstate X * list (vtransition_item X) :=
  match state_destructor s' with
  | [] => (s', [])
  | (item, s) :: _ =>
    let (is, tr) := state_to_trace s in
    (is, tr ++ [item])

which generates the following goal:

 (s' : vstate X) (p : vtransition_item X * vstate X) (l : list (vtransition_item X * vstate X))
  (item : vtransition_item X) (s : vstate X),
  p = (item, s)  state_destructor s' = (item, s) :: l  state_size s < state_size s'

I'm trying to convert the above to Equations, and I came up with this definition:

Equations state_to_trace (s' : vstate X) :
  vstate X * list (vtransition_item X) by wf (state_size s') lt :=
state_to_trace s' with state_destructor s' :=
  state_to_trace s' [] => (s', []);
  state_to_trace s' ((item, s) :: _) =>
    let (is, tr) := state_to_trace s in
    (is, tr ++ [item])

I would expect to get a similar proof obligation as above, but instead the state_destructor equation is not among the hypotheses:

 s' : vstate X,
  vtransition_item X
    s : vstate X,
      list (vtransition_item X * vstate X)
       (∀ x : vstate X,
           state_size x < state_size s'
            vstate X * list (vtransition_item X))
         state_size s < state_size s'

Do you have any suggestions on how to rewrite the definition to make it work? Thanks!

view this post on Zulip Paolo Giarrusso (Jul 20 2022 at 14:32):

oh, you probably need the inspect pattern

view this post on Zulip Traian Florin Șerbănuță (Jul 20 2022 at 14:32):

I now see there was a similar question:

Last updated: Jan 29 2023 at 15:02 UTC