pure propositions

Stream: iris-lean

[Alex Bai]

In iris-lean, does pure propositions need to have the <affine> keyword in front like
https://github.com/leanprover-community/iris-lean/blob/5fe59a8fd5dfca4fa645aa30b462b6bb089a7187/src/Iris/Tests/Tactics.lean#L521-L525

[Markus de Medeiros]

If you remove the <affine> modality you get the error

failed to synthesize
  Std.TCOr (Affine iprop(⌜⊢ Q⌝)) (Absorbing Q)

icases requires that the term you are casing on the be affine in order to manipulate the proof context. Adding an <affine> modality is one way to make this true in any BI, however it is not necsary for BI's that have a BIAffine instance like iProp or uPred. Indeed, if you add [BIAffine PROP] you can remove the <affine> modality.

[Markus de Medeiros]

I haven't thought too hard about if there is a BI where pure propositions are not affine

[Alex Bai]

For context, I was trying to prove the theorems in bupd_alt.v. https://github.com/ahuoguo/iris-lean/blob/bupdalt/src/Iris/BI/BUpdAlt.lean

I got stuck for a bit since I need to add the affine modality for own_updateP_plainly even though the original rocq code doesn't add it.

[Michael Sammler]

You can debug this problem by using Set Typeclasses Debug in the Rocq code before the iIntros of the hypothesis. This shows that Rocq uses the plainly_absorbing typeclass instance. My guess would be that this instance is missing in Iris Lean.

[Alex Bai]

thanks! Seems like the lean equivalent is set_option trace.Meta.synthInstance true?