Coq中build_goal_aux相关定理证明思路线索求助

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.

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 <> [].

先理清函数实际行为 #

先搞懂两个函数的执行逻辑，这是找证明方向的关键：

• build_goal_aux acc n：当n=0时直接返回acc；当n是S n'时，把当前的n放到acc的最前面，再递归处理n'。比如build_goal_aux [e] 3最终会生成[3,2,1,e]。
• last l：递归取列表最后一个元素——空列表返回None，单元素列表返回该元素的Some包装，多元素列表就递归取尾列表的最后一个元素。

针对 build_goal_aux_last 的证明提示 #

对n做归纳是正确的选择，分两步走：

• 基础情况（n=0）：直接展开build_goal_aux [e] 0，得到[e]，再展开last [e]，结果就是Some e，等式直接成立。
• 归纳步骤（n=S n'）：先写出归纳假设：对任意e，last (build_goal_aux [e] n') = Some e。现在要证last (build_goal_aux [e] (S n')) = Some e。先展开build_goal_aux的递归定义，build_goal_aux [e] (S n')等于build_goal_aux (S n' :: [e]) n'。接下来你需要分析：last作用在x :: l上的结果，和last l的结果有什么关联？结合归纳假设里last l的结论，就能推导出最终结果。（如果不确定这个关联，可以手动写个小引理证明，或者在当前证明里直接展开last的定义一步步推导）

针对 build_goal_aux_never_nil 的证明提示 #

同样对n做归纳：

• 基础情况（n=0）：展开build_goal_aux [0] 0得到[0]，显然[0]不等于空列表，直接得证。
• 归纳步骤（n=S n'）：归纳假设是build_goal_aux [0] n' <> []。现在看build_goal_aux [0] (S n')，根据函数定义，它等于build_goal_aux (S n' :: [0]) n'。这里要注意：不管递归后的结果是什么，这个列表的最前面已经有一个元素S n'了——只要列表有首元素，就不可能是空列表。或者结合归纳假设，build_goal_aux [0] n'非空，那么在它前面加一个元素后的列表肯定也非空，直接得出结论。

内容的提问来源于stack exchange，提问作者Lepticed