Как использовать решающую тактику Coq arithmeti c с арифметикой SSReflect c - PullRequest
Новая
       103

Как использовать решающую тактику Coq arithmeti c с арифметикой SSReflect c

2 голосов
/ 04 апреля 2020

Coq имеет несколько удобных тактик для автоматического доказательства арифметических c лемм, например 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.

Это, однако, очень руководство. Есть ли какая-то техника / подход / тактика c, которая может автоматизировать это применение лемм, таких как lia, к заявлениям в стиле SSR?

1 Ответ

2 голосов
/ 04 апреля 2020

В общем, это еще не полностью решенная проблема: вы можете отслеживать ее прогресс здесь .

В вашем конкретном примере достаточно следующего: 

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.

Иногда вам может потребоваться добавить еще несколько преобразований стандартных арифметических c типов, используя что-то вроде rewrite -?plusE -?multE -?minusE (добавление дополнительных преобразований, если в вашей цели больше арифметических c операций).

Там как минимум два проекта пытаются решить проблему в целом:

...