How to make Coq evaluate a specific redex (or - why does it refuse in this case?)

Question

When I am trying to prove a theorem about a recursive function (see below), I end up at a reducible expression

(fix picksome L H := match A with .... end) L1 H1 = RHS

I would like to expand the match expression, but Coq refuses. Doing simpl just expands the right hand side into an unreadable mess. Why is Coq not able to finish the proof with simpl; reflexivity, and how should instruct Coq to expand precisely the redex, and finish the proof ?

The function is a recursive function pick that takes a list nat and takes the first nat called a, drops the following a items from the list, and recurses on the remaining list. I.e.

pick [2;3;4;0;1;3])=[2; 0; 1]

The theorem I'm trying to prove is that the function 'does nothing' on lists that only contains zeroes. Here is the development that leads up to the problem:

Require Import Arith.
Require Import List.
Import ListNotations.

Fixpoint drop {T} n (l:list T) :=
  match n,l with
    | S n', cons _ l' => drop n' l'
    | O, _ => l
    | _, _ => nil
  end.

The first lemma:

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.

Second lemma:

Lemma picksome_term: forall l l' (a :nat),
       l = a::l' -> Acc lt (length l) ->  Acc lt (length (drop a l')).
Proof.
  intros; apply H0; rewrite H; simpl; apply le_lt_n_Sm; apply drop_lemma_le.
Defined.

A few more definitions:

Fixpoint picksome (l:list nat) (H : Acc lt (length l)) {struct H}: list nat :=
  match l as m return l=m -> _ with
    | nil       => fun _  => nil
    | cons a l' => fun Hl =>
                     cons a (picksome (drop a l')
                                      (picksome_term _ _ _ Hl H))
  end
    (eq_refl _).

Definition pick (l:list nat) : list nat := picksome l (lt_wf (length l)).

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

Now, 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.
  induction k; try reflexivity.
  unfold pick at 1.
  unfold picksome.

This is the goal and context:

a : nat
k : list nat
IHk : pick (0 :: k) = 0 :: pick k
============================
 (fix picksome (l : list nat) (H : Acc lt (length l)) {struct H} :
    list nat :=
    match l as m return (l = m -> list nat) with
    | [] => fun _ : l = [] => []
    | a0 :: l' =>
        fun Hl : l = a0 :: l' =>
        a0 :: picksome (drop a0 l') (picksome_term l l' a0 Hl H)
    end eq_refl) (0 :: a :: k) (lt_wf (length (0 :: a :: k))) =
 0 :: pick (a :: k)

Answer 1

@Vinz explained the reason why Coq does not reduce a beta-redex with fix. Here is also a relevant excerpt from CDPT:

One candidate rule would say that we apply recursive definitions wherever possible. However, this would clearly lead to nonterminating reduction sequences, since the function may appear fully applied within its own definition, and we would naively "simplify" such applications immediately. Instead, Coq only applies the beta rule for a recursive function when the top-level structure of the recursive argument is known.

I just wanted to add that the lemma can be proved without assuming additional axioms -- simple generalization would suffice.

Let's start by defining a new induction principle for lists:

Definition lt_list {A} (xs ys : list A) := length xs < length ys.

Definition lt_list_wf {A : Type} : well_founded (@lt_list A) :=
  well_founded_ltof (list A) (@length A).

Lemma lt_list_wf_ind {A} (P : list A -> Prop) :
  (forall ys, (forall xs, length xs < length ys -> P xs) -> P ys) ->
  forall l, P l.
Proof. intros ? l; elim (lt_list_wf l); auto with arith. Qed.

Essentially, the lt_list_wf_ind induction principle says that if we can prove a predicate P holds for a list ys under the assumption that P holds for all lists of lesser lengths, then we have P for all lists.

Now, let's prove a lemma that expresses proof-irrelevance of the accessibility parameter of picksome:

Lemma picksome_helper l : forall acc acc',
  picksome l acc = picksome l acc'.
Proof.
  induction l as [l IH] using lt_list_wf_ind; intros acc acc'.
  destruct l; destruct acc, acc'; [trivial |].
  simpl. f_equal.
  apply IH.
  simpl; rewrite Nat.lt_succ_r.
  apply drop_lemma_le.
Qed.

Using this local version of proof-irrelevance of Acc we can now prove the pick_zero lemma:

Lemma pick_zero k : pick (0::k) = 0::pick k.
Proof.
  unfold pick.
  destruct (lt_wf (length (0 :: k))).
  simpl (picksome (0 :: k) _).
  f_equal.
  apply picksome_helper.
Qed.

Answer 2

Coq's reduction rules about fixpoint is quite simple: you can unfold a step of a fixpoint if and only if the fixpoint is applied to a "constructed" term. For example length (1 :: nil) will reduce, but in the context were l = 1 :: nil, length l will not reduce. You have to explicitly replace l by the constructed term 1 :: nil to enable reduction to append.

In your goal, picksome is defined by structural recursion on H, the accessibility proof. If you try to simpl, reduction actually happens, and stops when this argument is no longer "constructed". In your particular case, after a simpl you end up with a (fix picksome ...) (drop a1 l'0) (nat_ind <big term>) proof, and Coq can't reduce picksome anymore.

EDIT: to finish your proof, I tried first to prove:

Lemma picksome_unfold : 
  forall (hd:nat) (tl:list nat) (H:Acc lt (length (hd::tl))), picksome (hd::tl) H = 
    cons hd (picksome (drop hd tl) (picksome_term (hd::tl) tl hd (eq_refl (hd::tl)) H)).

(which is quite easy if you destruct H). However to finish the pickzero_lemma lemma, I need to prove equality of the accessibility proof, which might require proof irrelevance. I'm not sure, sorry.