`simp` can exit the ProofMode

[markusdemedeiros]

There are some examples in our repo where simp will unfold too far, exiting the Iris proofmode altogether. At the moment the fix is is to use dsimp instead, but the proofmode should probably be stable under simp. The bug can be witnessed by changing the dsimp only statements to simp only in the (post 4.31) Quicksort example, though I recall encountering this it in a few places even before the 4.31 upgrade.

Michael suggests making Entails' a def instead of an abbrev, which seems like a good idea, but currently breaks the build in a number of places.

[MackieLoeffel]

I looked into this and it seems like simp sometimes removes the mdata that tracks the proof mode names. In the quicksort example, dsimp only results in the following

  ProofMode.Entails'
    iprop(((□
            [mdata name:IH ivar:_uniq.3996.249] iprop(∀ x_1 x_2 x_3, ...)∗
          [mdata name:Hl ivar:_uniq.3996.332] iprop(⌜l = hl_val(injl(#()))⌝)) ∗
        [mdata name:HΦ ivar:_uniq.3996.344] iprop(∀ x_1 x_2, ...)
    (WP ...)

while simp results in the following (note that [mdata name:Hl ivar:_uniq.3996.332] is missing):

  ProofMode.Entails'
    iprop(((□
            [mdata name:IH ivar:_uniq.3996.249] iprop(∀ x_1 x_2 x_3, ...) ∗
          ⌜l = hl_val(injl(#()))⌝) ∗
        [mdata name:HΦ ivar:_uniq.3996.344] iprop(∀ x_1 x_2, ...)
    (WP ...)

I am not sure what we can do about this except changing the proof mode to not rely on mdata.

I created #472 to make Entails' a def, but the problem above remains.

[markusdemedeiros]

Hm. How did you display this information? I'd be interested in coming up with a MWE so we can ask for guidance from the zulip.

[MackieLoeffel]

I added set_option pp.mdata true in before the dsimp only call in Quicksort and also add a failing command (exact id) after it to get the goal displayed in an error. For simp, this is enough, for dsimp I also had to disable the pretty printing of the proof mode by adding a failure at the beginning of delabIrisGoal in Display.lean. (We should have an option for disabling this printing.)

[markusdemedeiros]

Sweet, I didn't know about that option. Agreed about adding a flag to disable the delaboration too, it's annoying that the only options are having all notation on or off when debugging Iris stuff.

[markusdemedeiros]

Related issue: #475 (comment)

[Kaptch]

Actually, is there a way to avoid mdata at all? Probably having something like EntailsPP (A : SyntacticPresentation) (B : ActualEntails) := B and use a sealed version of this one in the proof mode (while using A for pretty-printing). My worry here is that I vaguely remember (probably it's different now) that there's no guarantee that tactics preserve mdata, so it can break if some Lean tactic changes.