Skip to content

fix applying big_sepL_singleton

Ralf Jung requested to merge ralf/pm into gen_proofmode

This came up when bumping Iris in LambdaRust.

I am not extremely happy about arbitrarily putting some PM option combinators into cbv and some into cbn, but this produced the best results. The reason is that We do not always want pm_default emp P to unfold, which is notation involving pm_from_option.

Alternatively, we could:

  • Define (in bi/derived_connectives.v) a function option PROP -> PROP that defaults to emp, use that for lemmas related to bi_wandM, add that function to cbn and move pm_from_option and pm_option_fun to cbv.
  • Generalize bi_wandM to bi_wandL that takes a list, and use big-ops to state the lemmas that are currently stated using pm_default emp.

Merge request reports