0

来自逻辑基础的 Rel 章节。我得到了我试图理解的 excersize 的解决方案：

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 b.

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

4

1 回答 1

2

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]]]. 请注意，如果构造函数不带参数，则无需重命名，因此您可以将模式留空。

特别是，像自然数这样的东西可以用 来破坏destruct n as [ | n']。这分为n0 的情况（并且构造函数没有参数，因此 . 的左侧没有任何内容）|或. 类似地，可以将列表破坏为分为列表在哪里和它在哪里的情况。左边的空间是不必要的，所以你可以做.nn'destruct li as [ | a li']nilcons a li'|destruct li as [| a li']

在您的情况下发生的具体情况是将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(ie B -> False)。第二个目标 ( ?Goal0) 具有类型B。如果我们可以同时提供两者，则?Goal ?Goal0有 type False，因此False_rect A (?Goal ?Goal0)产生 type 的见证A。

于 2019-10-20T23:16:10.057 回答