Skip to content

Prove different versions of Löb rule

Robbert Krebbers requested to merge robbert/loeb into master

This MR follows a discussion with @dreyer @amintimany and @birkedal about a version of Löb without implication. We came up with □ (▷ P -∗ P) ⊢ P and showed it's equivalent to the normal Löb rule in affine BIs (lemma löb_alt in this MR).

I then spend an hour staring and trying to generalize löb_alt to non-affine BIs, but gave up.

This MR adds the following lemmas:

Lemma löb_wand_intuitionistically `{!BiLöb PROP} P :  (  P -∗ P)  P.
Lemma löb_wand `{!BiLöb PROP} P :  ( P -∗ P)  P.
Lemma löb_alt `{!BiAffine PROP} : BiLöb PROP   P,  ( P -∗ P)  P.

Also, it shortens the proof of tac_löb via löb_wand_intuitionistically.

Edited by Robbert Krebbers

Merge request reports