Felipe (Jun 23 2021 at 23:31): Felipe (Jun 23 2021 at 23:31):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?
Li-yao (Jun 24 2021 at 15:14):It might be good to share the code where the above goal occurs. Does that happen before or after defining queue_dump_all?
Felipe (Jun 24 2021 at 16:11):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.
Felipe (Jun 24 2021 at 16:37):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
Paolo Giarrusso (Jun 27 2021 at 01:49):I'm used to hearing as fuel, but yes I've seen this before, mostly without guarantees on the needed fuel.
Matthieu Sozeau (Jun 29 2021 at 12:25):@Felipe I posted a solution that avoids dependent rewrites
Last updated: Oct 13 2024 at 01:02 UTC