在Ssreflect中证明简单的不等式
问题描述:
我在Coq中使用MathComp库进行反射时遇到了一些非常简单的问题。在Ssreflect中证明简单的不等式
假设我要证明这个定理:
From mathcomp Require Import ssreflect ssrbool ssrnat.
Lemma example m n: n.+1 < m -> n < m.
Proof.
have predn_ltn_k k: (0 < k.-1) -> (0 < k).
by case: k.
rewrite -subn_gt0 subnS => submn_pred_gt0.
by rewrite -subn_gt0; apply predn_ltn_k.
Qed.
这种做法似乎有点“非正统”给我这样一个简单的任务。有没有更好/更简单的方法来做到这一点?
答
是的,有一个更好的办法。你引理是ltnW : forall m n, m < n -> m <= n
一个特殊情况:
Lemma example n m : n.+1 < m -> n < m.
Proof. exact: ltnW. Qed.
这工作,因为n < m
是n.+1 <= m
实际语法糖。
答
我没有练过ssreflect了很多,所以我真的不能告诉这是否可以golfed下来,但基本思路是n < n.+1 < m
:
Require Import mathcomp.ssreflect.ssrnat.
Require Import mathcomp.ssreflect.ssrbool.
Require Import mathcomp.ssreflect.ssreflect.
Lemma example m n: n.+1 < m -> n < m.
Proof.
move => ltSnm; apply: ltn_trans; by [apply ltnSn | apply ltSnm].
Qed.
+2
提示:将您的三条第一行更改为:'From mathcomp Require Import ssrnat ssrbool ssreflect.' –
请在发布代码段时始终包含导入列表。 – gallais