Documentation

Mathlib.Control.LawfulFix

Lawful fixed point operators #

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

Main definition #

class LawfulFix (α : Type u_3) [OmegaCompletePartialOrder α] extends Fix :
Type u_3

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
    theorem LawfulFix.fix_eq {α : Type u_3} [OmegaCompletePartialOrder α] [self : LawfulFix α] {f : α →o α} :
    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) :
    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 : ) :
    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.approxChain {α : Type u_1} {β : αType u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) :

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

    Equations
    Instances For
      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)} :
      theorem Part.Fix.approx_mem_approxChain {α : Type u_1} {β : αType u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) {i : } :
      theorem Part.fix_eq_ωSup {α : Type u_1} {β : αType u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) :
      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 : OmegaCompletePartialOrder.Continuous f) :
      Part.fix f = f (Part.fix f)
      @[simp]
      theorem Part.toUnitMono_coe {α : Type u_1} (f : Part α →o Part α) (x : UnitPart α) (u : Unit) :
      (Part.toUnitMono f) x u = f (x u)
      def Part.toUnitMono {α : Type u_1} (f : Part α →o Part α) :
      (UnitPart α) →o UnitPart α

      toUnit as a monotone function

      Equations
      Instances For
        instance Part.lawfulFix {α : Type u_1} :
        Equations
        instance Pi.lawfulFix {α : Type u_1} {β : Type u_3} :
        LawfulFix (αPart β)
        Equations
        @[simp]
        theorem Pi.monotoneCurry_coe (α : Type u_1) (β : αType u_2) (γ : (a : α) → β aType u_3) [(x : α) → (y : β x) → Preorder (γ x y)] (f : (x : (a : α) × β a) → γ x.fst x.snd) (x : α) (y : β x) :
        (Pi.monotoneCurry α β γ) f x y = Sigma.curry f x y
        def Pi.monotoneCurry (α : Type u_1) (β : αType u_2) (γ : (a : α) → β aType 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
        Instances For
          @[simp]
          theorem Pi.monotoneUncurry_coe (α : Type u_1) (β : αType u_2) (γ : (a : α) → β aType u_3) [(x : α) → (y : β x) → Preorder (γ x y)] (f : (x : α) → (y : β x) → γ x y) (x : Sigma β) :
          def Pi.monotoneUncurry (α : Type u_1) (β : αType u_2) (γ : (a : α) → β aType 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
          Instances For
            theorem Pi.continuous_curry (α : Type u_1) (β : αType u_2) (γ : (a : α) → β aType u_3) [(x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)] :
            theorem Pi.continuous_uncurry (α : Type u_1) (β : αType u_2) (γ : (a : α) → β aType u_3) [(x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)] :
            instance Pi.hasFix {α : Type u_1} {β : αType u_2} {γ : (a : α) → β aType u_3} [Fix ((x : Sigma β) → γ x.fst x.snd)] :
            Fix ((x : α) → (y : β x) → γ x y)
            Equations
            • Pi.hasFix = { fix := fun (f : ((x : α) → (y : β x) → γ x y)(x : α) → (y : β x) → γ x y) => Sigma.curry (Fix.fix (Sigma.uncurry f Sigma.curry)) }
            theorem Pi.uncurry_curry_continuous {α : Type u_1} {β : αType u_2} {γ : (a : α) → β aType u_3} [(x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)] {f : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y} (hc : OmegaCompletePartialOrder.Continuous f) :
            instance Pi.lawfulFix' {α : Type u_1} {β : αType u_2} {γ : (a : α) → β aType u_3} [(x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)] [LawfulFix ((x : Sigma β) → γ x.fst x.snd)] :
            LawfulFix ((x : α) → (y : β x) → γ x y)
            Equations