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
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: Feb 08 2023 at 22:03 UTC