Recursion

Difficulty: optional — 9 definitions, 0 abbreviations, 1 lemmas, 5 theorems, 0 examples.

definition lemma theorem
legend

A specification says which values a relation is allowed to take. A recursive specification says that while already speaking of the very relation it is about: the value at one place is described in terms of the values at other places. Read as a demand, such a specification asks for a relation that answers itself, a fixed point.

Self-reference of this kind is settled the same way any other definition is settled. A recursive specification defines a relation exactly when it has one fixed point and no more, so recursion is definite description again, now applied to relations rather than to elements. The circle closes because uniqueness leaves the specification a single answer.

Two demands make a specification well behaved. Handed a relation that gives at least one value everywhere, it again allows at least one value everywhere. Handed a relation that gives at most one value everywhere, it again allows at most one value everywhere. A specification with both properties and a unique fixed point is a recursive definition, and the relation it defines is written as its denotation.

The specification \(\Phi\) is insensitive to the relation it speaks of: handed any two relations, it asks for the same thing.

structure Structure.Arithmetic.Predicative.{u_1, u_2} {L : Type u_1} {V : Type u_2}
  (Φ : (L → V → Prop) → L → V → Prop) : Prop

  • The specification asks the same of every relation.

    const : ∀ (R R' : L → V → Prop), Φ R = Φ R'
Show details

Outer dependencies: (none)

Lean core dependencies: Eq

Used by: Structure.Arithmetic.instDefForallForallPropFixedPointOfPredicative

The relation \(R\) answers the specification \(\Phi\): applying \(\Phi\) to \(R\) gives back \(R\) itself.

recursive-definition
structure Structure.Arithmetic.FixedPoint.{u_1, u_2} {L : Type u_1} {V : Type u_2}
  (Φ : (L → V → Prop) → L → V → Prop) (R : L → V → Prop) : Prop

  • Applying the specification to the relation gives back that relation.

    self : Φ R = R
Show details

Outer dependencies: (none)

Lean core dependencies: Eq

Used by: Structure.Arithmetic.Recursive, Structure.Arithmetic.fixedPoint_iter, Structure.Arithmetic.instDefForallForallPropFixedPointOfPredicative, Structure.Arithmetic.instDefForallForallPropFixedPointOfRecursive, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent, Structure.Arithmetic.rec, Structure.Arithmetic.rec_primitive, Structure.Arithmetic.rec_spec

A specification that is insensitive to the relation it speaks of is already a definition: it denotes its own constant value, which is also its only fixed point.

instance Structure.Arithmetic.instDefForallForallPropFixedPointOfPredicative.{u_1, u_2} {L : Type u_1}
  {V : Type u_2} {Φ : (L → V → Prop) → L → V → Prop} [Structure.Arithmetic.Predicative Φ] :
  Structure.Arithmetic.Def (Structure.Arithmetic.FixedPoint Φ)
Show details 
fun {L} {V} {Φ} [Structure.Arithmetic.Predicative Φ] =>
  {
    ex :=
      Exists.intro (Φ fun x x_1 => True)
        { self := Structure.Arithmetic.Predicative.const (Φ fun x x_1 => True) fun x x_1 => True },
    uniq := fun R R' hR hR' =>
      Eq.mpr (id (congrArg (fun _a => _a = R') (Eq.symm Structure.Arithmetic.FixedPoint.self)))
        (Eq.mpr (id (congrArg (fun _a => Φ R = _a) (Eq.symm Structure.Arithmetic.FixedPoint.self)))
          (Eq.mpr
            (id (congrArg (fun _a => _a = Φ R') (Structure.Arithmetic.Predicative.const R R')))
            (Eq.refl (Φ R')))) }

Complexity: 529 (size of the value term)

Outer dependencies: Structure.Arithmetic.Def, Structure.Arithmetic.FixedPoint, Structure.Arithmetic.Predicative

Lean core dependencies: Eq, Eq.mpr, Eq.symm, True, congrArg, id

Used by: (none)

The specification \(\Phi\) does consult the relation it speaks of.

structure Structure.Arithmetic.Impredicative.{u_1, u_2} {L : Type u_1} {V : Type u_2}
  (Φ : (L → V → Prop) → L → V → Prop) : Prop

  • Some two relations are asked different things.

    not_const : ¬∀ (R R' : L → V → Prop), Φ R = Φ R'
Show details

Outer dependencies: (none)

Lean core dependencies: Eq, Not

Used by: (none)

A relation with at least one and at most one value at each place defines the value at each place.

instance Structure.Arithmetic.instDefOfSerialOfUnivalent.{u_1, u_2} {L : Type u_1} {V : Type u_2}
  {R : L → V → Prop} [Structure.Arithmetic.Serial R] [Structure.Arithmetic.Univalent R] (a : L) :
  Structure.Arithmetic.Def (R a)
Show details 
fun {L} {V} {R} [Structure.Arithmetic.Serial R] [Structure.Arithmetic.Univalent R] a =>
  { ex := Structure.Arithmetic.Serial.ex a, uniq := Structure.Arithmetic.Univalent.uniq a }

Complexity: 59 (size of the value term)

Outer dependencies: Structure.Arithmetic.Def, Structure.Arithmetic.Serial, Structure.Arithmetic.Univalent

Used by: Structure.Arithmetic.fixedPoint_iter, Structure.Arithmetic.step, Structure.Arithmetic.step_spec

Handed a relation with a value everywhere, the specification \(\Phi\) allows at least one value at each place.

structure Structure.Arithmetic.Totally.{u_1, u_2} {L : Type u_1} {V : Type u_2}
  (Φ : (L → V → Prop) → L → V → Prop) : Prop

  • Seriality is passed on.

    ex : ∀ (R : L → V → Prop), Structure.Arithmetic.Serial R → Structure.Arithmetic.Serial (Φ R)
Show details

Outer dependencies: (none)

Inner dependencies: Structure.Arithmetic.Serial

Used by: Structure.Arithmetic.Recursive, Structure.Arithmetic.instSerialOfTotally, Structure.Arithmetic.instTotallyPrimitiveOfSerial

Handed a relation with at most one value everywhere, the specification \(\Phi\) allows at most one value at each place.

structure Structure.Arithmetic.Univalently.{u_1, u_2} {L : Type u_1} {V : Type u_2}
  (Φ : (L → V → Prop) → L → V → Prop) : Prop

  • Univalence is passed on.

    uniq : ∀ (R : L → V → Prop), Structure.Arithmetic.Univalent R → Structure.Arithmetic.Univalent (Φ R)
Show details

Outer dependencies: (none)

Inner dependencies: Structure.Arithmetic.Univalent

Used by: Structure.Arithmetic.Recursive, Structure.Arithmetic.instUnivalentOfUnivalently, Structure.Arithmetic.instUnivalentlyPrimitiveOfUnivalent

instance Structure.Arithmetic.instSerialOfTotally.{u_1, u_2} {L : Type u_1} {V : Type u_2}
  {Φ : (L → V → Prop) → L → V → Prop} [Structure.Arithmetic.Totally Φ] (R : L → V → Prop)
  [Structure.Arithmetic.Serial R] : Structure.Arithmetic.Serial (Φ R)
Show details 
fun {L} {V} {Φ} [Structure.Arithmetic.Totally Φ] R [inst_1 : Structure.Arithmetic.Serial R] =>
  Structure.Arithmetic.Totally.ex R inst_1

Complexity: 51 (size of the value term)

Outer dependencies: Structure.Arithmetic.Serial, Structure.Arithmetic.Totally

Used by: (none)

instance Structure.Arithmetic.instUnivalentOfUnivalently.{u_1, u_2} {L : Type u_1} {V : Type u_2}
  {Φ : (L → V → Prop) → L → V → Prop} [Structure.Arithmetic.Univalently Φ] (R : L → V → Prop)
  [Structure.Arithmetic.Univalent R] : Structure.Arithmetic.Univalent (Φ R)
Show details 
fun {L} {V} {Φ} [Structure.Arithmetic.Univalently Φ] R
    [inst_1 : Structure.Arithmetic.Univalent R] =>
  Structure.Arithmetic.Univalently.uniq R inst_1

Complexity: 51 (size of the value term)

Outer dependencies: Structure.Arithmetic.Univalent, Structure.Arithmetic.Univalently

Used by: (none)

A recursive definition: a specification that speaks of the very relation it is about, that is well behaved in both respects, and that exactly one relation answers. Uniqueness of the answer is what resolves the self-reference.

structure Structure.Arithmetic.Recursive.{u_1, u_2} {L : Type u_1} {V : Type u_2}
  (Φ : (L → V → Prop) → L → V → Prop) : Prop

  • Seriality is passed on.

    (inherited from Structure.Arithmetic.Totally)

    ex : ∀ (R : L → V → Prop), Structure.Arithmetic.Serial R → Structure.Arithmetic.Serial (Φ R)

  • Univalence is passed on.

    (inherited from Structure.Arithmetic.Univalently)

    uniq : ∀ (R : L → V → Prop), Structure.Arithmetic.Univalent R → Structure.Arithmetic.Univalent (Φ R)

  • Exactly one relation answers the specification.

    defines : Structure.Arithmetic.Def (Structure.Arithmetic.FixedPoint Φ)
Show details

Outer dependencies: (none)

Inner dependencies: Structure.Arithmetic.Def, Structure.Arithmetic.FixedPoint, Structure.Arithmetic.Totally, Structure.Arithmetic.Univalently

Used by: Structure.Arithmetic.PrimitiveRecursive, Structure.Arithmetic.instDefForallForallPropFixedPointOfRecursive, Structure.Arithmetic.rec, Structure.Arithmetic.rec_spec

instance Structure.Arithmetic.instDefForallForallPropFixedPointOfRecursive.{u_1, u_2} {L : Type u_1}
  {V : Type u_2} {Φ : (L → V → Prop) → L → V → Prop} [Structure.Arithmetic.Recursive Φ] :
  Structure.Arithmetic.Def (Structure.Arithmetic.FixedPoint Φ)
Show details 
fun {L} {V} {Φ} [Structure.Arithmetic.Recursive Φ] => Structure.Arithmetic.Recursive.defines

Complexity: 33 (size of the value term)

Outer dependencies: Structure.Arithmetic.Def, Structure.Arithmetic.FixedPoint, Structure.Arithmetic.Recursive

Used by: Structure.Arithmetic.rec, Structure.Arithmetic.rec_spec

The relation that the recursive definition \(\Phi\) denotes.

def Structure.Arithmetic.rec.{u_1, u_2} {L : Type u_1} {V : Type u_2}
  (Φ : (L → V → Prop) → L → V → Prop) [Structure.Arithmetic.Recursive Φ] : L → V → Prop
Show details 
| Structure.Arithmetic.rec Φ = Structure.Arithmetic.the (Structure.Arithmetic.FixedPoint Φ)

Complexity: 49 (size of the value term)

Outer dependencies: Structure.Arithmetic.Recursive

Inner dependencies: Structure.Arithmetic.FixedPoint, Structure.Arithmetic.instDefForallForallPropFixedPointOfRecursive, Structure.Arithmetic.the

Lean core dependencies: Eq

Used by: Structure.Arithmetic.Exp, Structure.Arithmetic.ExpSpec, Structure.Arithmetic.Plus, Structure.Arithmetic.Times, Structure.Arithmetic.TimesSpec, Structure.Arithmetic.exp_base, Structure.Arithmetic.exp_step, Structure.Arithmetic.instSerialRecPrimitive, Structure.Arithmetic.instUnivalentRecPrimitive, Structure.Arithmetic.rec_base, Structure.Arithmetic.rec_primitive, Structure.Arithmetic.rec_spec, Structure.Arithmetic.rec_step, Structure.Arithmetic.times_base, Structure.Arithmetic.times_step

What a recursive definition denotes answers that definition.

theorem Structure.Arithmetic.rec_spec.{u_1, u_2} {L : Type u_1} {V : Type u_2}
  (Φ : (L → V → Prop) → L → V → Prop) [Structure.Arithmetic.Recursive Φ] :
  Φ (Structure.Arithmetic.rec Φ) = Structure.Arithmetic.rec Φ
Show details 
fun {L} {V} Φ [Structure.Arithmetic.Recursive Φ] => Structure.Arithmetic.FixedPoint.self

Complexity: 83 (size of the value term)

Dependencies: Structure.Arithmetic.Recursive, Structure.Arithmetic.rec

Proof dependencies: Structure.Arithmetic.FixedPoint, Structure.Arithmetic.instDefForallForallPropFixedPointOfRecursive, Structure.Arithmetic.the, Structure.Arithmetic.the_spec

Lean core dependencies: Eq

Used by: Structure.Arithmetic.rec_base, Structure.Arithmetic.rec_step

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionlemmatheoremdeclared elsewheredependencyproof dependency
legend