如何将Coq算术求解器策略与SSReflect算术语句一起使用

Question

Coq具有一些用于自动证明算术引理的便捷策略，例如lia：

From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import ssrnat.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Require Import Psatz.

Lemma obv : forall (x y z: nat), (x < y)%coq_nat -> (y < z)%coq_nat -> (z < 3)%coq_nat -> (x < 3)%coq_nat.
Proof.
  move => x y z xlty yltz zlt3. lia.
Qed.

但是这些策略不直接支持SSReflect样式的布尔反射语句：

Lemma obv_ssr: forall (x y z: nat), (x < y) && (y < z) && (z < 3) -> (x < 3).
Proof.
  move => x y z H.  Fail lia.
Abort.

Lemma obv_ssr: forall (x y z: nat), (x < y) -> (y < z) -> (z < 3) -> (x < 3).
Proof.
  move => x y z xlty yltz zlt3. Fail lia.
Abort.

可以通过使用视图转换为非SSR格式来解决它们：

Lemma obv_ssr: forall (x y z: nat), (x < y) && (y < z) && (z < 3) -> (x < 3).
Proof.
  move => x y z.  move/andP => [/andP [/ltP x_lt_y /ltP y_lt_z] /ltP z_lt_3].
  apply/ltP. lia.
Qed.

然而，这是非常手动的。是否有某种技术/方法/策略可以自动将像lia这样的引理应用到SSR风格的语句？

Answer 1

总体上，这尚未完全解决问题：您可以跟踪其进度here。

在您的特定示例中，以下足够：

Lemma obv_ssr: forall (x y z: nat), (x < y) && (y < z) && (z < 3) -> (x < 3).
Proof.
move=> x y z.
rewrite -?(rwP andP) -?(rwP ltP).
lia.
Qed.

有时您可能想使用rewrite -?plusE -?multE -?minusE之类的东西来进行标准算术类型的更多转换（如果您的目标中有更多的算术运算，请添加更多的转换）。

至少有两个项目试图解决该问题：

• [https://github.com/amahboubi/lia4mathcomp（请参阅此处的ssrnatlia战术，但是我除非我误认为它无法解决您的目标）。]]
• https://github.com/pi8027/mczify-一个活动的项目，具有不同的体系结构，据我所知，它应该能够解决许多SSReflect样式的目标。