The Coq mailing list

[Lars Rasmusson SICS <Lars.Rasmusson AT sics.se>]

Thank you!
That was really enlightening, both the part about proof_irrel and the
use of patten matching tactics!
And a really nice proof.
Thanks again!

On Tue, Dec 9, 2014 at 12:03 AM, James Wilcox <wilcoxjay AT gmail.com> wrote:

Here is one solution. The basic idea is to prove a lemma describing how picksome processes a cons. With a normal function, simpl would give you this, but here the Acc argument makes things ugly so it's best to wrap it up as a lemma. Then you can prove that picksome doesn't depend on the proof term. Your lemma follows.

https://gist.github.com/wilcoxjay/599da596ca3575d5515f

James

On Mon, Dec 8, 2014 at 2:35 PM, <lars.rasmusson AT sics.se> wrote:

Salut à tous!

I'm trying to understand how to work with recursive functions where I have to
use Acc to prove termination, and I made a small example function, "pick".

"pick" takes a "list nat" that starts with "n", then drops the "n" following
elements, and then does "picksome" on the rest.

 I.e. pick [1,2,3,4,5] = [1,3]

(take the "1", then drop 1 (i.e. drop the "2"), then take the "3" , drop the
next 3 items, i.e the "4" and "5", and then end)

I am able to prove that the function terminates alright, but I want to prove a
lemma that given a list of all zeros, picksome will return the same list:
forall l, allzeros l -> picksome l = l.
(take the first zero, drop zero elements, take the next zero, drop zero
elements, ......)

However, the proof of this lemma gets all tangled upp with the Accesibility
term, and it quickly gets out of hand.  How should one structure this kind of
proof to make it feasible, and so that I don't have to deal with the Acc term
(which ideally should be irrelevant for the proof)?

I posted a small development here
https://gist.github.com/larsr/3a4f8997e5ad0d6d98e0

I'd be very thankful for an example proof, either using my formulation (which
is intended to be close to how I would write the function in Ocaml, or perhaps
structured differently, if it makes the proving easier.

Thanks!
/Lars