coq - 如何在 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 样式的 bool 反射语句:

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.

可以通过使用 View 转换为非 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 风格的目标。