小编Aka*_*kay的帖子

我已经证明了Coq中多态列表的反函数的"正确性" .以下证明工作正常,但我有一些关于重写策略如何工作的问题.

这是代码:

Require Export Coq.Lists.List.
Import ListNotations.

Fixpoint rev {T:Type} (l:list T) : list T :=
  match l with
  | nil    => nil
  | h :: t => rev t ++ [h]
  end.

(* Prove rev_acc equal to above naive implementation. *)
Fixpoint rev_acc {T:Type} (l acc:list T) : list T :=
  match l with
  | nil => acc
  | h :: t => rev_acc t (h::acc)
  end.

Theorem app_assoc : forall  (T:Type) (l1 l2 …