相对：le_antisymmetric 理解

Question

逻辑基础的相关章节。我得到了我试图理解的运动量的解决方案：

Definition antisymmetric {X: Type} (R: relation X) :=
  forall a b : X, (R a b) -> (R b a) -> a = b.

Theorem le_antisymmetric :
  antisymmetric le.
Proof.
  unfold antisymmetric. intros a b [| b' H1] H2.
  - reflexivity.
  - absurd (S b' <= b').
    + apply le_Sn_n.
    + etransitivity ; eassumption.

我不明白，介绍模式 [| b' H1] 是如何工作的？介绍后显示：

2 subgoals (ID 43)

  a, b : nat
  H2 : a <= a
  ============================
  a = a

subgoal 2 (ID 46) is:
 a = S b'

第二个子目标：

a, b, b' : nat
H1 : a <= b'
H2 : S b' <= a
============================
a = S b'

我知道它等同于destruct，但什么样的destruct？绝对不是简单的destruct b.

我也试图理解使用 absurd (S b' <= b') 战术背后的逻辑。这是否意味着如果我们在这种情况下证明a = S b'，则意味着我们将H1中的a重写为S b'后，我们得到：S b' <= b'，这是一个普遍错误的陈述（荒谬）？

Answer 1

intros a b [| b' H1] H2等同于

intros a b H H2.
destruct H as [| b' H1].

destruct 模式通常遵循以下规则：如果归纳类型具有单个构造函数（例如产品），那么对于该归纳类型中的 x，destruct x as [a b c...] 会（非递归) 归纳并将新变量重命名为 a、b、c 等。当归纳类型具有多个构造函数时，存在多种情况。为此，您使用 destruct x as [a b c ... | d e f ... | ...]。如果需要，可以嵌套这些破坏模式，例如destruct x as [[a b] | [c [d | e]]]。请注意，如果构造函数不带参数，则无需重命名，因此您可以将模式留空。

你的情况具体是 le 被定义为归纳类型，类似于

Inductive le (n : nat) : nat -> Prop :=
| le_n : le n n
| le_S : forall m : nat, le n m -> le n (S m).

所以有两种情况：一种是没有参数，另一种是参数为m: nat和H: le n m的后继情况。因此，破坏模式是 [| m H].

回答你的第二个问题，absurd (S b' <= b'). 意味着（我们认为）我们能够在当前上下文中证明 S b' <= b'。我们还可以证明（在相同的上下文中）S b' <= b' 是荒谬的，即导致 False 的见证（更准确地说，S b' <= b' -> False）。使用 False 的归纳原理，这允许我们为任何类型生成见证，特别是 a = S b'.

你可以看到什么样的证明项 absurd 用最少的实验产生。

Goal forall A B: Type, A.
Proof.
  intros A B.
  absurd B.
  Show Proof.

这应该打印 (fun A B : Type => False_rect A (?Goal ?Goal0))。第一个目标 (?Goal) 的类型为 ~B（即 B -> False）。第二个目标 (?Goal0) 的类型为 B。如果我们可以同时提供两者，那么 ?Goal ?Goal0 的类型为 False，因此 False_rect A (?Goal ?Goal0) 会生成 A.

类型的见证

相对：le_antisymmetric 理解

Rel: le_antisymmetric comprehension

coq

logical-foundations