如何在 Coq 中使用归纳类型来处理案例

发布于 2024-11-26 10:32:07 字数 837 浏览 1 评论 0原文

我想使用destruct策略通过案例来证明一个陈述。我在网上读了几个例子，但我很困惑。有人可以更好地解释一下吗？

这是一个小例子（还有其他方法可以解决它，但尝试使用 destruct）：

 Inductive three := zero 
                  | one 
                  | two.
 Lemma has2b2: forall a:three, a<>zero /\ a<>one -> a=two.

现在一些在线示例建议执行以下操作：

intros. destruct a.

在这种情况下我得到：

3 subgoals H : zero <> zero /\ zero <> one
______________________________________(1/3) 
zero = two

______________________________________(2/3) 
one = two

______________________________________(3/3) 
two = two

所以，我想证明第一个两种情况是不可能的。但机器将它们列为子目标并希望我证明它们......这是不可能的。

概括：如何准确剔除不可能的情况？

我看过一些使用 inversion 的例子，但我不明白这个过程。

最后，如果我的引理取决于几种归纳类型并且我仍然想涵盖所有情况，会发生什么？

原文

I wan to use the destruct tactic to prove a statement by cases. I have read a couple of examples online and I'm confused. Could someone explain it better?

Here is a small example (there are other ways to solve it but try using destruct):

 Inductive three := zero 
                  | one 
                  | two.
 Lemma has2b2: forall a:three, a<>zero /\ a<>one -> a=two.

Now some examples online suggest doing the following:

intros. destruct a.

In which case I get:

3 subgoals H : zero <> zero /\ zero <> one
______________________________________(1/3) 
zero = two

______________________________________(2/3) 
one = two

______________________________________(3/3) 
two = two

So, I want to prove that the first two cases are impossible. But the machine lists them as subgoals and wants me to PROVE them... which is impossible.

Summary:
How to exactly discard the impossible cases?

I have seen some examples using inversion but I don't understand the procedure.

Finally, what happens if my lemma depends on several inductive types and I still want to cover ALL cases?

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

温柔一刀 2024-12-03 10:32:07

如何排除不可能的情况？嗯，确实，前两项义务无法证明，但请注意，它们具有相互矛盾的假设（分别是零<>零和一<>一 ）。因此，您将能够使用 tauto 来证明这些目标（如果您感兴趣，还有更原始的策略可以实现这一点）。

inversion 是 destruct 的更高级版本。除了“破坏”归纳法之外，它有时还会生成一些等式（您可能需要）。它本身是归纳的简单版本，它还会为您生成归纳假设。

如果您的目标中有多种归纳类型，您可以将它们一一解构/反转。

更详细的演练：

Inductive three := zero | one | two .

Lemma test : forall a, a <> zero /\ a <> one -> a = two.
Proof.
  intros a H.
  destruct H. (* to get two parts of conjunction *)
  destruct a. (* case analysis on 'a' *)
(* low-level proof *)
  compute in H. (* to see through the '<>' notation *)
  elimtype False. (* meaning: assumptions are contradictory, I can prove False from them *)
  apply H.
  reflexivity.
(* can as well be handled with more high-level tactics *)
  firstorder.
(* the "proper" case *)
  reflexivity.
Qed.

How to discard impossible cases? Well, it's true that the first two obligations are impossible to prove, but note they have contradicting assumptions (zero <> zero and one <> one, respectively). So you will be able to prove those goals with tauto (there are also more primitive tactics that will do the trick, if you are interested).

inversion is a more advanced version of destruct. Additional to 'destructing' the inductive, it will sometimes generate some equalities (that you may need). It itself is a simple version of induction, which will additionally generate an induction hypothesis for you.

If you have several inductive types in your goal, you can destruct/invert them one by one.

More detailed walk-through:

Inductive three := zero | one | two .

Lemma test : forall a, a <> zero /\ a <> one -> a = two.
Proof.
  intros a H.
  destruct H. (* to get two parts of conjunction *)
  destruct a. (* case analysis on 'a' *)
(* low-level proof *)
  compute in H. (* to see through the '<>' notation *)
  elimtype False. (* meaning: assumptions are contradictory, I can prove False from them *)
  apply H.
  reflexivity.
(* can as well be handled with more high-level tactics *)
  firstorder.
(* the "proper" case *)
  reflexivity.
Qed.

回复收藏 0 原文

两个我 2024-12-03 10:32:07

如果您看到一个不可能的目标，则有两种可能性：要么您在证明策略中犯了错误（也许您的引理是错误的），要么假设是矛盾的。

如果您认为这些假设是矛盾的，您可以将目标设置为False，以消除一点复杂性。 elimtype False 实现了这一点。通常，您通过证明命题 P 及其否定 ~P 来证明 False；策略荒谬的P从P和~P推断出任何目标。如果存在一个矛盾的特定假设，contradict H 会将目标设置为 ~H，或者如果假设是否定的 ~A，则目标将是A（比~~A更强，但通常更方便）。如果一个特定的假设明显矛盾，矛盾 H 或只是矛盾 将证明任何目标。

有许多策略涉及归纳类型的假设。确定使用哪一个主要取决于经验。以下是主要的（但您很快就会遇到这里未涵盖的情况）：

destruct 只是将假设分解为几个部分。它丢失了有关依赖关系和递归的信息。一个典型的例子是 destruct H，其中 H 是一个连词 H : A /\ B，它将 H 拆分为A 和 B 类型的两个独立假设；或双重destruct H，其中H是析取H : A \/ B，它将证明分成两个不同的子证明，一个带有假设A 和假设 B 的一个。
case_eq 与 destruct 类似，但保留了假设与其他假设的联系。例如，destruct n，其中 n : nat 将证明分解为两个子证明，一个用于 n = 0，另一个用于 n = S米。如果 n 用于其他假设（即您有一个 H : P n），您可能需要记住您已经得到的 n destructed 与这些假设中使用的 n 相同：case_eq n 执行此操作。
inversion 对假设类型进行案例分析。当 destruct 会忘记的假设类型存在依赖关系时，它特别有用。您通常会对 Set 中的假设（其中相等相关）使用 case_eq ，对 Prop 中的假设使用 inversion （其中有非常依赖的类型）。 inversion 策略留下了很多等式，并且通常后面跟着 subst 来简化假设。 inversion_clear 策略是 inversion 的简单替代方案； subst 但丢失了一些信息。
归纳意味着您将通过给定假设的归纳（=递归）来证明目标。例如，归纳 n，其中 n : nat 表示您将执行整数归纳并证明基本情况（n 替换为 0）和归纳情况（n 替换为 m+1）。

你的例子很简单，你可以证明它“通过对 a 的案例分析是显而易见的”。

Lemma has2b2: forall a:three, a<>zero/\a<>one ->a=two.
Proof. destruct a; tauto. Qed.

但是让我们看看由 destruct 策略生成的情况，即在 intros; 之后。销毁a。。（a 为 one 的情况是对称的；最后一种情况，其中 a 为 two，很明显：反身性。）

H : zero <> zero /\ zero <> one
============================
 zero = two

这个目标看起来不可能。我们可以将这一点告诉 Coq，在这里它可以自动发现矛盾（zero=zero 是显而易见的，其余的是由 tauto 策略处理的一阶同义反复））。

elimtype False. tauto.

事实上，即使你不一开始就告诉 Coq 不要担心目标，并且先编写了不带 elimtype False 的 tauto，tauto 仍然可以工作（ IIRC 它在旧版本的 Coq 中没有）。您可以通过编写 info tauto 来了解 Coq 使用 tauto 策略所做的事情。 Coq 会告诉您 tauto 策略生成了什么证明脚本。这不太容易理解，所以让我们看一下这个案例的手动证明。首先，让我们将假设（这是一个合取）分成两部分。

destruct H as [H0 H1].

我们现在有两个假设，其中之一是零<>。零。这显然是错误的，因为它是 zero = Zero 的否定，而这显然是正确的。

contradiction H0. reflexivity.

我们可以更详细地了解矛盾策略的作用。（信息矛盾会揭示场景下发生的情况，但同样这对新手不友好）。我们声称目标是正确的，因为假设是矛盾的，所以我们可以证明任何事情。因此，让我们将中间目标设置为False。

assert (F : False).

在 H0 中运行“red”。可以看到“0 ”零实际上是~(zero=zero)的表示法，它又被定义为含义zero=zero ->错误。所以 False 是 H0 的结论：

apply H0.

现在我们需要证明 zero=zero，即

reflexivity.

现在我们已经证明了我们的断言错误。剩下的就是证明 False 暗示了我们的目标。好吧，False 意味着任何目标，这就是它的定义（False 被定义为具有 0 个案例的归纳类型）。

destruct F.

If you see an impossible goal, there are two possibilities: either you made a mistake in your proof strategy (perhaps your lemma is wrong), or the hypotheses are contradictory.

If you think the hypotheses are contradictory, you can set the goal to False, to get a little complexity out of the way. elimtype False achieves this. Often, you prove False by proving a proposition P and its negation ~P; the tactic absurd P deduces any goal from P and ~P. If there's a particular hypothesis which is contradictory, contradict H will set the goal to ~H, or if the hypothesis is a negation ~A then the goal will be A (stronger than ~ ~A but usually more convenient). If one particular hypothesis is obviously contradictory, contradiction H or just contradiction will prove any goal.

There are many tactics involving hypotheses of inductive types. Figuring out which one to use is mostly a matter of experience. Here are the main ones (but you will run into cases not covered here soon):

destruct simply breaks down the hypothesis into several parts. It loses information about dependencies and recursion. A typical example is destruct H where H is a conjunction H : A /\ B, which splits H into two independent hypotheses of types A and B; or dually destruct H where H is a disjunction H : A \/ B, which splits the proof into two different subproofs, one with the hypothesis A and one with the hypothesis B.
case_eq is similar to destruct, but retains the connections that the hypothesis has with other hypotheses. For example, destruct n where n : nat breaks the proof into two subproofs, one for n = 0 and one for n = S m. If n is used in other hypotheses (i.e. you have a H : P n), you may need to remember that the n you've destructed is the same n used in these hypotheses: case_eq n does this.
inversion performs a case analysis on the type of a hypothesis. It is particularly useful when there are dependencies in the type of the hypothesis that destruct would forget. You would typically use case_eq on hypotheses in Set (where equality is relevant) and inversion on hypotheses in Prop (which have very dependent types). The inversion tactic leaves a lot of equalities behind, and it's often followed by subst to simplify the hypotheses. The inversion_clear tactic is a simple alternative to inversion; subst but loses a little information.
induction means that you are going to prove the goal by induction (= recursion) on the given hypothesis. For example, induction n where n : nat means that you'll perform integer induction and prove the base case (n replaced by 0) and the inductive case (n replaced by m+1).

Your example is simple enough that you can prove it as “obvious by case analysis on a”.

Lemma has2b2: forall a:three, a<>zero/\a<>one ->a=two.
Proof. destruct a; tauto. Qed.

But let's look at the cases generated by the destruct tactic, i.e. after just intros; destruct a.. (The case where a is one is symmetric; the last case, where a is two, is obvious by reflexivity.)

H : zero <> zero /\ zero <> one
============================
 zero = two

The goal looks impossible. We can tell this to Coq, and here it can spot the contradiction automatically (zero=zero is obvious, and the rest is a first-order tautology handled by the tauto tactic).

elimtype False. tauto.

In fact tauto works even if you don't start by telling Coq not to worry about the goal and wrote tauto without the elimtype False first (IIRC it didn't in older versions of Coq). You can see what Coq is doing with the tauto tactic by writing info tauto. Coq will tell you what proof script the tauto tactic generated. It's not very easy to follow, so let's look at a manual proof of this case. First, let's split the hypothesis (which is a conjunction) into two.

destruct H as [H0 H1].

We now have two hypotheses, one of which is zero <> zero. This is clearly false, because it's the negation of zero = zero which is clearly true.

contradiction H0. reflexivity.

We can look in even more detail at what the contradiction tactic does. (info contradiction would reveal what happens under the scene, but again it's not novice-friendly). We claim that the goal is true because the hypotheses are contradictory so we can prove anything. So let's set the intermediate goal to False.

assert (F : False).

Run red in H0. to see that zero <> zero is really notation for ~(zero=zero) which in turn is defined as meaning zero=zero -> False. So False is the conclusion of H0:

apply H0.

And now we need to prove that zero=zero, which is

reflexivity.

Now we've proved our assertion of False. What remains is to prove that False implies our goal. Well, False implies any goal, that's its definition (False is defined as an inductive type with 0 case).