Folding back after unfolding

Question

I have fold_length defined like this:

Inductive list (X: Type) : Type :=
  | nil : list X
  | cons : X -> list X -> list X.

Arguments nil {X}.
Arguments cons {X} _ _.

Notation "x :: y" := (cons x y)
                     (at level 60, right associativity).
Notation "[ ]" := nil.

Fixpoint fold {X Y:Type} (f: X -> Y -> Y) (l:list X) (b:Y) : Y :=
  match l with
  | nil => b
  | h :: t => f h (fold f t b)
  end.

Definition fold_length {X : Type} (l : list X) : nat :=
  fold (fun _ n => S n) l 0.

I have to prove a theorem and this is my code so far:

Theorem fold_length_correct : forall X (l : list X),
  fold_length l = length l.
Proof.
  intros X l.
  induction l as [| n l' IHl'].
  - simpl.
    unfold fold_length.
    simpl.
    reflexivity.
  - simpl.
    unfold fold_length.
    simpl.

Right now, my goal looks like this:

  X : Type
  n : X
  l' : list X
  IHl' : fold_length l' = length l'
  ============================
   S (fold (fun (_ : X) (n0 : nat) => S n0) l' 0) = S (length l')

Now I want to convert the expression (fold (fun (_ : X) (n0 : nat) => S n0) l' 0) to fold_length l' using the definition of fold_length. Is there a way to do that in Coq (There seems to something named fold tactic in Coq. Can that achieve this.) ?

Also, is there a way to prove the above theorem without the usage of unfold and fold tactic ?

You can either rewrite to the right now rewrite <- IHl' or use an aux lemma: Lemma fold_lengthE {X : Type} (l : list X) : fold_right (fun _ n => S n) 0 l = fold_length l. Proof. now trivial. Qed. then rewrite using it. — ejgallego
@ejgallego Thanks. So something like fold cannot be used here ? — Sibi
What is fold? AFAICT it's not in the stdlib. Please provide a self-contained example (with the right imports & definitions). — gallais
@Sibi as answered below, fold is usually not powerful enough to work well in most cases, YMMV, but usually one want to prevent unfolding itself instead of refolding. Controlling reduction is a bit complex in Coq, you can use simpl flags (see the manual) or deploy some other custom solution like mathcomp's nosimpl. — ejgallego
@ gallais Thanks, I have made it self-contained now. @ejgallego Thanks for the valuable input. — Sibi

eponier eponier · Accepted Answer · 2017-03-22T09:43:07

To answer your first question, yes, the fold tactic can be used here to replace the left side of the equality with S (fold_length l'). Usually, for a function f, fold f is not powerful enough to detect what it can fold. But if you specify the whole term, like here fold (fold_length l'), it works.

Regarding your second question, note that tactics like reflexivity or assumption can conclude if the terms involved are equal up to some simplifications. Here, the base case of the induction can be just reflexivity. For the second case, assuming that fold is List.fold_right, simpl can surprisingly simplify without unfolding and you should not need unfold or fold here either.

Folding back after unfolding

1 Answers