问题描述
Coq具有一些自动证明算术引理的便捷策略，例如 lia :
Coq has some convenient tactics for automatically proving arithmetic lemmas, for instance 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样式的布尔反射语句:
The tactics do not directly support SSReflect-style boolean reflection statements however:
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格式来解决这些问题:
It's possible to solve them by converting to non-SSR format using views:
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风格的语句中?
This is however very manual. Is there some kind of technique/approach/tactic that can automate this application of lemmas like lia to SSR-style statements?
推荐答案
总体而言，这尚未完全解决:您可以跟踪其进度此处.
This is not yet a totally resolved issue in general: you can track its progress here.
在您的特定示例中，以下内容就足够了:
In your particular example the following is enough:
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 之类的东西来进行标准算术类型的更多转换(如果您的算术运算更多，则添加更多的转换)目标).
Sometimes you might want to throw in some more conversions of the standard arithmetic types using something like rewrite -?plusE -?multE -?minusE (adding more conversions if you have more arithmetic operations in your goal).
至少有两个项目试图解决该问题:
There are at least two projects trying to resolve the issue in general:
- https://github.com/amahboubi/lia4mathcomp (请参见 ssrnatlia 策略，但我除非我误以为它不能解决您的目标).
- https://github.com/pi8027/mczify -一个具有不同内容的活动项目架构，据我所知，它应该能够解决许多SSReflect风格的目标.
- https://github.com/amahboubi/lia4mathcomp (see ssrnatlia tactic there, but I unless I'm mistaken it cannot solve your goal).
- https://github.com/pi8027/mczify -- an active project with a different architecture and as far as I know it should be capable of solving a lot of SSReflect-style goals.
这篇关于如何将Coq算术求解器策略与SSReflect算术语句一起使用的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！