展开后向后折叠

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 (fun (_ : X) (n0 : nat) => S n0) l' 0)为fold_length l'使用fold_length. 有没有办法在 Coq 中做到这一点（在 Coq 中似乎有一种名为foldtactic 的东西。可以做到这一点。）？

另外，有没有办法在不使用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这里。