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