omega with bit shifts

Stream: metaprogramming / tactics

[Geoffrey Irving]

Is it possible to use omega for the theory of Nat with +, -, <, and <<< (shifting left with no overflow)? I.e., is there a mechanical way to reduce to something omega can handle?

My guess is no, but I figured I would check just in case (it would be amazing if there was an approach).

[Mario Carneiro]

yes, that's in principle something omega could handle, although it will have to split on any x - y subterms

[Mario Carneiro]

Oh, but the shifts have to be by constants

[Geoffrey Irving]

Yes, I mean the nonconstant shift case, alas.

[Mario Carneiro]

in that case you should try linarith

[Geoffrey Irving]

Nonconstant shifts are nonlinear, so I don’t think that applies. Currently I’m just bludgeoning through it all manually, but it’s painful.

[Mirek Olšák]

It occurred to me that omega could be in theory able to handle also right shifts by a constant (in general integer division by a constant), although I don't really need that...

[Geoffrey Irving]

If it can do one, it can do the other.

[Geoffrey Irving]

(Because y = x >>> s iff exists z, z < 1 <<< s && x = y <<< s + z.)

[Kim Morrison]

It already handles integer division by a constant. To handle right shift by a constant you will need to rewrite as a division first.

[Geoffrey Irving]

Yes, the original question was whether nonconstant shifts are weaker enough to work too.

[Geoffrey Irving]

Presumably no, but I wanted to check.