Ssreflect Users Discussion List

[Laurent Thery <>]

On 02/18/2016 10:35 AM, François Pottier wrote:
> Hi Laurent,
>
> Thanks for your reply; this is helpful.
>
> > You can still perform an adhoc translation with Ltac but I guess this is not  
> > > what you are looking for
>
> I think this is what I am looking for, especially if someone has already
> written this piece of Ltac and if it handles all of the arithmetic operators
> and logical connectives known to "omega". Does such a thing exist? It seems
> that (for certain kinds of proofs) it would be a pity to work without
> "omega".

This could be a nice little project for the upcoming code-spring but 
then maybe lia would be a better target than omega.

Anyway, I guess that the tactic

Definition ssrop := (multE, plusE).

Ltac rm_leqn :=
  match goal with
   H : is_true (_ <= _) |- _ => move/leP: H; rewrite -!ssrop => H
  end.

Ltac ssr_omega :=
  intuition; repeat rm_leqn; try apply/leP; rewrite -?ssrop; omega.

could be enough to solve "most" of the linear goals.

--
Laurent.