Library prosa.util.ssrlia
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
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.
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.
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.
repeat arith_hypo_ssrnat2coqnat; arith_goal_ssrnat2coqnat;
simpl;
lia.