feat: monotone tactic - #595
Conversation
| refine BI.sep_ne.ne ?_ ?_ | ||
| · exact Hwp m m_n _ _ _ | ||
| · exact BI.BigSepL.bigSepL_dist <| fun _ => Hwp m m_n _ _ _ | ||
| distLater_dist := by contractive |
|
Can you create this PR as a stacked pull request on top of #558? This would make it easier to review this PR. |
| Copyright (c) 2026 Oliver Soeser. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Oliver Soeser | ||
| -/ |
There was a problem hiding this comment.
I think this file should be in the BI folder, next to the Fixpoint file.
|
|
||
| open Iris BI OFE Iris.Std | ||
|
|
||
| class MonotonePred [BI PROP] [OFE A] |
There was a problem hiding this comment.
Can this be unified with BIMonoPred?
| monotone : ∀ (Φ Ψ : A → PROP), | ||
| ⊢ (□ ∀ x, Φ x -∗ Ψ x) -∗ ∀ x, F Φ x -∗ F Ψ x | ||
|
|
||
| class AntitonePred [BI PROP] [OFE A] |
There was a problem hiding this comment.
Can we unify AntitonePred and MonotonePred, maybe with a boolean which says whether the wand is flipped? This would hopefully avoid the need for the duplicated instances below.
|
|
||
| @[expose] public section | ||
|
|
||
| open Iris BI OFE Iris.Std |
There was a problem hiding this comment.
I am wondering if it makes more sense to follow the design of PartialOrder / CCPO in the standard library more closely. The design there seems quite nice since it for example allows n-ary predicates very naturally.
I have something like the following in mind. I have not fully thought it through, so I am not fully sure if it will work, but might be worth playing around with a bit.
class BIPartialOrder PROP [BI PROP] (α : Sort u) where
/--
A “less-or-equal-to” or “approximates” relation.
-/
rel : α → α → PROP
/-- The “less-or-equal-to” or “approximates” relation is reflexive. -/
rel_refl : ∀ {x}, ⊢ rel x x
/-- The “less-or-equal-to” or “approximates” relation is transitive. -/
rel_trans : ∀ {x y z}, rel x y -∗ rel y z -∗ rel x z
scoped infix:50 " ⊑ᵢ " => BIPartialOrder.rel
def monotone {α β} PROP [BI PROP] [BIPartialOrder PROP α] [BIPartialOrder PROP β] (f : α → β) : Prop :=
∀ x y, ⊢@{PROP} (□ x ⊑ᵢ y) -∗ f x ⊑ᵢ f y
3 participants
Description
Implements the
monotonetactic for proving the monotonicity of functions on Iris predicates and extendsnonexpto handle uncurried functionsDepends on #558
Checklist
authorssection of any appropriate files