rewrite with short goal and rewrite term does not finish (within 1 hour)

[MSoegtropIMC]

Dear Coq Team,

in the following example:

(* Princeton VST toolchain *)
Require Import VST.floyd.proofauto.
Require Import VST.floyd.library.

Coercion Int.repr : Z >-> Integers.int.

Example Test1 (i : Integers.int) :
   emp |-- !! (Int.eq (Int.shl i (Int.repr (- (1)))) (Int.repr 0) = true) && emp.

 Time rewrite -> @isptr_field_address_lemma.
 Time rewrite -> @is_pointer_or_null_field_address_lemma.

both rewrites at the end do not finish - the first one I aborted after more than 1 hour. The goal term and the rewrite lemmas are reasonably short, so that this is unexpected.

Both rewrites should not apply to the goal term - this gets stuck as part of an autorewrite with a hint database.

This is with Coq 8.12.0 and VST 2.6 (as in the Coq platform 8.12 beta 1).

@andrew-appel : FYI: I have issues that entailer gets stuck in autorewrite with entailer_rewrite in *, which I tracked down to this small example.

[MSoegtropIMC]

Here is an example using a much simpler term to rewrite:

(* Princeton VST toolchain *)
Require Import VST.floyd.proofauto.
Require Import VST.floyd.library.

Coercion Int.repr : Z >-> Integers.int.

Example Test2 (i : Integers.int) :
   Int.eq (Int.and (Int.shl i (Int.sub 0 1)) 1) 0 = true.

  try timeout 5 rewrite -> (neg_repr).
Abort.

[MSoegtropIMC]

That rewrite takes so long might have something to do with the below case, where reflexivity takes pretty much forever:

Require Import ZArith.
Require Import compcert.lib.Integers.

Coercion Int.repr : Z >-> Integers.int.

Open Scope Z_scope.

Example Test3 (i : Integers.int):
   (Int.eq (Int.and (Int.shl (i) (0 - 1)) 8388608) 0 = true).
Proof.
  Timeout 3 reflexivity.

[MSoegtropIMC]

Interestingly for the same expression with plain Z (which differs from CompCert integers by the missing modulo wordsize) this is immediate:

Require Import ZArith.

(* Example 3 with Z instead of CompCert numbers *)

Example Test3b (i : Z):
   (Z.eqb (Z.land (Z.shiftl (i) (0 - 1)) 8388608) 0 = true).
Proof.
  Fail reflexivity.
Abort.

So I guess the modulo wordsize is simply too hard to figure out in the presence of variables - understandable but not very nice. Possibly this would work if CompCert would use a specific power of 2 modulus function for the word size rather than the generic modulus function, but then this would lead to quite an inflation of functions and lemmas.

Still I somehow need to be able to rewrite simple terms with simple lemmas - any idea what I can do about this?

Btw.: up to now I mostly used my own automation for VST but it is quite specific to certain use cases. I am currently doing some experiment on how far I get with the VST supplied automation for a different use case. My own automation only applies reflexivity or rewrite when it knows it will work, but the VST supplied automation has things like autorewrite with reflexivity to solve premises with might or might not work.

[MSoegtropIMC]

P.S.: I guess the issue is that Int.shl and Z.shiftl do very different things when the shift is negative, Z.shiftl actually does a shift right then, but Int.shl does a shift left of 2^32-shift, which is surely problematic. Still it is not nice that the rewrites take forever.

[fakusb]

Does "Set Keyed Unification." help in your usecase? Then coq only rewrites if the head of the side of the equation can really be seen. Now at least the rewrites on your first example fail quick. But this could break a lot of other things.

[MSoegtropIMC]

@fakusb : thanks, yes with this the rewrites fail immediately. I guess the issue is that without this the modulo 2^32 operations get expanded looking for a suitable head symbol, and this takes forever.

If I understand this correctly, "Set Keyed Unification" requires that head symbol is immediately visible in the goal. This might indeed be a bit too strong. I guess ideal would be to be able to specify a maximum number of reduction steps until the head symbol must be found. I would think that usually a small number, say 5 or 10 depending on how one counts these, would be sufficient.

[gares]

This might indeed be a bit too strong.

The rewrite from SSR uses this strategy, and in mathcomp we did not feel the need for a much deeper search. Sure, from time to time you do rewrite /def lem which first unfolds def and then rewrites with lem. It's still quite rare IIRC, since if def has an associated theory, then lem may also be there for def formulated so that it does not lose the "abstraction" given by def.

[MSoegtropIMC]

@gares : thanks, I will look into this. Is the number of reduction steps a rewrite does in ssreflect adjustable? If not, what is it?

[gares]

0 for the head symbol, unlimited for its arguments. But you can override the pattern, hence the head symbol, very easily. So the choice to look for the head verbatim is not as rigid as it sounds

[ppedrot]

This is a variant of #15593. (Here the problem happens in conversion of types rather than closed subterms, but that's the same underlying issue.)