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!

oh, you probably need the `inspect`

pattern

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: Oct 13 2024 at 01:02 UTC