The Coq mailing list

[julien.forest AT ensiie.fr]

Hi Lars,

here is a version of your development using Function (which helps you
to deal with no structural functions).

Hope this helps,

Best regards,

Julien

On Mon, 08 Dec 2014 23:35:55 +0100
<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

Require Import Arith.
Require Import List.
Import ListNotations.
Require Import Recdef.
Function drop {T} n (l:list T) :=
  match n,l with
    | S n', cons _ l' => drop n' l'
    | O, _ => l
    | _, _ => nil
  end.

Lemma drop_lemma_le : forall {T} n (l:list T), length (drop n l) <= (length 
l).
Proof.
  intros; generalize n; induction l; intros; destruct n0; try reflexivity;
  apply le_S; apply IHl.
Defined.

Function pick (l: list nat) { measure length l } :=
  match l with
      nil => nil
    | cons a l' => cons a (pick (drop a l'))
  end.
Proof.
  intros l a l' teq.
  subst l.
  simpl.
  apply le_lt_n_Sm.
  apply drop_lemma_le.
Defined.  

Inductive zerolist : list nat -> Prop :=
| znil : zerolist nil
| hzlist : forall l, zerolist l -> zerolist (O::l).

(* We can prove our theorem if we have the lemma H *)
Theorem pickzero': (forall k, pick (0::k) = 0::pick k) ->
                forall l, zerolist l -> pick l = l.
Proof.
  intros H l H0; induction H0; [ | rewrite H; rewrite IHzerolist]; 
reflexivity.
Qed.

(* but trying to prove the lemma *)
Lemma pickzero_lemma : forall k, pick (0::k) = 0::pick k.
Proof.
  intros k.
  rewrite pick_equation.
  reflexivity.
Qed.