0

我来到了这一点：

Theorem le_antisymmetric :
  antisymmetric le.
Proof.
  unfold antisymmetric. intros a b H1 H2. generalize dependent a.
  induction b as [|b' IH].
  - intros. inversion H1. reflexivity.
  - intros.

输出：

b' : nat
IH : forall a : nat, a <= b' -> b' <= a -> a = b'
a : nat
H1 : a <= S b'
H2 : S b' <= a
------------------------------------------------------
a = S b'

我的计划是使用传递性le：

a <= b -> b <= c -> a <= c

并替换 a := a, b := (S b') 和 c := a。

所以我们会得到：

a <= (S b') -> (S b') <= a -> a <= a

我将使用 H1 和 H2 作为所需的 2 个假设并得到 Ha：a <= a。然后对其进行反演，得到构造 this is a = a 的唯一方法。

但是我应该使用什么语法来应用我的 2 个假设的传递性来得到 Ha？

4

1 回答 1

2

你在这里的第一次感应b似乎没有必要。考虑le：

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

相反，您应该先进行检查H1。如果是le_n，那么这就是平等，你就完成了。如果是le_S，那么大概这是不可能的。

intros a b [ | b' H1] H2.
- reflexivity.

这给我们留下了

a, b, b' : nat (* b is extraneous *)
H1 : a <= b'
H2 : S b' <= a
______________________________________(1/1)
a = S b'

现在，传递性是有意义的。它可以给你S b' <= b'，这是不可能的。您可以使用归纳法得出矛盾（我认为），或者您可以使用现有的引理。整个证明是这样的。

intros a b [ | b' H1] H2.
- reflexivity.
- absurd (S b' <= b').
  + apply Nat.nle_succ_diag_l.
  + etransitivity; eassumption.

最后一点是使用传递性的一种方式。etransitivity将目标R x z变成R x ?y和R ?y z，为一个新的存在变量?y。eassumption然后找到与该模式匹配的假设。具体来说，在这里，您将分别获得目标S b' <= ?y和，由和?y <= b填充。您还可以显式地给出中间值，这样您就可以删除存在前缀。H2H1e

transitivity a; assumption.
于 2019-09-15T22:05:14.213 回答