2

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 样式语句中？

4

1 回答 1

2

一般来说，这还不是一个完全解决的问题：您可以在此处跟踪其进度。

在您的特定示例中，以下内容就足够了：

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更多转换（如果您的目标中有更多算术运算，则添加更多转换）。

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

于 2020-04-04T16:03:49.153 回答