Project-declaredLean 4.32.1 · null

Mon Pred sbi emp valid exist

Iris.BI.MonPred.monPred_sbi_emp_valid_exist

separation logic program logic semantics mon pred

Plain-language statement

A monotone predicate P is objective if its value does not depend on the index: P i ⊢ P j for all i j. Equivalently P ⊣⊢ <obj> P. -/ @[rocq_alias Objective] class Objective {I : BiIndex} {PROP : Type _} [BI PROP] (P : MonPred I PROP) : Prop where objective_at : ∀ i j : I.car, P.monPred_at i ⊢ P.monPred_at j namespace MonPred variable {I : BiIndex...

Exact Lean statement

@[rocq_alias monPred_sbi_emp_valid_exist]
theorem monPred_sbi_emp_valid_exist {bot : I.car} [BiIndexBottom I bot] [SbiEmpValidExist PROP] :
    SbiEmpValidExist (MonPred I PROP) where
  siEmpValid_sExists_1 Ψ

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

@[rocq_alias monPred_sbi_emp_valid_exist]theorem monPred_sbi_emp_valid_exist {bot : I.car} [BiIndexBottom I bot] [SbiEmpValidExist PROP] :    SbiEmpValidExist (MonPred I PROP) where  siEmpValid_sExists_1 Ψ := by    refine (siEmpValid_mono (forall_elim bot)).trans ?_    refine (siEmpValid_sExists_1      (fun p => ∃ q : MonPred I PROP, Ψ q ∧ q.monPred_at bot = p)).trans ?_    refine exists_elim fun p => pure_elim_left fun ⟨q, hΨ, hq⟩ => ?_    subst hq    refine exists_intro_trans q (and_intro (pure_intro hΨ) ?_)    exact (siEmpValid_mono (forall_intro fun k => q.monPred_mono (BiIndexBottom.bot_le k)))

Project: Iris-Lean
License: Apache-2.0
Commit: 37f53e0ac065
Source: Iris/Iris/BI/MonPred.lean:1562-1572

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.32.1

Co Pset Raw eq

CoPset.coPsetRaw_eq

Plain-language statement

Two CoPsetRaw trees are equal if they have the same membership function and both are well-formed.

separation logicprogram logicsemantics

Source project: Iris-Lean

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.1

Inj on of nodup map

FromMathlib.inj_on_of_nodup_map

Plain-language statement

NB. Copied from Mathlib

separation logicprogram logicsemantics

Source project: Iris-Lean

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.1

Big Op L hom weak

Iris.Algebra.BigOpL.bigOpL_hom_weak

Plain-language statement

Weak monoid homomorphisms distribute over non-empty big ops.

separation logicprogram logicsemantics

Source project: Iris-Lean

Person-level attribution pending.

View proof record