Rev.v le_antisymmetric
Rev.v le_antisymmetric
我得出的结论是:
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?
你对 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
,分别由 H2
和 H1
填充。您还可以明确给出中间值,这样您就可以删除 e
xistential 前缀。
transitivity a; assumption.
我得出的结论是:
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?
你对 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
,分别由 H2
和 H1
填充。您还可以明确给出中间值,这样您就可以删除 e
xistential 前缀。
transitivity a; assumption.