Library prosa.util.ssrlia

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Require Import Lia.

(* Adopted from http://github.com/pi8027/formalized-postscript/blob/master/stdlib_ext.v *)

This tactic matches over the hypotheses, searching for expressions that can be converted from ssreflect arithmetic to Coq arithmetic.
Ltac arith_hypo_ssrnat2coqnat :=
  match goal with
  | H : context [andb _ _] |- _ ⇒ let H0 := fresh in case/andP: H ⇒ H H0
  | H : context [orb _ _] |- _ ⇒ case/orP: H ⇒ H
  | H : context [?L ≤ ?R] |- _ ⇒ move/leP: H ⇒ H
  | H : context [?L < ?R] |- _ ⇒ move/ltP : H ⇒ H
  | H : context [?L == ?R] |- _ ⇒ move/eqP : H ⇒ H
  | H : context [addn ?L ?R] |- _ ⇒ rewrite -plusE in H
  | H : context [muln ?L ?R] |- _ ⇒ rewrite -multE in H
  | H : context [subn ?L ?R] |- _ ⇒ rewrite -minusE in H
  end.

This tactic matches the goal, searching for expressions that can be converted from ssreflect arithmetic to Coq arithmetic.
Ltac arith_goal_ssrnat2coqnat :=
  rewrite ?NatTrec.trecE -?plusE -?minusE -?multE -?leqNgt -?ltnNge;
  repeat match goal with
         | |- is_true (andb _ _) ⇒ apply/andP; split
         | |- is_true (orb _ _) ⇒ try apply/orP
         | |- is_true (_ ≤ _) ⇒ try apply/leP
         | |- is_true (_ < _) ⇒ try apply/ltP
         end.

Solves linear integer arithmetic goals containing ssreflect expressions. This tactic first rewrites the context to replace operations from ssreflect to the corresponding operations in the Coq library, then calls lia.
Ltac ssrlia :=
  repeat arith_hypo_ssrnat2coqnat; arith_goal_ssrnat2coqnat;
  simpl;
  lia.