Search code examples
coqcoq-tacticssreflect

How to use Coq arithmetic solver tactics with SSReflect arithmetic statements

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.

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.

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.

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?

Solution

  • 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.

    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: