I posted on SO yesterday about this queue I'm trying to specify, and have made some small progress. The `dump_all`

function is challenging to work with because it uses wf recursion, so any time I try to rewrite the measure (e.g., for induction) I hit dependent errors of the sort described in this question "Dependent type error in rewrite of ...", which I gather is because WF recursion requires passing around proof terms which aren't amenable to rewriting.

E.g., with this goal, I'd like to rewrite using `q1_len`

, but that would require simultaneously updating the `eq_refl`

proof term. Is there a way of achieving this? Or am I stuck in a dead end? fiddle

```
A : Type
q1, q2 : queue_type A
elt : A
dequeue_some : (dequeue q1).2 = Some elt
n : nat
q1_len : queue_length q1 = S n
============================
queue_dump_all_eq_clause_1_worker q1 (exist (fun q : queue_type A => queue_length q = queue_length q1) q1 erefl) [] =
queue_dump_all_eq (dequeue q1).1 ++ [elt]
```

Just to be sure, is it intentional to define `queue_dump_all`

by recursion instead of just `back ++ rev front`

?

It might be good to share the code where the above goal occurs. Does that happen before or after defining `queue_dump_all`

?

Yes it's intentional. JsCoq is complaining about something else, and I don't have the code anymore. But it happens after the definition of `queue_dump_all`

, where I'm proving that you just get `back ++ rev front`

.

I actually managed to solve this by moving to a weak specification and getting the proof terms out of the function altogether: https://stackoverflow.com/a/68119220/754254. Would be curious to know if using the `gas`

argument is common -- didn't see it anywhere online so might write it up

I'm used to hearing as fuel, but yes I've seen this before, mostly without guarantees on the needed fuel.

@Felipe I posted a solution that avoids dependent rewrites

Last updated: Jun 16 2024 at 01:42 UTC