error at qed: no such assumption

[andres-erbsen]

Description of the problem

mit-plv/bedrock2@b717b6b#diff-5c7e120c9281033af09d97fd489aa26aR166 errors at qed with No such section variable or assumption: H6. I may try to minimize it more, but I have already sunk a couple of hours into this with minimal progress. @JasonGross ideas?

Potentially related #4086
Also wishing for #9911

Coq Version

8.9.0

[JasonGross]

You're not using instantiate or exact_no_check anywhere, are you? (I recently ran into this at #9913)

Or perhaps it is #9937? (I found that when trying to figure out ways you could get this error message just now.)

You can also get this via

Goal True -> True /\ True.
  intro x; split; let x' := constr:(x) in clear x; exact_no_check x'.

[andres-erbsen]

I am not using instantiate or exact_no_check (more precisely: the link above does use exact_no_check, but the error appears just the same if all uses of exact_no_check are replaced with exact). I am not sure about what counts as refining with an evar, but bedrock2 separation logic automation does shuffle quite a few evars around.

[andres-erbsen]

The same also happens if I remove all uses of clear (but then the build is painfully slow).

[andres-erbsen]

It looks like the definition of H6 refers to H6 (assuming I manipulated the unwieldy proof term correctly). https://github.com/mit-plv/bedrock2/compare/qed-error-unknown-variable-bsearch#diff-5c7e120c9281033af09d97fd489aa26aR2021

[andres-erbsen]

So it looks like I was using rename, and the new more minimized version is using clear https://github.com/mit-plv/bedrock2/blob/3650c64438b8b61ea16192fb2804f193f3abfa66/bedrock2/src/Examples/bsearch.v

[andres-erbsen]

Looking more and more similar to #9937... https://github.com/mit-plv/bedrock2/blob/dcd21693397064996d69ff9fb44bbe995812b2a4/bedrock2/src/Examples/bsearch.v

[andres-erbsen]

Goal exists (x4 : list word) (x5 : mem -> Prop), forall M : mem,
    sep (array scalar (word.of_Z 0) (word.of_Z 0) x4) x5 M ->
    sep (array scalar (word.of_Z 0) (word.of_Z 0) nil) (fun _ => False) M
.
Proof.
  pose proof I as X.
  unshelve (refine (ex_intro _ ?[e1] _); refine (ex_intro _ ?[e2] _); intros M H); cycle -1.
  1: unshelve epose proof ((admit : forall n, n = n -> Lift1Prop.iff1
       (sep (array scalar (word.of_Z 0) (word.of_Z 0) ?[Goal]) (sep ?[P] ?[Q]))
       (array ?[element] ?[a] ?[aa] ?[xs]))_) as Hrw; cycle -1.
  1: unshelve (let Hrw := open_constr:((Hrw _)) in clear H;
       epose proof (proj1 (SeparationLogic.Proper_sep_iff1 _ _ Hrw _ _ (RelationClasses.reflexivity _) _) admit) as _).
  1: destruct X.
  all: apply admit.
  Show Proof.
(* (let X : True := I in *)
(*  ex_intro *)
(*    (fun x4 : list word => *)
(*     exists x5 : mem -> Prop, *)
(*       forall M : mem, *)
(*       sep (array scalar (word.of_Z 0) (word.of_Z 0) x4) x5 M -> *)
(*       sep (array scalar (word.of_Z 0) (word.of_Z 0) nil) *)
(*         (fun _ : mem => False) M) admit *)
(*    (ex_intro *)
(*       (fun x5 : mem -> Prop => *)
(*        forall M : mem, *)
(*        sep (array scalar (word.of_Z 0) (word.of_Z 0) admit) x5 M -> *)
(*        sep (array scalar (word.of_Z 0) (word.of_Z 0) nil) *)
(*          (fun _ : mem => False) M) admit *)
(*       (fun (M : mem) *)
(*          (_ : sep (array scalar (word.of_Z 0) (word.of_Z 0) admit) admit M) *)
(*        => *)
(*        let Hrw : *)
(*          admit = admit -> *)
(*          Lift1Prop.iff1 *)
(*            (sep (array scalar (word.of_Z 0) (word.of_Z 0) admit) *)
(*               (sep admit admit)) (array admit admit admit admit) := *)
(*          admit admit in *)
(*        let H : sep (array admit admit admit admit) admit admit := *)
(*          proj1 *)
(*            (SeparationLogic.Proper_sep_iff1 *)
(*               (sep (array scalar (word.of_Z 0) (word.of_Z 0) admit) *)
(*                  (sep admit admit)) (array admit admit admit admit) *)
(*               (Hrw *)
(*                  (match X with *)
(*                   | I => *)
(*                       fun *)
(*                         (_ : sep *)
(*                                (array scalar (word.of_Z 0)  *)
(*                                   (word.of_Z 0) admit) admit M) *)
(*                         (_ : admit = admit -> *)
(*                              Lift1Prop.iff1 *)
(*                                (sep *)
(*                                   (array scalar (word.of_Z 0)  *)
(*                                      (word.of_Z 0) admit)  *)
(*                                   (sep admit admit)) *)
(*                                (array admit admit admit admit)) => admit *)
(*                   end H Hrw)) admit admit (RelationClasses.reflexivity admit) *)
(*               admit) admit in *)
(*        admit))) *)
Qed. (* Error: No such section variable or assumption: H. *)

[JasonGross]

Yes, I think this is the same as #9937. Since that one is smaller, perhaps we should close this as a duplicate of that?

Also, I've posted a workaround at #9937 (comment).