执行coq命令

Question

我在小于或等于的情况下使用destruct命令，在小于的情况下使用同样的命令。我在应用(ltb_correct)命令时遇到了问题，错误信息是 "this command is not found"。请指导我如何应用ltb_correct。在标准库中，leb_correct存在，但ltb_correct不存在。

  `destruct (le_lt_dec n m).
   Lemma leb_correct m n : m <= n -> (m <=? n) = true.
  (leb_correct _ _ l).

  destruct (lt_dec  n m).
  Lemma ltb_correct m n : m < n -> (m <? n) = true.
  (ltb_correct _ _ l).`

Answer 1

事实上，没有 ltb_correct 等价物存在于标准库中，可能意味着你不应该使用这个外稃。如果你搜索涉及 Nat.leb 和 Nat.ltb你会发现以下几个。

Nat.leb_le : forall n m, (n <=? m) = true <-> n <= m
Nat.ltb_lt : forall n m, (n <?  m) = true <-> n <  m.

你可以用这样的等价物与 apply 策略。

Require Import Coq.Arith.Arith.

Goal forall n m : nat, False.
intros n m.
destruct (le_lt_dec n m) as [l|l].
- apply Nat.leb_le in l.
  admit.
- apply Nat.ltb_lt in l.
  admit.
Admitted.