为什么反转策略在下面的Coq证明中不起作用？

Question

Require Import FMapAVL.
Require Import OrderedTypeEx.

Module M := FMapAVL.Make(Nat_as_OT).
Fixpoint cc (n: nat) (c: M.t nat):bool :=
  match M.find n c with
  | None => false
  | Some e => true
  end.

Lemma l: forall (n: nat) (k:nat) (m: M.t nat), cc n m = true  -> cc n (M.add k k m) = true.
Proof.
  intros.
  inversion H.

调用inversion H之前的环境

1 subgoals
n : nat
k : nat
m : M.t nat
H : cc n m = true
______________________________________(1/1)
cc n (M.add k k m) = true

根据我对反转策略的理解，使用策略inversion H，应该能够预测M.find n m = Some e。但它只是复制了H。

有人能帮我解释一下Coq是怎么解释这里的吗？

Answer 1

当假设的主要谓词是归纳谓词时，反转工作。在这里，假设H的主要谓词是相等，其深层的等式由一个归纳谓词来表示。所以inversion认为它可以工作。

直观地说，inversion试图帮助您推理可以使用什么构造函数，这种推理是通过添加相等的语句来完成的，这些语句对应于当使用这个构造函数来证明假设时必须满足的约束条件。

在您的情况下，等式由一个只有一个构造函数的归纳定义表示。因此，inversion研究了使用此构造函数的约束是什么:等式的两个成员应该是相同的。因此，inversion添加了一个新的等式，说明等式的两边应该是相同的。这就是为什么你会看到这个假设的重复。

碰巧的是，inversion不是这里使用的正确策略。

在前面对其中一个your questions的回答中，我写道，您不应该使用Fixpoint来定义函数cc，因为这个函数不是递归的。请遵照我的建议写信

Definition cc (n: nat) (c: M.t nat):bool :=
match M.find n c with
| None => false
| Some e => true
end.

这将使其余的证明更容易(我们也可以用使用cc定义的Fixpoint来解决您的问题，但它增加了不必要的复杂性)。我对你问题的回答现在假设你确实遵循了这条建议。这是如何在你的证据方面取得进展。

Proof.
intros n k m H; unfold cc in H.

此时，假设H包含模式匹配语句和true之间的相等。您需要的是通过在证明中执行相同的案例分析来研究此match语句的两种可能的计算。以下是如何做这件事。

case_eq (M.find n m); [intros v Hfind | intros Hfind].

在此之后，你将有两个目标。一个是H : match ... with ... end = true和Hfind : M.find n m = Some v，另一个是H : match M.find n m with ... end = true和Hfind : M.find n m = None。使用Hfind在H中重写，您将将假设转换为H : false = true，这将使用discriminate解决。以后要记住这一点。

对于第一个目标，您应该能够通过unfold cc再次取得进展。

那么M.find n (M.add k k m)的价值是什么呢？如果n是k，则此值为Some k。如果n与k不同，则M.find n (M.add k k m)的值与M.find n m的值相同。我们已经给这个值取了一个名字，这个名字是v，假设Hfind是这么说的。

为了对n是否等于k进行案例分析，我建议您编写destruct (M.E.eq_dec k n) as [kn | knn]。

因此，你将有一个假设kn : k = n的第一个目标。在这种情况下，我建议您通过输入以下命令来证明一个中间事实。

assert (step : M.find n (M.add k k m) = Some k).

您应该能够使用M.find_1，M.add_1来证明这一点。

一旦你完成了这个证明，用step重写，然后结束。

然后你将有一个假设knn : k <> n的第二个目标，对于这个目标，你必须证明一个不同的中间陈述，你再次使用M.find_1来证明，但是你使用M.add_2和M.find_2。