coq - 在coq中检查小于或等于自然数

Question

我有函数 ( beq_nat_refl) 确定两个自然数的相等性并给出一个布尔值。但现在我想证明一个引理，说明一个自然数x小于或等于x。我可以使用上述函数（beq_nat_refl）吗？

Theorem beq_nat_refl : 
  forall n : nat,
    true = beq_nat n n.

Theorem leq_nat :
  forall x:nat,
    x <= x.

标签： coq

Answer 1

如果您将其定义x <= y为，那将起作用x < y || x == y；然而，这不是定义，所以通常证明x <= x往往是归纳[在计算案例上]，或者如果使用见证，则应用基本构造函数。