/- Copyright (c) 2026 Edwin Fernando. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Edwin Fernando -/ import Bppl.Lilac.KRM import Iris.BI.Extensions import Iris.Std.Equivalence /-! # Generating instance of BI (logic of Bunched Implications) given a KRM (Kripke Resource Monoid) This file instantiates MoSeL, the frontend of Iris offering a proofmode for general separatin logics. We also prove that the Lilac is an affine logic, which is guaranteed by our defintion of the Krm along with the following standard recipe for constructing a BI out of it. ## Main Definitions - `Iris.Instances.instBIBase`: Semantics of the standard separation logic connectives given a `Krm` - `Iris.Instances.instBI`: Proof that the instantiation satisfies the axioms of separaiton logic - `Iris.Instances.instKrmBIAffine`: Such an instantiation of BI with `Krm` is affine. -/ namespace Iris.Instances open Iris.BI variable {Env Resource : Type*} [Krm Resource] /-- An "Iris Proposition" (prop in the separation logic) is defined by this deep embedding, directly providing the semantics. In this subtype the data part, `sem`, defines the satisfiability relation, and we add the monotonicity constraint: any `IProp` satisfied by a "less informative" resource is also satisfied by a more informative resource. Note: Consider automation of monotonicity proof by `@[mono]` annotations? -/ abbrev IProp (Resource : Type*) [Krm Resource] := {sem : Resource → Prop // ∀ σ₁ σ₂, σ₁ ≤ σ₂ → sem σ₁ → sem σ₂} /-! ### BIBase instance -/ instance instBIBase : BIBase (IProp Resource) where Entails P Q := ∀ σ, P.1 σ → Q.1 σ -- technically `emp` accepts any resource `Ω` such that `1 ≤ Ω`. But this is a tautology -- by `Krm.one_le`. So we just mark `emp` as `True` to make auxilliary proofs easier. emp := ⟨fun _ ↦ True, fun _ _ _ _ ↦ trivial⟩ pure φ := ⟨fun _ ↦ φ, fun _ _ _ hσ₁ ↦ hσ₁⟩ and P Q := ⟨fun σ ↦ P.1 σ ∧ Q.1 σ, by intro σ₁ σ₂ hle ⟨hPσ₁, hQσ₁⟩ exact ⟨P.2 σ₁ σ₂ hle hPσ₁ , Q.2 σ₁ σ₂ hle hQσ₁⟩ ⟩ or P Q := ⟨fun σ ↦ P.1 σ ∨ Q.1 σ, fun σ1 σ2 hle hσ1 => hσ1.elim (Or.inl ∘ P.2 σ1 σ2 hle) (Or.inr ∘ Q.2 σ1 σ2 hle) ⟩ imp P Q := ⟨fun σ ↦ ∀ σ', σ ≤ σ' → (P.1 σ' → Q.1 σ'), fun σ₁ σ₂ σ₁_le_σ₂ hσ₁ σ' σ₂_le_σ' hPσ' ↦ hσ₁ σ' (σ₁_le_σ₂.trans σ₂_le_σ') hPσ' ⟩ sForall Ψ := ⟨fun σ ↦ ∀ p, Ψ p → p.1 σ, by intro σ₁ σ₂ σ₁_le_σ₂ hσ₁ p hp exact p.2 σ₁ σ₂ σ₁_le_σ₂ (hσ₁ p hp) ⟩ sExists Ψ := ⟨fun σ ↦ ∃ p, Ψ p ∧ p.1 σ, by intro σ₁ σ₂ σ₁_le_σ₂ ⟨p, hp, hpσ₁⟩ exact ⟨p, hp, p.2 σ₁ σ₂ σ₁_le_σ₂ hpσ₁⟩ ⟩ sep P Q := ⟨fun σ ↦ ∃ σ₁ σ₂, ∃ (σ₁₂ : ✓'(σ₁ ⋆ σ₂)), ↓σ₁₂ ≤ σ ∧ P.1 σ₁ ∧ Q.1 σ₂, by intro σ₁ σ₂ σ₁_le_σ₂ ⟨σP, σQ, h_exists, h_le, hP, hQ⟩ use σP, σQ, h_exists exact ⟨h_le.trans σ₁_le_σ₂, hP, hQ⟩ ⟩ wand P Q := ⟨fun σ ↦ ∀ σP, ∀ σQ : ✓'(σP ⋆ σ), (P.1 σP → Q.1 ↓σQ), by intro σ₁ σ₂ σ₁_le_σ₂ h σP σQ hP obtain ⟨p, hp, hple⟩ := Krm.le_mul_mono σP σP σ₁ σ₂ ((σP ⋆ σ₂).get σQ) (Preorder.le_refl σP) σ₁_le_σ₂ ((Option.some_get σQ).symm) have hs : (σP ⋆ σ₁).isSome = true := hp.symm ▸ rfl have hle : (σP ⋆ σ₁).get hs ≤ (σP ⋆ σ₂).get σQ := by simp only [← hp.symm, Option.get_some]; exact hple exact Q.2 _ _ hle (h σP hs hP) ⟩ persistently P := ⟨fun _ ↦ P.1 1, fun _ _ _ h ↦ h⟩ later P := ⟨fun σ ↦ P.1 σ, P.2⟩ instance : Std.Preorder (Entails (PROP := IProp Resource)) where refl := fun _ h => h trans := fun h_xy h_yz σ h_x => h_yz σ (h_xy σ h_x) instance : COFE (IProp Resource) := COFE.ofDiscrete Eq equivalence_eq /-! ### BI instance -/ open BI in /-- These proofs have been ported from the Iris-lean to the classical separation logic, modified as necessary. -/ instance instBI : BI (IProp Resource) where entails_preorder := by infer_instance equiv_iff {P Q} := ⟨ fun h : P = Q => h ▸ ⟨fun _ φ ↦ φ, fun _ φ ↦ φ⟩, fun ⟨h₁, h₂⟩ => by ext σ; exact ⟨h₁ σ, h₂ σ⟩ ⟩ and_ne := ⟨by rintro _ _ _ rfl _ _ rfl; rfl⟩ or_ne := ⟨by rintro _ _ _ rfl _ _ rfl; rfl⟩ imp_ne := ⟨by rintro _ _ _ rfl _ _ rfl; rfl⟩ sep_ne := ⟨by rintro _ _ _ rfl _ _ rfl; rfl⟩ wand_ne := ⟨by rintro _ _ _ rfl _ _ rfl; rfl⟩ persistently_ne := ⟨by rintro _ _ _ rfl; rfl⟩ later_ne := ⟨by rintro _ _ _ rfl; rfl⟩ sForall_ne {_ P Q} h := liftRel_eq.1 h ▸ rfl sExists_ne {_ P Q} h := liftRel_eq.1 h ▸ rfl pure_intro h _ _ := h pure_elim' h_φP σ h_φ := h_φP h_φ σ ⟨⟩ and_elim_l := by dsimp only [Entails, BI.and]; tauto and_elim_r := by dsimp only [Entails, BI.and]; tauto and_intro := by dsimp only [Entails, BI.and]; tauto or_intro_l := by dsimp only [Entails, BI.or]; tauto or_intro_r := by dsimp only [Entails, BI.or]; tauto or_elim := by dsimp only [Entails, BI.or]; tauto imp_intro := by dsimp only [Entails, BI.imp, BI.and]; grind imp_elim := by dsimp only [Entails, BI.imp, BI.and] intro _ _ _ h_PQR σ ⟨h_P, h_Q⟩ exact h_PQR σ h_P σ (Preorder.le_refl σ) h_Q sForall_intro := by dsimp only [Entails] intro _ _ h_PΨ σ h_P p hp exact h_PΨ p hp σ h_P sForall_elim := by simp only [Entails] intro _ _ hp _ h_Ψ exact h_Ψ _ hp sExists_intro := by simp only [Entails] intro _ _ hp _ h_Ψ exact ⟨_, hp, h_Ψ⟩ sExists_elim := by simp only [Entails] intro _ _ h_ΦQ σ ⟨p, hp, h_Φ⟩ exact h_ΦQ p hp σ h_Φ sep_mono := by dsimp only [Entails, sep]; tauto emp_sep := ⟨ fun σ h => by rename_i P obtain ⟨σ₁, σ₂, h_s, h_le, _, hP⟩ := h obtain ⟨p, hp, hple⟩ := Krm.le_mul_mono 1 σ₁ σ₂ σ₂ ((σ₁ ⋆ σ₂).get h_s) (Krm.one_le σ₁) (Preorder.le_refl σ₂) ((Option.some_get h_s).symm) have : p = σ₂ := Option.some_injective _ ((Pcm.one_mul σ₂).symm ▸ hp.symm) exact P.2 σ₂ σ (this ▸ hple |>.trans h_le) hP, fun σ hP => ⟨1, σ, by rw [Pcm.one_mul]; rfl, by simp [Pcm.one_mul], trivial, hP⟩⟩ sep_symm := fun σ h => by obtain ⟨σ₁, σ₂, s, h_le, hP, hQ⟩ := h exact ⟨σ₂, σ₁, Pcm.comm σ₂ σ₁ ▸ s, by simp only [Pcm.comm σ₂ σ₁]; exact h_le, hQ, hP⟩ sep_assoc_l := fun σ h => by obtain ⟨σ₁₂, σ₃, s₁₂₃, h_le₁₂₃, ⟨σ₁, σ₂, s₁₂, h_le₁₂, hP, hQ⟩, hR⟩ := h obtain ⟨p, hp, hple⟩ := Krm.le_mul_mono ((σ₁ ⋆ σ₂).get s₁₂) σ₁₂ σ₃ σ₃ ((σ₁₂ ⋆ σ₃).get s₁₂₃) h_le₁₂ (Preorder.le_refl σ₃) ((Option.some_get s₁₂₃).symm) have lhs : (PcmBase.binop <$> (σ₁ ⋆ σ₂) <*> some σ₃).join = some p := by rw [(Option.some_get s₁₂).symm]; change ((σ₁ ⋆ σ₂).get s₁₂) ⋆ σ₃ = some p; exact hp rw [Pcm.assoc] at lhs obtain ⟨bc, hbc, habc⟩ : ∃ bc, σ₂ ⋆ σ₃ = some bc ∧ σ₁ ⋆ bc = some p := by cases hbc : σ₂ ⋆ σ₃ with | none => rw [hbc] at lhs; cases lhs | some bc => rw [hbc] at lhs; change (σ₁ ⋆ bc) = some p at lhs; exact ⟨bc, rfl, lhs⟩ refine ⟨σ₁, bc, habc.symm ▸ rfl, ?_, hP, σ₂, σ₃, hbc.symm ▸ rfl, ?_, hQ, hR⟩ · change (σ₁ ⋆ bc).get (habc.symm ▸ rfl) ≤ σ have : (σ₁ ⋆ bc).get (habc.symm ▸ rfl) = p := by simp [habc] rw [this]; exact hple.trans h_le₁₂₃ · change (σ₂ ⋆ σ₃).get (hbc.symm ▸ rfl) ≤ bc have : (σ₂ ⋆ σ₃).get (hbc.symm ▸ rfl) = bc := by simp [hbc] rw [this] wand_intro := fun h σ hP σQ h_s hQ => by apply h exact ⟨σ, σQ, Pcm.comm σ σQ ▸ h_s, by simp only [Pcm.comm σ σQ]; exact Preorder.le_refl _, hP, hQ⟩ wand_elim := fun h σ hex => by rename_i _ _ R obtain ⟨σ₁, σ₂, s, h_le, hP, hQ⟩ := hex have hr := h σ₁ hP σ₂ (Pcm.comm σ₂ σ₁ ▸ s) hQ simp only [Pcm.comm σ₂ σ₁] at hr exact R.2 _ σ h_le hr persistently_mono := by dsimp only [Entails, persistently]; tauto persistently_idem_2 := by dsimp only [Entails, persistently]; intro _ _ h; exact h persistently_emp_2 := by dsimp only [Entails, persistently, emp]; intro σ P; trivial persistently_and_2 := by dsimp only [Entails, persistently, BI.and]; intro _ _ _ h; exact h persistently_sExists_1 := by dsimp only [Entails, persistently, BI.exists] intro _ σ ⟨p, hp, h⟩ exact ⟨_, ⟨_, rfl⟩, hp, h⟩ persistently_absorb_l := by dsimp only [Entails, persistently, sep]; grind persistently_and_l := fun σ h => by refine ⟨1, σ, ?_, ?_, h.1, h.2⟩ · rw [Pcm.one_mul]; rfl · simp [Pcm.one_mul] later_mono := id later_intro _ := id later_sForall_2 := by dsimp only [Entails, BI.pure, BI.imp, later, sForall] intro Φ σ h p hp have := h ⟨fun σ ↦ ∀ σ', σ ≤ σ' → Φ p → p.1 σ', fun σ₁ σ₂ h₁₂ h₁ σ' h₂ ↦ h₁ σ' (h₁₂.trans h₂)⟩ ⟨_, rfl⟩ exact this σ (Preorder.le_refl σ) hp later_sExists_false := by dsimp only [Entails, later, BI.or, BI.exists, BI.pure] intro _ _ ⟨p, hp⟩ exact Or.inr ⟨_, ⟨_, rfl⟩, hp⟩ later_sep := ⟨fun _ => id, fun _ => id⟩ later_persistently := ⟨fun _ => id, fun _ => id⟩ later_false_em := by dsimp only [Entails, later, BI.or, BI.imp, BI.pure]; grind /-- A KRM generates a separation logic where every proposition is affine (may be dropped in a proof). -/ instance instKrmBIAffine : BIAffine (IProp Resource) where affine P := ⟨by intro Ω _; trivial⟩ end Iris.Instances