如何在 SSReflect 算术语句中使用 Coq 算术求解器策略

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.

然而，这是非常手动的。是否有某种 technique/approach/tactic 可以自动将 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 (see ssrnatlia战术在那里，但我除非我弄错了它不能解决你的目标）。
https://github.com/pi8027/mczify -- 一个具有不同架构的活跃项目，据我所知它应该能够解决很多 SSReflect 风格的目标。

如何在 SSReflect 算术语句中使用 Coq 算术求解器策略

How to use Coq arithmetic solver tactics with SSReflect arithmetic statements

coq

coq-tactic

ssreflect