时间戳

首页 > 解决方案 > Coq：在假设或目标中使用“forall”重写

coq - Coq：在假设或目标中使用“forall”重写

问题描述

我已经证明了 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证明的归纳步骤中，如果我跳过intro k，然后用app_assoc重写会抱怨它找不到匹配的子项。

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

在这里，我假设? 在占位符名称之前表示这些术语受到约束，在这种情况下，对于某些类型T来说是List T类型；并且由于目标中的rev l'和[h]是List T的实例，因此人们会期望目标中的匹配项。

另一方面，使用归纳假设（rewrite -> IHl'）而不是app_assoc进行重写，而不需要之前的介绍 k。

我发现这种重写行为有点令人困惑，并且 Coq 手册没有提供任何细节。我不想通读实现，但我需要对重写策略的作用有一个很好的操作理解，特别是关于术语匹配的工作原理。高度赞赏这个方向的任何答案/参考。

标签： coqcoq-tactic

解决方案

这种重写的复杂之处在于有一个活页夹（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 参考手册中的活页夹下的重写）。手册告诉你需要声明态射，但在这种情况下，相关的都已经为你实现了 for forall，所以setoid_rewrite app_assoc就可以了。

请注意，虽然您总是可以引入 aforall来摆脱活页夹，setoid_rewrite但当您的目标是exists. 而不是使用eexists你可以在活页夹下重写。

推荐阅读