I combined Plain
and Absorbing
because that lets you assume both while proving that F
is either. This was necessary in my application because an argument of the fixpoint appeared in negative position in an implication, so that I needed to assume the argument was Absorbing
to prove the fixpoint Plain
and vice versa.
The latter -- I imagine Persistent and Absorbing could be proved similarly. (I can try in a day or two when I recover from jetlag, if you haven't already done it by then.)
I tried proving it in the logic and got stuck. It seems like the logic-level contractiveness lemmas require equivalence, while Plainly
only gives us entailment in one direction. I'll post what I have if we don't get a chance to discuss it while I'm here.
Is there a good way to state the lemmas over n-ary predicates? Maybe with telescopes? I don't know telescopes well enough.
Sorry for the delay! For some reason I didn't get notifications on this at all.
Do you mean different statements, or different proofs? The statement looks similar to e.g. https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/bi/lib/fixpoint.v#L98 to me. The proofs are different because I put this in plainly.v
, before proofmode is imported. I'll try it in the logic now.
William Mansky (6f40f593) at 25 May 05:50
This seems to work, thanks!
William Mansky (40ec1954) at 01 Apr 20:20
compatibility fix
Added some lemmas about typeclass instances for fixpoints on bi_ofeO
(as opposed to least
/greatest_fixpoint
in the logic).
William Mansky (a9310945) at 01 Apr 19:54
add fixpoint lemmas for plainly
Some of my Iris students stumbled across this issue: when iPoseProof and derived tactics are given a bad proof mode term, they appear to run forever instead of giving an error. A minimal example:
Lemma test Σ (P : iProp Σ) : P -∗ P.
Proof.
iIntros "P".
iPoseProof ("P" "P") as "H". (* diverges *)
This is a pretty silly example, but it's easy to stumble into if you forget the $!
or with
notation:
Lemma test2 Σ (P : expr -> iProp Σ) (x : nat) : (∀ x, P x) -∗ P #x.
Proof.
iIntros "P".
iPoseProof ("P" #x) as "H". (* diverges *)
This appears to be the case in versions from 3.4.0 to the current dev version (dev.2022-04-07.0.8fa39f7c).