Prove equality on list constructed with a map

Question

I have two lists, one constructed directly by recursion and the other constructed using a map operation. I'm trying to show they are equal, and surprisingly I got stuck.

Require Import Coq.Lists.List.
Import ListNotations.

Fixpoint ls_zeroes n :=
  match n with
  | 0 => nil
  | S n' => 0 :: ls_zeroes n'
  end.

Fixpoint ls_ones n := map S (ls_zeroes n).
Fixpoint ls_ones' n :=
  match n with
  | 0 => nil
  | S n' => 1 :: ls_ones' n'
  end.

Goal forall n, ls_ones n = ls_ones' n.
Proof.
  intros.
  induction n.
  - reflexivity.
  - simpl. f_equal. (* ??? *)
Abort.

This is what the context looks like:

1 subgoal
n : nat
IHn : ls_ones n = ls_ones' n
______________________________________(1/1)
map S (ls_zeroes n) = ls_ones' n

I thought fold ls_ones would map S (ls_zeroes n) into ls_ones n since that's literally the definition of ls_ones but it does nothing. If I try to unfold ls_ones in IHn I get a nasty recursive expression instead of the verbatim definition of ls_ones.

What is the cleanest way to complete this proof?

Answer 1

I thought fold ls_ones would map S (ls_zeroes n) into ls_ones n since that's literally the definition of ls_ones

Is it? You said Fixpoint ls_ones, not Definition. Just like any Fixpoint, this means that the given definition of ls_ones is transformed into a fix. There's no recursive structure in the definition given, so this is pointless, but you said to do it, so Coq does it. Issue Print ls_ones. to see the actual definition. The true solution is to make ls_ones a Definition.

If you don't fix that, Coq will only reduce a Fixpoint if the recursive argument(s) start with constructors. Then, in order to complete this proof, you need to destruct n to show those constructors:

Goal forall n, ls_ones n = ls_ones' n.
Proof.
  intros.
  induction n.
  - reflexivity.
  - simpl. f_equal. destruct n; assumption.
Qed.