mathlib3 documentation

control.lawful_fix

Lawful fixed point operators #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This module defines the laws required of a has_fix instance, using the theory of omega complete partial orders (ωCPO). Proofs of the lawfulness of all has_fix instances in control.fix are provided.

Main definition #

class lawful_fix

@[class]

structure lawful_fix (α : Type u_3) [omega_complete_partial_order α] :

Type u_3

to_has_fix : has_fix α
fix_eq : ∀ {f : α →o α}, omega_complete_partial_order.continuous f → has_fix.fix ⇑f = ⇑f (has_fix.fix ⇑f)

Intuitively, a fixed point operator fix is lawful if it satisfies fix f = f (fix f) for all f, but this is inconsistent / uninteresting in most cases due to the existence of "exotic" functions f, such as the function that is defined iff its argument is not, familiar from the halting problem. Instead, this requirement is limited to only functions that are continuous in the sense of ω-complete partial orders, which excludes the example because it is not monotone (making the input argument less defined can make f more defined).

Instances of this typeclass

Instances of other typeclasses for lawful_fix

lawful_fix.has_sizeof_inst

theorem lawful_fix.fix_eq' {α : Type u_1} [omega_complete_partial_order α] [lawful_fix α] {f : α → α} (hf : omega_complete_partial_order.continuous' f) :

has_fix.fix f = f (has_fix.fix f)

theorem part.fix.approx_mono' {α : Type u_1} {β : α → Type u_2} (f : (Π (a : α), part (β a)) →o Π (a : α), part (β a)) {i : ℕ} :

part.fix.approx ⇑f i ≤ part.fix.approx ⇑f i.succ

theorem part.fix.approx_mono {α : Type u_1} {β : α → Type u_2} (f : (Π (a : α), part (β a)) →o Π (a : α), part (β a)) ⦃i j : ℕ⦄ (hij : i ≤ j) :

part.fix.approx ⇑f i ≤ part.fix.approx ⇑f j

theorem part.fix.mem_iff {α : Type u_1} {β : α → Type u_2} (f : (Π (a : α), part (β a)) →o Π (a : α), part (β a)) (a : α) (b : β a) :

b ∈ part.fix ⇑f a ↔ ∃ (i : ℕ), b ∈ part.fix.approx ⇑f i a

theorem part.fix.approx_le_fix {α : Type u_1} {β : α → Type u_2} (f : (Π (a : α), part (β a)) →o Π (a : α), part (β a)) (i : ℕ) :

part.fix.approx ⇑f i ≤ part.fix ⇑f

theorem part.fix.exists_fix_le_approx {α : Type u_1} {β : α → Type u_2} (f : (Π (a : α), part (β a)) →o Π (a : α), part (β a)) (x : α) :

∃ (i : ℕ), part.fix ⇑f x ≤ part.fix.approx ⇑f i x

def part.fix.approx_chain {α : Type u_1} {β : α → Type u_2} (f : (Π (a : α), part (β a)) →o Π (a : α), part (β a)) :

omega_complete_partial_order.chain (Π (a : α), part (β a))

The series of approximations of fix f (see approx) as a chain

Equations

part.fix.approx_chain f = {to_fun := part.fix.approx ⇑f, monotone' := _}

theorem part.fix.le_f_of_mem_approx {α : Type u_1} {β : α → Type u_2} (f : (Π (a : α), part (β a)) →o Π (a : α), part (β a)) {x : Π (a : α), part (β a)} :

x ∈ part.fix.approx_chain f → x ≤ ⇑f x

theorem part.fix.approx_mem_approx_chain {α : Type u_1} {β : α → Type u_2} (f : (Π (a : α), part (β a)) →o Π (a : α), part (β a)) {i : ℕ} :

part.fix.approx ⇑f i ∈ part.fix.approx_chain f

theorem part.fix_eq_ωSup {α : Type u_1} {β : α → Type u_2} (f : (Π (a : α), part (β a)) →o Π (a : α), part (β a)) :

part.fix ⇑f = omega_complete_partial_order.ωSup (part.fix.approx_chain f)

theorem part.fix_le {α : Type u_1} {β : α → Type u_2} (f : (Π (a : α), part (β a)) →o Π (a : α), part (β a)) {X : Π (a : α), part (β a)} (hX : ⇑f X ≤ X) :

part.fix ⇑f ≤ X

theorem part.fix_eq {α : Type u_1} {β : α → Type u_2} {f : (Π (a : α), part (β a)) →o Π (a : α), part (β a)} (hc : omega_complete_partial_order.continuous f) :

part.fix ⇑f = ⇑f (part.fix ⇑f)

def part.to_unit_mono {α : Type u_1} (f : part α →o part α) :

(unit → part α) →o unit → part α

to_unit as a monotone function

Equations

part.to_unit_mono f = {to_fun := λ (x : unit → part α) (u : unit), ⇑f (x u), monotone' := _}

@[simp]

theorem part.to_unit_mono_coe {α : Type u_1} (f : part α →o part α) (x : unit → part α) (u : unit) :

⇑(part.to_unit_mono f) x u = ⇑f (x u)

theorem part.to_unit_cont {α : Type u_1} (f : part α →o part α) (hc : omega_complete_partial_order.continuous f) :

omega_complete_partial_order.continuous (part.to_unit_mono f)

@[protected, instance]

def part.lawful_fix {α : Type u_1} :

lawful_fix (part α)

Equations

part.lawful_fix = {to_has_fix := part.has_fix α, fix_eq := _}

@[protected, instance]

def pi.lawful_fix {α : Type u_1} {β : Type u_2} :

lawful_fix (α → part β)

Equations

pi.lawful_fix = {to_has_fix := pi.part.has_fix β, fix_eq := _}

@[simp]

theorem pi.monotone_curry_coe (α : Type u_1) (β : α → Type u_2) (γ : Π (a : α), β a → Type u_3) [Π (x : α) (y : β x), preorder (γ x y)] (f : Π (x : Σ (a : α), β a), γ x.fst x.snd) (x : α) (y : β x) :

⇑(pi.monotone_curry α β γ) f x y = sigma.curry f x y

def pi.monotone_curry (α : Type u_1) (β : α → Type u_2) (γ : Π (a : α), β a → Type u_3) [Π (x : α) (y : β x), preorder (γ x y)] :

(Π (x : Σ (a : α), β a), γ x.fst x.snd) →o Π (a : α) (b : β a), γ a b

sigma.curry as a monotone function.

Equations

pi.monotone_curry α β γ = {to_fun := sigma.curry γ, monotone' := _}

@[simp]

theorem pi.monotone_uncurry_coe (α : Type u_1) (β : α → Type u_2) (γ : Π (a : α), β a → Type u_3) [Π (x : α) (y : β x), preorder (γ x y)] (f : Π (x : α) (y : (λ (a : α), β a) x), (λ (a : α) (b : β a), γ a b) x y) (x : Σ (a : α), β a) :

⇑(pi.monotone_uncurry α β γ) f x = sigma.uncurry f x

def pi.monotone_uncurry (α : Type u_1) (β : α → Type u_2) (γ : Π (a : α), β a → Type u_3) [Π (x : α) (y : β x), preorder (γ x y)] :

(Π (a : α) (b : β a), γ a b) →o Π (x : Σ (a : α), β a), γ x.fst x.snd

sigma.uncurry as a monotone function.

Equations

pi.monotone_uncurry α β γ = {to_fun := sigma.uncurry (λ (a : α) (b : β a), γ a b), monotone' := _}

theorem pi.continuous_curry (α : Type u_1) (β : α → Type u_2) (γ : Π (a : α), β a → Type u_3) [Π (x : α) (y : β x), omega_complete_partial_order (γ x y)] :

omega_complete_partial_order.continuous (pi.monotone_curry α β γ)

theorem pi.continuous_uncurry (α : Type u_1) (β : α → Type u_2) (γ : Π (a : α), β a → Type u_3) [Π (x : α) (y : β x), omega_complete_partial_order (γ x y)] :

omega_complete_partial_order.continuous (pi.monotone_uncurry α β γ)

@[protected, instance]

def pi.has_fix {α : Type u_1} {β : α → Type u_2} {γ : Π (a : α), β a → Type u_3} [has_fix (Π (x : sigma β), γ x.fst x.snd)] :

has_fix (Π (x : α) (y : β x), γ x y)

Equations

pi.has_fix = {fix := λ (f : (Π (x : α) (y : β x), γ x y) → Π (x : α) (y : β x), γ x y), sigma.curry (has_fix.fix (sigma.uncurry ∘ f ∘ sigma.curry))}

theorem pi.uncurry_curry_continuous {α : Type u_1} {β : α → Type u_2} {γ : Π (a : α), β a → Type u_3} [Π (x : α) (y : β x), omega_complete_partial_order (γ x y)] {f : (Π (x : α) (y : β x), γ x y) →o Π (x : α) (y : β x), γ x y} (hc : omega_complete_partial_order.continuous f) :

omega_complete_partial_order.continuous ((pi.monotone_uncurry α β γ).comp (f.comp (pi.monotone_curry α β γ)))

@[protected, instance]

def pi.pi.lawful_fix' {α : Type u_1} {β : α → Type u_2} {γ : Π (a : α), β a → Type u_3} [Π (x : α) (y : β x), omega_complete_partial_order (γ x y)] [lawful_fix (Π (x : sigma β), γ x.fst x.snd)] :

lawful_fix (Π (x : α) (y : β x), γ x y)

Equations

pi.pi.lawful_fix' = {to_has_fix := pi.has_fix lawful_fix.to_has_fix, fix_eq := _}