@[implicit_reducible]

noncomputable instance Lean.Order.CompleteLattice.instMinCompleteLattice {α : Type u_1} [CompleteLattice α] : Min α

The binary meet of a complete lattice, as the infimum of {x, y}.

Equations

• Lean.Order.CompleteLattice.instMinCompleteLattice = { min := fun (x y : α) => Lean.Order.inf fun (z : α) => z = x ∨ z = y }

noncomputable def Lean.Order.CompleteLattice.top {α : Sort u_1} [CompleteLattice α] : α

The top element of a complete lattice, as the supremum of the whole carrier.

Equations

• Lean.Order.CompleteLattice.top = Lean.Order.CompleteLattice.sup fun (x : α) => True

def Lean.Order.CompleteLattice.«term⊤ₚ» : ParserDescr

Notation ⊤ₚ for the Paco lattice top (to avoid clashing with core's ⊤).

Equations

• Lean.Order.CompleteLattice.«term⊤ₚ» = Lean.ParserDescr.node `Lean.Order.CompleteLattice.«term⊤ₚ» 1024 (Lean.ParserDescr.symbol "⊤ₚ")

def Lean.Order.CompleteLattice.«term_⊓ₚ_» : TrailingParserDescr

Notation x ⊓ₚ y for the Paco lattice meet (to avoid clashing with core's ⊓).

Equations

• One or more equations did not get rendered due to their size.

theorem Lean.Order.CompleteLattice.top_spec {α : Sort u_1} [CompleteLattice α] (x : α) : PartialOrder.rel x top

theorem Lean.Order.CompleteLattice.meet_spec {α : Type u_1} {z : α} [CompleteLattice α] (x y : α) : PartialOrder.rel z (min x y) ↔ PartialOrder.rel z x ∧ PartialOrder.rel z y

theorem Lean.Order.CompleteLattice.meet_le_left' {α : Type u_1} {z y : α} [CompleteLattice α] (x : α) : PartialOrder.rel x z → PartialOrder.rel (min x y) z

theorem Lean.Order.CompleteLattice.meet_le_right' {α : Type u_1} {z x : α} [CompleteLattice α] (y : α) : PartialOrder.rel y z → PartialOrder.rel (min x y) z

theorem Lean.Order.CompleteLattice.meet_top {α : Type u_1} [CompleteLattice α] (x : α) : min x top = x

theorem Lean.Order.CompleteLattice.meet_comm {α : Type u_1} [CompleteLattice α] (x y : α) : min x y = min y x

theorem Lean.Order.CompleteLattice.meet_assoc {α : Type u_1} [CompleteLattice α] (x y z : α) : min (min x y) z = min x (min y z)

theorem Lean4Itree.monotonize_mon {α : Type u_1} [Lean.Order.CompleteLattice α] (f : α → α) (r : α) : Lean.Order.monotone fun (x : α) => Lean.Order.inf fun (z : α) => ∃ (y : α), z = f y ∧ Lean.Order.PartialOrder.rel (min r x) y

theorem Lean4Itree.plfp_arg_mon {α : Type u_1} [Lean.Order.CompleteLattice α] {f : α → α} (hm : Lean.Order.monotone f) (r : α) : Lean.Order.monotone fun (x : α) => f (min r x)

noncomputable def Lean4Itree.plfp {α : Type u_1} [Lean.Order.CompleteLattice α] (f : α → α) {hm : Lean.Order.monotone f} (r : α) : α

Parameterized least fixed point, we don't "monotonize" f (⌈f⌉) as in paco for now version in paco: lfp (λ x => inf (λ z => ∃ y, z = f y ∧ r ⊓ₚ x ⊑ y)

Equations

• Lean4Itree.plfp f r = Lean.Order.lfp_monotone (fun (x : α) => f (min r x)) ⋯

noncomputable def Lean4Itree.uplfp {α : Type u_1} [Lean.Order.CompleteLattice α] (f : α → α) {hm : Lean.Order.monotone f} (r : α) : α

The "unfolded" parameterized least fixed point r ⊓ₚ plfp f r.

Equations

• Lean4Itree.uplfp f r = min r (Lean4Itree.plfp f r)

theorem Lean4Itree.plfp_mon {α : Type u_1} [Lean.Order.CompleteLattice α] {f : α → α} (hm : Lean.Order.monotone f) : Lean.Order.monotone (plfp f)

theorem Lean4Itree.plfp_init {α : Type u_1} [Lean.Order.CompleteLattice α] {f : α → α} (hm : Lean.Order.monotone f) : Lean.Order.lfp_monotone f hm = plfp f Lean.Order.CompleteLattice.top

theorem Lean4Itree.plfp_unfold {α : Type u_1} {r : α} [Lean.Order.CompleteLattice α] {f : α → α} (hm : Lean.Order.monotone f) : plfp f r = f (uplfp f r)

theorem Lean4Itree.uplfp_goal {α : Type u_1} {r z : α} [Lean.Order.CompleteLattice α] {f : α → α} (hm : Lean.Order.monotone f) : Lean.Order.PartialOrder.rel r z ∨ Lean.Order.PartialOrder.rel (plfp f r) z → Lean.Order.PartialOrder.rel (uplfp f r) z

theorem Lean4Itree.uplfp_hyp {α : Type u_1} {z r : α} [Lean.Order.CompleteLattice α] {f : α → α} (hm : Lean.Order.monotone f) : Lean.Order.PartialOrder.rel z (uplfp f r) → Lean.Order.PartialOrder.rel z r ∧ Lean.Order.PartialOrder.rel z (plfp f r)

theorem Lean4Itree.fun_sup_equiv {α : Sort u} {β : α → Sort v} [(x : α) → Lean.Order.CompleteLattice (β x)] (c : ((x : α) → β x) → Prop) (x : α) : Lean.Order.fun_sup c x = Lean.Order.inf fun (y : β x) => ∀ (f : (x : α) → β x), c f → Lean.Order.PartialOrder.rel (f x) y

theorem Lean4Itree.plfp_acc_aux {α : Type u_1} [Lean.Order.CompleteLattice α] {f : α → α} (hm : Lean.Order.monotone f) (r x : α) : Lean.Order.PartialOrder.rel (plfp f r) x ↔ Lean.Order.PartialOrder.rel (plfp f (min r x)) x

theorem Lean4Itree.plfp_acc {α : Type u_1} [Lean.Order.CompleteLattice α] {f : α → α} (hm : Lean.Order.monotone f) (l r : α) (obg : ∀ (φ : α), Lean.Order.PartialOrder.rel φ r → Lean.Order.PartialOrder.rel φ l → Lean.Order.PartialOrder.rel (plfp f φ) l) : Lean.Order.PartialOrder.rel (plfp f r) l