Coq中证明相等推出小于等于时找不到le_lteq引用问题

报错原因 #

Coq.Structures.Orders文档中记录的le_lteq是定义在泛用有序类型接口LeIsLtEq下的抽象引理，没有绑定具体数据类型，无法直接全局调用，必须通过实现了该接口的具体类型实例来调用。

解决方案1：使用nat专属简化证明（最推荐） #

针对nat类型的相等推导小于等于场景，直接使用算术库基础规则即可，无需引入Orders相关模块：

Require Import Coq.Arith.Arith.

Lemma easy: forall a b : nat, (a = b) -> (a <= b).
Proof.
  intros a b H.
  rewrite H.
  apply le_refl.
Qed.

解决方案2：正确调用泛用le_lteq引理 #

如果需要使用Orders模块下的泛用le_lteq，需要先导入nat对应的有序结构实例，再指定实例前缀调用：

Require Import Coq.Structures.OrdersFacts.
Require Import Coq.Structures.Orders.
Require Import Coq.Arith.Orders. (* 导入nat的有序结构实例 *)

Lemma easy: forall a b : nat, (a = b) -> (a <= b).
Proof.
  intros a b H.
  apply Nat_as_OT.le_lteq. (* 指定调用nat有序实例下的le_lteq *)
  right.
  exact H.
Qed.

内容的提问来源于stack exchange，提问作者OrenIshShalom