Prove theorem about the last element of a list

I’ve two functions build_goal_aux and last defined like this:

Require Import List.
Import ListNotations.

Fixpoint build_goal_aux (acc:list nat)(n:nat) : list nat :=
  match n with
  | O => acc
  | S n' => build_goal_aux (n::acc) n'
  end.

Fixpoint last (l:list nat) : option nat :=
  match l with
    | [] => None
    | a :: [] => Some a
    | _ :: l => last l
  end.

I would to prove some theorem about build_goal_aux, such as:

Lemma build_goal_aux_last : forall n e, last (build_goal_aux [e] n) = Some e.
Lemma build_goal_aux_never_nil : forall (n:nat), build_goal_aux [0] n <> [].

But I have no clues about how to do it. I tried an induction on n, but I don’t know how to finish the proof. I still want to try to prove it myself, so I don’t want a complete solution, but some clues would be great.

Solution

Both of your lemmas are too specific. Let's see what happens when we try to do induction:

Lemma build_goal_aux_last : forall n e, last (build_goal_aux [e] n) = Some e.
Proof.
  intros n.
  induction n.
  - easy.
  - intros e.
    simpl.
    (*
      n : nat
      IHn : forall e : nat, last (build_goal_aux [e] n) = Some e
      e : nat
      ============================
      last (build_goal_aux [S n; e] n) = Some e
    *)
Abort.

We see that our induction hypothesis talks about build_goal_aux [e] n and our goal talks about build_goal_aux [S n; e] n, so there is no way that the induction hypothesis is going to be useful. The way out is to generalize the lemma so that it holds for every list given to build_goal_aux, and then derive your desired result as a corollary.

What does the lemma try to say? That as long as the aux list is non-empty, the last element of build_goal_aux aux n is already predetermined regardless of n. One way to write this is:

Lemma build_goal_aux_last : forall n e w,
  last (build_goal_aux (e :: w) n) = last (e :: w).

(Note that I chose to implement "aux is non-empty" as e :: w instead of as aux <> [], which is ultimately a design choice. I prefer this version but YMMV.)

Now the induction hypothesis is actually useful, and your original lemma is obviously a corollary.

The problem with your second lemma is the same and has a similar solution.

This pattern of generalizing a lemma in order to make it provable by induction pops up a lot when you have a recursive definition decreasing on something (a nat in this case) that modifies some other argument of the function (a list nat in this case). You typically need statements that are fully general in the non-decreasing arguments in order to obtain strong-enough induction hypotheses.