lt_index 去哪儿了？

Question

我在 coq 中使用了一个名为 lt_index 的引理，我记得它说

n < 2 * m + 1 -> (n - 1) / 2 < m

现在，我不能再使用这个引理了，当我使用 SearchAbout lt_index 时，coq 的回答是

Error: The reference lt_index was not found in the current environment.

我的导入如下

Require Import Coq.Numbers.Natural.Peano.NPeano.
Require Import Arith.

我是不是漏掉了什么？

编辑：显然，我梦见了这个 lt_index 引理，但从未存在过。无论如何，我想出了一个相同结果的证明，我添加了 1 <= n 作为前提条件。在这里

Lemma lt_solve:forall (n m:nat), 1 <= n -> n < 2 * m + 1 -> (n - 1) / 2 < m.
Proof.
intros.
assert (n <= n - 1 + 1).
apply Nat.sub_add_le.
inversion H1.
rewrite <-H2.
rewrite H2 in H0.
rewrite plus_comm in H0.
assert (2*m+1=1+2*m).
apply plus_comm.
rewrite H3 in H0.
apply plus_lt_reg_l in H0.
apply Nat.div_lt_upper_bound in H0.
trivial.
discriminate.
rewrite plus_comm in H2.
rewrite (le_plus_minus_r 1 n) in H2.
eapply (le_lt_trans n m0 (S m0)) in H3.
rewrite H2 in H3.
contradict H3.
apply lt_irrefl.
apply lt_n_Sn.
trivial.
Qed.

如果您发现此证明有改进，我将很高兴听到。

Answer 1

虽然尝试手动解决这些类型的问题作为练习很好，但如果您真的想做其他事情，那么长时间运行可能会变得乏味。

有些策略可以帮助您求解不等式方程组。例如，您可以使用 Psatz 中的策略 lia，或 Omega 中的 omega。证明项不是很好看，但如果这不重要，那为什么不呢。

不幸的是他们不处理除法，所以他们不能解决这个系统，但是库中有一个引理可以用来摆脱 /。我通过 Search ( _ / _ < _ ).

找到了它

Require Import Coq.Numbers.Natural.Peano.NPeano.
Require Import Psatz. (* this provides 'lia' for solving linear integer arithmetic *)

Lemma lt_solve:forall (n m:nat), 
   1 <= n -> n < 2 * m + 1 -> (n - 1) / 2 < m.
Proof.
   intros; apply Nat.div_lt_upper_bound; lia.
Qed.

Answer 2

如果您出于某种原因想要使用标准库获得 "manual" 解决方案，那么就在这里。

Require Import Coq.Arith.Arith.

Lemma lt_solve : forall (n m:nat),
    1 <= n -> n < 2 * m + 1 -> (n - 1) / 2 < m.
Proof with auto.
  intros.
  apply Nat.div_lt_upper_bound...
  destruct n.
  - inversion H.
  - rewrite Nat.sub_succ.
    rewrite Nat.sub_0_r.
    rewrite (Nat.add_lt_mono_r _ _ 1).
    rewrite Nat.add_1_r...
Qed.

lt_index 去哪儿了？

Where did lt_index go?

coq