Ssreflect Users Discussion List

[Laurent Thery <>]

On 02/18/2016 09:43 AM, François Pottier wrote:
> Hello,
>
> Once ssreflect is loaded, the tactic "omega" no longer works out of the box
> (see attached file for an example). Is there a simple way of expanding away
> all of ssreflect's notations and definitions, so that "omega" works again?
>
> Thanks,

Unfortunately, nat in ssreflect has its own operator that omega is not 
aware of.

You can still perform an adhoc translation with Ltac but I guess this is 
not what you are looking for

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

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

Goal
  forall x y,
  x < y ->
  x < y + 1.
Proof.
intros.
ssr_omega.

--
Laurent