The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 08/12/2014 23:35, 
lars.rasmusson AT sics.se
 wrote:
> 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.

(Warning: maybe off topic?)

Dunno if that counts as a change of formulation, but you can just get
rid of the Acc function in this particular case:

Fixpoint pick (l : list nat) : list nat := match l with
| nil => nil
| cons n l =>
  let fix F (n : nat) (l : list nat) {struct l} := match n with
  | 0 => pick l
  | S n =>
    match l with
    | nil => nil
    | cons _ l => F n l
    end
  end in
  cons n (F n l)
end.

I know that defeats the purpose of using accessibility proofs, but
that's always better not to rely on them when you do not have to...

PMP

Attachment: signature.asc
Description: OpenPGP digital signature