[rewrite] Unable to match RHS

[RalfJung]

In the following code, ssreflect is unable to perform the rewrite, claiming that wp _ does not match the goal:

(* File reduced by coq-bug-finder *)
Require Import Coq.Setoids.Setoid.
Require Import Coq.Unicode.Utf8.
Require Import mathcomp.ssreflect.ssreflect.

Global Generalizable All Variables.

Class Lookup (K A M : Type) := lookup: K → M → option A.
Notation "m !! i" := (lookup i m) (at level 20).

Section S1.
Context `{∀ A, Lookup nat A (M A)}.

Definition iProp := Prop.
Definition state := M nat.

Program Definition wp (Q : iProp) : iProp := True.

(* Just some relation. *)
Inductive entails (P Q : Prop) : Prop :=
  | Entails : (P → Q) → entails P Q.

Lemma wp_lift_atomic_step {Q} (φ : state → Prop) :
  entails (False) (wp Q).
Admitted.

Instance uPred_entails_rewrite_relation : RewriteRelation entails.
Global Instance: PreOrder entails.
Proof. Admitted.

Lemma wp_alloc_pst (σ : state) Q :
  entails Q (wp Q).
Proof.
  set (φ σ' := ∃ l, σ' = σ ∧ σ !! l = None).
  rewrite -(wp_lift_atomic_step (λ σ', ∃ l, σ' = σ ∧ σ !! l = None))=>//.

This is obviously wrong, the RHS does match the goal. If I replace rewrite - by rewrite <-, the rewrite succeeds. Similar, if I replace the (λ ... ) by φ, the rewrite succeeds. Finally, if I replace σ !! l = None by l = 0, again the rewrite succeeds.

This is with ssreflect 1.6 and Coq 8.5.

[gares]

You are perfectly right, it is a bug. What fails is the resolution of the type class behind the ( !! ) notation. It fails because the code used to pass the wrong set of universe constraints to the type class engine. I'm testing the fix and hopefully pushing it shortly.

[robbertkrebbers]

Thank you very much Enrico! It also fixes the issue in our (= Ralf's and mine) actual code.

[RalfJung]

Thanks a lot for fixing this :) However, is there any chance of a release any time soon? Without a release, we have to keep our work-arounds in place so that people can use our development with a stable version of ssreflect...

[gares]

Unfortunately, you will not see a release before Christmas. I'm too busy to make it happen.

[RalfJung]

You actually did make it happen before Christmas, after all. Thanks a ton :)