Stream: Equations devs & users

Topic: Use `with` matching conditions when proving obligations

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])
end.
``````

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!

Paolo Giarrusso (Jul 20 2022 at 14:32):

oh, you probably need the `inspect` pattern

Traian Florin Șerbănuță (Jul 20 2022 at 14:32):

I now see there was a similar question: https://coq.zulipchat.com/#narrow/stream/237659-Equations-devs-.26-users/topic/getting.20equalities.20out.20of.20with.20clauses
:-)

Last updated: Jun 13 2024 at 04:03 UTC