展开后向后折叠

Question

我 fold_length 定义如下：

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.

我必须证明一个定理，这是我目前的代码：

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.

现在，我的目标是这样的：

  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')

现在我想使用 fold_length 的定义将表达式 (fold (fun (_ : X) (n0 : nat) => S n0) l' 0) 转换为 fold_length l'。有没有办法在 Coq 中做到这一点（Coq 中似乎有一种名为 fold 的策略。可以实现这一点。）？

另外，有没有不使用unfold和fold策略来证明上述定理的方法？

Answer 1

要回答您的第一个问题，是的，可以在此处使用 fold 策略将等式的左侧替换为 S (fold_length l')。通常，对于函数 f，fold f 不够强大，无法检测到它可以折叠的内容。但是，如果您指定整个术语，就像这里 fold (fold_length l')，它会起作用。

关于你的第二个问题，请注意，如果所涉及的术语等于某些简化，则像 reflexivity 或 assumption 这样的策略可以得出结论。这里，归纳的基本情况可以只是 reflexivity。对于第二种情况，假设 fold 是 List.fold_right，simpl 可以令人惊讶地简化而不展开，并且您在这里也不需要 unfold 或 fold。

展开后向后折叠

Folding back after unfolding

coq