Library prosa.util.ssrlia


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)


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: HH H0
  | H : context [orb _ _] |- _case/orP: HH
  | H : context [?L ?R] |- _move/leP: HH
  | H : context [?L < ?R] |- _move/ltP : HH
  | H : context [?L == ?R] |- _move/eqP : HH
  | 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.