Is this function present in mathlib4?

Stream: new members

[Kamila Szewczyk]

Can I find something like this in mathlib4 already:

def fixedPoint {α : Type} (f : Set α → Set α) (s : Set α) : Set α :=
  let step : Set α → Set α := λ t => s ∪ (f t)
  let result : Nat → Set α := λ n => Nat.iterate step n s
  let limit : Set α := ⋂ (n : Nat), result n
  limit

[Richard Copley]

Did you intend f (fixedPoint f s) = fixedPoint f s to always be true?

import Mathlib.Tactic.PushNeg
import Mathlib.Data.Set.Lattice
import Mathlib.Logic.Function.Iterate

def fixedPoint {α : Type} (f : Set α → Set α) (s : Set α) : Set α :=
  let step : Set α → Set α := λ t => s ∪ (f t)
  let result : Nat → Set α := λ n => Nat.iterate step n s
  let limit : Set α := ⋂ (n : Nat), result n
  limit

theorem fixedPoint_apply' {α : Type} (f : Set α → Set α) (s : Set α) :
    fixedPoint f s = ⋂ (n : Nat), (fun t => s ∪ f t)^[n] s :=
  rfl

example : ¬∀ (α : Type) (f : Set α → Set α) (s : Set α),
    f (fixedPoint f s) = fixedPoint f s := by
  push_neg
  use ℕ, fun _ => Set.univ, ∅
  rw [fixedPoint_apply', ← Set.inter_iInter_nat_succ, Function.iterate_zero_apply,
    Set.empty_inter, ← Set.nonempty_iff_ne_empty, ← Set.nonempty_iff_univ_nonempty]
  infer_instance

[Kamila Szewczyk]

Richard Copley said:

Did you intend f (fixedPoint f s) = fixedPoint f s to always be true?

import Mathlib.Tactic.PushNeg
import Mathlib.Data.Set.Lattice
import Mathlib.Logic.Function.Iterate

def fixedPoint {α : Type} (f : Set α → Set α) (s : Set α) : Set α :=
  let step : Set α → Set α := λ t => s ∪ (f t)
  let result : Nat → Set α := λ n => Nat.iterate step n s
  let limit : Set α := ⋂ (n : Nat), result n
  limit

theorem fixedPoint_apply' {α : Type} (f : Set α → Set α) (s : Set α) :
    fixedPoint f s = ⋂ (n : Nat), (fun t => s ∪ f t)^[n] s :=
  rfl

example : ¬∀ (α : Type) (f : Set α → Set α) (s : Set α),
    f (fixedPoint f s) = fixedPoint f s := by
  push_neg
  use ℕ, fun _ => Set.univ, ∅
  rw [fixedPoint_apply', ← Set.inter_iInter_nat_succ, Function.iterate_zero_apply,
    Set.empty_inter, ← Set.nonempty_iff_ne_empty, ← Set.nonempty_iff_univ_nonempty]
  infer_instance

oh, yes... thank you! I wonder why mathlib doesn't have this already...

[Richard Copley]

I'm confused! What's it useful for?

[Kamila Szewczyk]

iterating functions in a fixed point, many programming languages already have it as a combinator. e.g. APL: ⍣≡

[Sébastien Gouëzel]

Richard has just shown that, precisely, your definition doesn't give a fixpoint in general.