Stream: Coq users

Topic: Two-sided queue


view this post on Zulip 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]

view this post on Zulip Li-yao (Jun 24 2021 at 15:13):

Just to be sure, is it intentional to define queue_dump_all by recursion instead of just back ++ rev front?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Jun 29 2021 at 12:25):

@Felipe I posted a solution that avoids dependent rewrites


Last updated: Feb 08 2023 at 22:03 UTC