In VST 3.0beta2, normalize1 tactic

[andrew-appel]

In vst_on_iris, this line of Ltac normalize1 in seplog_tactics.v can't possibly be right:

  match goal with
  | |- bi_entails(PROP := monPredI _ _) _ _ => let rho := fresh "rho" in split => rho; monPred.unseal

It turns ENTAIL Delta, PQR |-- PQR' into lift1 bi_pure (tc_environ Delta) rho ∧ (... ) ⊢ PQR' which doesn't seem desirable at all.

I ran into this in cbench-vst/verif_fac6.

[mansky1]

It could be right -- that's essentially the effect of go_lower, which I believe the old version of normalize also performs. It's possible that it should also be doing some unfold_lift to turn the lift1 bi_pure ... into a pure assertion. Do you happen to know what the same normalize does when using the master branch?

[andrew-appel]

unfold_lift doesn't do anything on the resulting goal.

[andrew-appel]

And also: this line was entirely missing from the master-branch version of normalize1, perhaps we should just delete it and see if anything breaks.

[andrew-appel]

For further documentation: Here's an example (from floyd/client_lemmas.v) that this line was intended to address:

OK_ty : Type
Σ : gFunctors
VSTGS0 : VSTGS OK_ty Σ
B : biIndex
P1 : Prop
A : monPred B (iPropI Σ)
P : list Prop
QR : monPred B (iPropI Σ)
S : monPredI B (iPropI Σ)
H : P1 → A ∧ ⌜foldr and True P⌝ ∧ QR ⊢ S
______________________________________(1/1)
A ∧ ⌜P1 ∧ foldr and True P⌝ ∧ QR ⊢ S

but example on which it inappropriately introduces environment rho is at line 471 of https://github.com/cverified/cbench-vst/blob/vst3.0/fac/verif_fac6.v

[andrew-appel]

In that commit, I have addressed the issue by commenting out the problematic line in normalize1, and then patching all the lemma-proofs in floyd as necessary. I will leave this issue open, at least for now, in case someone wants to make a new version of the problematic line that is more precise in where it applies, so it does something useful without doing things that are harmful.

[mansky1]

Okay, I remember why that's there. The issue is that (because of the ad-hoc way that mpred equality works now) many of normalize's rewrites can't be stated generically across the mpred and assert levels. My hack was to have normalize lower assert to mpred automatically, because I didn't see any cases where we actually cared about staying at the assert level when using normalize. But you've found such a case now. Re-proving all of the equalities at assert would be annoying and adding them might slow down normalize, so I'm happy to stick with your solution as long as it doesn't break any client proofs.