Coq:在假设或目标中用'forall'重写

Question

我已经证明了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 l3 : list T),
  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
Admitted.

Theorem rev_acc_correct : forall (T:Type) (l k :list T),
  rev l ++ k = rev_acc l k.
Proof.
  intros T l.
  induction l as [ | h l' IHl' ].
  - reflexivity.
  - simpl. 
    intro k.
    (* Why is "intro k" required for "rewrite -> app_assoc" *)
    (* But "rewrite -> IHl'" works regardless of "intro k".  *)
    (* generalize (rev l'), [h], k. *)
    rewrite -> app_assoc.
    simpl.
    rewrite -> IHl'.
    reflexivity.
Qed.

在rev_acc_correct的证明的归纳步骤中,如果我跳过介绍k,那么用app_assoc重写会抱怨它无法找到匹配的子项.

Found no subterm matching "(?M1058 ++ ?M1059) ++ ?M1060" in the current goal.

在这里,我认为是？在占位符名称之前表示术语是受约束的,在这种情况下,对于某些类型T,其类型为List T ; 并且由于目标中的rev l'和[h]是List T的实例,因此可以预期目标中的匹配.

另一方面,使用归纳假设(重写 - > IHl')而不是app_assoc进行重写,而不需要前面的介绍k.

我发现这种重写行为有点令人困惑,Coq手册没有提供任何细节.我不想阅读实现,但我需要对重写策略的作用有一个良好的操作理解,特别是关于术语匹配如何工作.任何在这个方向的答案/参考都非常感谢.

Answer 1

这种重写的复杂之处在于有一个绑定器(the forall k),它可以使事情复杂化.如果你只想让事情发挥作用,请使用setoid_rewrite而不是,rewrite它会在粘合剂下重写.

• rewrite IHl'看起来它发生在绑定器下,但重写的模式实际上并不涉及绑定变量,因此绑定器实际上并不重要.这就是我的意思:目标是

  forall k : list T, (rev l' ++ [h]) ++ k = rev_acc l' (h :: k)
  

  这与(即等于)相同:

   (fun l : list T => forall k : list T, l ++ k = rev_acc l' (h :: k)) (rev l' ++ [h])
  

  我pattern (rev l' ++ [h])在Ltac中使用过.现在很明显,您可以只重写正在应用的部分并忽略活页夹.当你做rewrite IHl'Coq时,很容易发现IHl应该是专门的[h]并且重写继续进行.

• rewrite app_assoc,而另一方面,需要专业化三个名单,特别是rev l',[h]和k.它不能专门用于当前上下文,因为变量k仅绑定在下面forall.这就是为什么模式(?x ++ ?y) ++ ?z没有出现在目标中的原因.

那你究竟做了什么？你当然可以介绍k所以没有绑定器,但是有一种更简单,更通用的技术:Coq具有可以在绑定器下重写的通用重写,你可以使用它来代替调用setoid_rewrite(参见Coq参考手册中的重写器下的重写).手册告诉你需要声明态射,但在这种情况下相关的已经为你实现了forall,所以setoid_rewrite app_assoc只会工作.

请注意,虽然你可以随时介绍一个forall摆脱活页夹,setoid_rewrite但当你的目标是一个时,可以非常方便exists.而不是使用eexists你可以只在绑定器下重写.