PrimitiveRecursion

Difficulty: optional — 4 definitions, 1 abbreviations, 11 lemmas, 10 theorems, 0 examples.

definition abbreviation lemma theorem

legend

Primitive recursion is the shape of recursive definition that a model of arithmetic supports by itself. A primitive specification is given by two pieces: a base value, taken at a zero, and a step relation, applied to the value at the predecessor everywhere else. The two clauses are kept apart by asking of the second that the place is no zero.

Such a specification is always a recursive definition, provided the step relation gives exactly one value at each place. It allows at least one value everywhere, since every element other than a zero has a predecessor. It allows at most one, since that predecessor is unique. And it has one fixed point and no more, which is where the layout of a model earns its keep: being below is well founded, because a nonempty collection meets a finite initial segment, whose least element is least in the collection. So values may be computed by descending along predecessors, and any two answers to the specification agree by induction along that descent.

NoteStructure.Arithmetic.Primitive

A primitive specification with base \(b\) and step relation \(g\): at a zero the value is \(b\), and at any other place it is a \(g\)-successor of the value at the predecessor.

primitive-recursion

def Structure.Arithmetic.Primitive.{u_1, u_2} {U : Type u_1} {V : Type u_2}
  [Structure.Arithmetic.Arith U] (b : V) (g : V → V → Prop) : (U → V → Prop) → U → V → Prop

Show details

| Structure.Arithmetic.Primitive b g R a v =
  (Structure.Arithmetic.Z a ∧ v = b ∨
    ¬Structure.Arithmetic.Z a ∧ ∃ u w, Structure.Arithmetic.S u a ∧ R u w ∧ g w v)

Complexity: 95 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith

Inner dependencies: Structure.Arithmetic.S, Structure.Arithmetic.Z

Lean core dependencies: And, Eq, Exists, Not, Or

Used by: Structure.Arithmetic.ExpSpec, Structure.Arithmetic.PlusSpec, Structure.Arithmetic.PrimitiveRecursive, Structure.Arithmetic.TimesSpec, Structure.Arithmetic.fixedPoint_iter, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent, Structure.Arithmetic.instSerialRecPrimitive, Structure.Arithmetic.instTotallyPrimitiveOfSerial, Structure.Arithmetic.instUnivalentRecPrimitive, Structure.Arithmetic.instUnivalentlyPrimitiveOfUnivalent, Structure.Arithmetic.rec_base, Structure.Arithmetic.rec_primitive, Structure.Arithmetic.rec_step

NoteStructure.Arithmetic.PrimitiveRecursive

A primitive recursive definition.

abbrev Structure.Arithmetic.PrimitiveRecursive.{u_1, u_2} {U : Type u_1} {V : Type u_2}
  [Structure.Arithmetic.Arith U] (b : V) (g : V → V → Prop) : Prop

Show details

| Structure.Arithmetic.PrimitiveRecursive b g =
  Structure.Arithmetic.Recursive (Structure.Arithmetic.Primitive b g)

Complexity: 33 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith

Inner dependencies: Structure.Arithmetic.Primitive, Structure.Arithmetic.Recursive

Used by: Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent

ImportantStructure.Arithmetic.instSerialS

The successor relation serves as a step relation: it gives a value at each place.

instance Structure.Arithmetic.instSerialS.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] :
  Structure.Arithmetic.Serial Structure.Arithmetic.S

Show details

fun {U} [Structure.Arithmetic.Arith U] => { ex := fun x => Structure.Arithmetic.Def.ex }

Complexity: 39 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.S, Structure.Arithmetic.Serial

Inner dependencies: Structure.Arithmetic.instDefS

Used by: Structure.Arithmetic.Exp, Structure.Arithmetic.Plus, Structure.Arithmetic.Times, Structure.Arithmetic.exp_base, Structure.Arithmetic.exp_step, Structure.Arithmetic.plus_base, Structure.Arithmetic.plus_step, Structure.Arithmetic.times_base, Structure.Arithmetic.times_step

ImportantStructure.Arithmetic.instUnivalentS

instance Structure.Arithmetic.instUnivalentS.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] :
  Structure.Arithmetic.Univalent Structure.Arithmetic.S

Show details

fun {U} [Structure.Arithmetic.Arith U] => { uniq := fun x => Structure.Arithmetic.Def.uniq }

Complexity: 39 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.S, Structure.Arithmetic.Univalent

Inner dependencies: Structure.Arithmetic.instDefS

Used by: Structure.Arithmetic.Exp, Structure.Arithmetic.Plus, Structure.Arithmetic.Times, Structure.Arithmetic.exp_base, Structure.Arithmetic.exp_step, Structure.Arithmetic.plus_base, Structure.Arithmetic.plus_step, Structure.Arithmetic.times_base, Structure.Arithmetic.times_step

TipStructure.Arithmetic.exists_S_of_not_Z

Every element other than a zero has a predecessor: among the finitely many elements up to a witness lying strictly below, a greatest one is a predecessor.

theorem Structure.Arithmetic.exists_S_of_not_Z.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] {a : U}
  (ha : ¬Structure.Arithmetic.Z a) : ∃ u, Structure.Arithmetic.S u a

Show details

fun {U} [Structure.Arithmetic.Arith U] {a} ha =>
  Exists.casesOn
    (Eq.mpr (id (congrArg Exists (funext fun y => not_le._simp_1)))
      (Eq.mp
        (Eq.trans Structure.Arithmetic.exists_S_of_not_Z._simp_1_1
          (congrArg Exists (funext fun x => not_le._simp_1)))
        ha))
    fun y hy =>
    Exists.casesOn
      (Set.exists_max_image {x | x < a} id
        (Set.Finite.subset (Structure.Arithmetic.Arith.reach a) fun x hx => le_of_lt hx)
        (Exists.intro y (not_le.mp hy)))
      fun u h =>
      And.casesOn h fun hu hmax =>
        Exists.intro u
          (Or.inl
            ⟨hu, fun z hz =>
              Decidable.byContradiction fun h => absurd (hmax z (not_le.mp h)) (not_le.mpr hz)⟩)

Complexity: 2927 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.S, Structure.Arithmetic.Z

Proof dependencies: Structure.Arithmetic.M

Mathlib dependencies: Set, Set.Finite.subset, Set.Iic, Set.exists_max_image, le_of_lt, not_le, setOf

Lean core dependencies: And, Classical.not_forall, Decidable.byContradiction, Eq, Eq.mp, Eq.mpr, Eq.trans, Exists, False, Not, absurd, congrArg, funext, id

Used by: Structure.Arithmetic.S_pred, Structure.Arithmetic.count_surjective, Structure.Arithmetic.instTotallyPrimitiveOfSerial, Structure.Arithmetic.pred

ImportantStructure.Arithmetic.instTotallyPrimitiveOfSerial

A primitive specification allows at least one value at each place.

instance Structure.Arithmetic.instTotallyPrimitiveOfSerial.{u_1, u_2} {U : Type u_1} {V : Type u_2}
  [Structure.Arithmetic.Arith U] (b : V) (g : V → V → Prop) [Structure.Arithmetic.Serial g] :
  Structure.Arithmetic.Totally (Structure.Arithmetic.Primitive b g)

Show details

fun {U} {V} [Structure.Arithmetic.Arith U] b g [Structure.Arithmetic.Serial g] =>
  {
    ex := fun R ht =>
      {
        ex := fun a =>
          if ha : Structure.Arithmetic.Z a then Exists.intro b (Or.inl ⟨ha, rfl⟩)
          else
            Exists.casesOn (Structure.Arithmetic.exists_S_of_not_Z ha) fun u hu =>
              Exists.casesOn (Structure.Arithmetic.Serial.ex u) fun w hw =>
                Exists.casesOn (Structure.Arithmetic.Serial.ex w) fun v hv =>
                  Exists.intro v (Or.inr ⟨ha, Exists.intro u (Exists.intro w ⟨hu, ⟨hw, hv⟩⟩)⟩) } }

Complexity: 743 (size of the value term)

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

Inner dependencies: Structure.Arithmetic.S, Structure.Arithmetic.Z, Structure.Arithmetic.exists_S_of_not_Z

Lean core dependencies: And, Eq, Exists, Not, dite, rfl

Used by: Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent

TipStructure.Arithmetic.S_unique

An element other than a zero has at most one predecessor.

theorem Structure.Arithmetic.S_unique.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] {a u u' : U}
  (ha : ¬Structure.Arithmetic.Z a) (h : Structure.Arithmetic.S u a)
  (h' : Structure.Arithmetic.S u' a) : u = u'

Show details

fun {U} [Structure.Arithmetic.Arith U] {a u u'} ha h h' =>
  Or.casesOn h
    (fun h =>
      And.casesOn h fun hu hmin =>
        Or.casesOn h'
          (fun h =>
            And.casesOn h fun hu' hmin' =>
              Or.casesOn (lt_trichotomy u u') (fun h => absurd (hmin u' h) (not_le.mpr hu'))
                fun h => Or.casesOn h (fun h => h) fun h => absurd (hmin' u h) (not_le.mpr hu))
          fun h => And.casesOn h fun left hz' => absurd hz' ha)
    fun h => And.casesOn h fun left hz => absurd hz ha

Complexity: 2103 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.S, Structure.Arithmetic.Z

Proof dependencies: Structure.Arithmetic.M

Mathlib dependencies: lt_trichotomy, not_le

Lean core dependencies: And, Eq, Not, Or, absurd

Used by: Structure.Arithmetic.fixedPoint_iter, Structure.Arithmetic.instUnivalentlyPrimitiveOfUnivalent, Structure.Arithmetic.iter_step, Structure.Arithmetic.rec_step

ImportantStructure.Arithmetic.instUnivalentlyPrimitiveOfUnivalent

A primitive specification allows at most one value at each place.

instance Structure.Arithmetic.instUnivalentlyPrimitiveOfUnivalent.{u_1, u_2} {U : Type u_1} {V : Type u_2}
  [Structure.Arithmetic.Arith U] (b : V) (g : V → V → Prop) [Structure.Arithmetic.Univalent g] :
  Structure.Arithmetic.Univalently (Structure.Arithmetic.Primitive b g)

Show details

fun {U} {V} [Structure.Arithmetic.Arith U] b g [Structure.Arithmetic.Univalent g] =>
  {
    uniq := fun R hu =>
      {
        uniq := fun a v w hv hw =>
          Or.casesOn hv
            (fun h =>
              And.casesOn h fun hz right =>
                Eq.ndrec (motive := fun b => Structure.Arithmetic.Primitive b g R a w → v = w)
                  (fun hw =>
                    Or.casesOn hw (fun h => And.casesOn h fun left right => right ▸ Eq.refl w)
                      fun h => And.casesOn h fun ha right => absurd hz ha)
                  right hw)
            fun h =>
            And.casesOn h fun ha right =>
              Exists.casesOn right fun u1 h =>
                Exists.casesOn h fun w1 h =>
                  And.casesOn h fun hu1 right =>
                    And.casesOn right fun hw1 hg1 =>
                      Or.casesOn hw (fun h => And.casesOn h fun hz right => absurd hz ha) fun h =>
                        And.casesOn h fun left right =>
                          Exists.casesOn right fun u2 h =>
                            Exists.casesOn h fun w2 h =>
                              And.casesOn h fun hu2 right =>
                                And.casesOn right fun hw2 hg2 =>
                                  Structure.Arithmetic.Univalent.uniq w2 v w
                                    (Eq.mp
                                      (congrArg (fun _a => g _a v)
                                        (Structure.Arithmetic.Univalent.uniq u2 w1 w2
                                          (Eq.mp
                                            (congrArg (fun _a => R _a w1)
                                              (Structure.Arithmetic.S_unique ha hu1 hu2))
                                            hw1)
                                          hw2))
                                      hg1)
                                    hg2 } }

Complexity: 2241 (size of the value term)

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

Inner dependencies: Structure.Arithmetic.S, Structure.Arithmetic.S_unique, Structure.Arithmetic.Z

Lean core dependencies: And, Eq, Eq.mp, Exists, Not, absurd, congrArg

Used by: Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent

TipStructure.Arithmetic.lt_wf

Being below is well founded: a nonempty collection meets a finite initial segment, whose least element is least in the collection.

theorem Structure.Arithmetic.lt_wf.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] :
  WellFounded fun x1 x2 => x1 < x2

Show details

fun {U} [Structure.Arithmetic.Arith U] =>
  Eq.mpr (id (congrArg (fun _a => _a) (propext WellFounded.wellFounded_iff_has_min))) fun s h =>
    match h with
    | Exists.intro x hx =>
      Exists.casesOn
        (Set.exists_min_image {y | y ∈ s ∧ y ≤ x} id
          (Set.Finite.subset (Structure.Arithmetic.Arith.reach x) fun y hy => hy.right)
          (Exists.intro x ⟨hx, le_rfl⟩))
        fun m h =>
        And.casesOn h fun left hmin =>
          And.casesOn left fun hm hmx =>
            Exists.intro m
              ⟨hm, fun y hy hlt =>
                Or.casesOn (le_total y x) (fun h => absurd (hmin y ⟨hy, h⟩) (not_le.mpr hlt))
                  fun h => absurd hlt (not_lt.mpr (LE.le.trans hmx h))⟩

Complexity: 3647 (size of the value term)

Dependencies: Structure.Arithmetic.Arith

Mathlib dependencies: Set, Set.Finite.subset, Set.Iic, Set.Nonempty, Set.exists_min_image, WellFounded.wellFounded_iff_has_min, le_rfl, le_total, not_le, not_lt, setOf

Lean core dependencies: And, Eq, Eq.mpr, Exists, False, Not, Or, WellFounded, absurd, congrArg, id

Used by: Structure.Arithmetic.count_surjective, Structure.Arithmetic.halts_of_measure, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.iter, Structure.Arithmetic.iter_eq

TipStructure.Arithmetic.S_lt

A predecessor lies below.

theorem Structure.Arithmetic.S_lt.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] {a u : U}
  (ha : ¬Structure.Arithmetic.Z a) (h : Structure.Arithmetic.S u a) : u < a

Show details

fun {U} [Structure.Arithmetic.Arith U] {a u} ha h =>
  Or.casesOn h (fun h => And.casesOn h fun h right => h) fun h =>
    And.casesOn h fun left hz => absurd hz ha

Complexity: 891 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.S, Structure.Arithmetic.Z

Proof dependencies: Structure.Arithmetic.M

Lean core dependencies: And, Not, absurd

Used by: Structure.Arithmetic.count_surjective, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.iter

NoteStructure.Arithmetic.pred

The predecessor of an element other than a zero.

def Structure.Arithmetic.pred.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] {a : U}
  (ha : ¬Structure.Arithmetic.Z a) : U

Show details

| Structure.Arithmetic.pred ha = Classical.choose ⋯

Complexity: 43 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Z

Inner dependencies: Structure.Arithmetic.S, Structure.Arithmetic.exists_S_of_not_Z

Lean core dependencies: Classical.choose, Not

Used by: Structure.Arithmetic.S_pred, Structure.Arithmetic.fixedPoint_iter, Structure.Arithmetic.iter, Structure.Arithmetic.iter_base, Structure.Arithmetic.iter_eq, Structure.Arithmetic.iter_step

TipStructure.Arithmetic.S_pred

theorem Structure.Arithmetic.S_pred.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] {a : U}
  (ha : ¬Structure.Arithmetic.Z a) : Structure.Arithmetic.S (Structure.Arithmetic.pred ha) a

Show details

fun {U} [Structure.Arithmetic.Arith U] {a} ha =>
  Classical.choose_spec (Structure.Arithmetic.exists_S_of_not_Z ha)

Complexity: 43 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.S, Structure.Arithmetic.Z, Structure.Arithmetic.pred

Proof dependencies: Structure.Arithmetic.exists_S_of_not_Z

Lean core dependencies: Classical.choose_spec, Not

Used by: Structure.Arithmetic.fixedPoint_iter, Structure.Arithmetic.iter, Structure.Arithmetic.iter_step

NoteStructure.Arithmetic.step

The \(g\)-successor of a value, where \(g\) gives exactly one value at each place.

def Structure.Arithmetic.step.{u_2} {V : Type u_2} (g : V → V → Prop) [Structure.Arithmetic.Serial g]
  [Structure.Arithmetic.Univalent g] (w : V) : V

Show details

| Structure.Arithmetic.step g w = Structure.Arithmetic.the (g w)

Complexity: 47 (size of the value term)

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

Inner dependencies: Structure.Arithmetic.instDefOfSerialOfUnivalent, Structure.Arithmetic.the

Used by: Structure.Arithmetic.fixedPoint_iter, Structure.Arithmetic.iter, Structure.Arithmetic.iter_base, Structure.Arithmetic.iter_eq, Structure.Arithmetic.iter_step, Structure.Arithmetic.step_spec

TipStructure.Arithmetic.step_spec

theorem Structure.Arithmetic.step_spec.{u_2} {V : Type u_2} (g : V → V → Prop)
  [Structure.Arithmetic.Serial g] [Structure.Arithmetic.Univalent g] (w : V) :
  g w (Structure.Arithmetic.step g w)

Show details

fun {V} g [Structure.Arithmetic.Serial g] [Structure.Arithmetic.Univalent g] w =>
  Structure.Arithmetic.the_spec (g w)

Complexity: 47 (size of the value term)

Dependencies: Structure.Arithmetic.Serial, Structure.Arithmetic.Univalent, Structure.Arithmetic.step

Proof dependencies: Structure.Arithmetic.instDefOfSerialOfUnivalent, Structure.Arithmetic.the_spec

Used by: Structure.Arithmetic.fixedPoint_iter

NoteStructure.Arithmetic.iter

The value of a primitive specification, computed by descending along predecessors.

def Structure.Arithmetic.iter.{u_1, u_2} {U : Type u_1} {V : Type u_2} [Structure.Arithmetic.Arith U]
  (b : V) (g : V → V → Prop) [Structure.Arithmetic.Serial g] [Structure.Arithmetic.Univalent g] :
  U → V

Show details

| Structure.Arithmetic.iter b g =
  ⋯.fix fun a ih =>
    if ha : Structure.Arithmetic.Z a then b
    else Structure.Arithmetic.step g (ih (Structure.Arithmetic.pred ha) ⋯)

Complexity: 205 (size of the value term)

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

Inner dependencies: Structure.Arithmetic.S_lt, Structure.Arithmetic.S_pred, Structure.Arithmetic.Z, Structure.Arithmetic.lt_wf, Structure.Arithmetic.pred, Structure.Arithmetic.step

Lean core dependencies: Not, WellFounded.fix, dite

Used by: Structure.Arithmetic.fixedPoint_iter, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.instSerialRecPrimitive, Structure.Arithmetic.instUnivalentRecPrimitive, Structure.Arithmetic.iter_base, Structure.Arithmetic.iter_eq, Structure.Arithmetic.iter_step, Structure.Arithmetic.rec_primitive

TipStructure.Arithmetic.iter_eq

theorem Structure.Arithmetic.iter_eq.{u_1, u_2} {U : Type u_1} {V : Type u_2} [Structure.Arithmetic.Arith U]
  (b : V) (g : V → V → Prop) [Structure.Arithmetic.Serial g] [Structure.Arithmetic.Univalent g]
  (a : U) :
  Structure.Arithmetic.iter b g a =
    if ha : Structure.Arithmetic.Z a then b
    else Structure.Arithmetic.step g (Structure.Arithmetic.iter b g (Structure.Arithmetic.pred ha))

Show details

fun {U} {V} [Structure.Arithmetic.Arith U] b g [Structure.Arithmetic.Serial g]
    [Structure.Arithmetic.Univalent g] a =>
  WellFounded.fix_eq Structure.Arithmetic.lt_wf
    (fun a ih =>
      if ha : Structure.Arithmetic.Z a then b
      else
        Structure.Arithmetic.step g
          (ih (Structure.Arithmetic.pred ha) (Structure.Arithmetic.iter._proof_1 a ha)))
    a

Complexity: 209 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Serial, Structure.Arithmetic.Univalent, Structure.Arithmetic.Z, Structure.Arithmetic.iter, Structure.Arithmetic.pred, Structure.Arithmetic.step

Proof dependencies: Structure.Arithmetic.lt_wf

Lean core dependencies: Eq, Not, WellFounded.fix_eq, dite

Used by: Structure.Arithmetic.iter_base, Structure.Arithmetic.iter_step

TipStructure.Arithmetic.iter_base

At a zero the value is the base.

theorem Structure.Arithmetic.iter_base.{u_1, u_2} {U : Type u_1} {V : Type u_2}
  [Structure.Arithmetic.Arith U] (b : V) (g : V → V → Prop) [Structure.Arithmetic.Serial g]
  [Structure.Arithmetic.Univalent g] {a : U} (ha : Structure.Arithmetic.Z a) :
  Structure.Arithmetic.iter b g a = b

Show details

fun {U} {V} [Structure.Arithmetic.Arith U] b g [Structure.Arithmetic.Serial g]
    [Structure.Arithmetic.Univalent g] {a} ha =>
  Eq.mpr (id (congrArg (fun _a => _a = b) (Structure.Arithmetic.iter_eq b g a)))
    (Eq.mpr (id (congrArg (fun _a => _a = b) (dif_pos ha))) (Eq.refl b))

Complexity: 769 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Serial, Structure.Arithmetic.Univalent, Structure.Arithmetic.Z, Structure.Arithmetic.iter

Proof dependencies: Structure.Arithmetic.iter_eq, Structure.Arithmetic.pred, Structure.Arithmetic.step

Lean core dependencies: Eq, Eq.mpr, Not, congrArg, dif_pos, dite, id

Used by: Structure.Arithmetic.fixedPoint_iter

TipStructure.Arithmetic.iter_step

Elsewhere the value is the \(g\)-successor of the value at the predecessor.

theorem Structure.Arithmetic.iter_step.{u_1, u_2} {U : Type u_1} {V : Type u_2}
  [Structure.Arithmetic.Arith U] (b : V) (g : V → V → Prop) [Structure.Arithmetic.Serial g]
  [Structure.Arithmetic.Univalent g] {a u : U} (ha : ¬Structure.Arithmetic.Z a)
  (h : Structure.Arithmetic.S u a) :
  Structure.Arithmetic.iter b g a = Structure.Arithmetic.step g (Structure.Arithmetic.iter b g u)

Show details

fun {U} {V} [Structure.Arithmetic.Arith U] b g [Structure.Arithmetic.Serial g]
    [Structure.Arithmetic.Univalent g] {a u} ha h =>
  Eq.mpr
    (id
      (congrArg (fun _a => _a = Structure.Arithmetic.step g (Structure.Arithmetic.iter b g u))
        (Structure.Arithmetic.iter_eq b g a)))
    (Eq.mpr
      (id
        (congrArg (fun _a => _a = Structure.Arithmetic.step g (Structure.Arithmetic.iter b g u))
          (dif_neg ha)))
      (Eq.mpr
        (id
          (congrArg
            (fun _a =>
              Structure.Arithmetic.step g (Structure.Arithmetic.iter b g _a) =
                Structure.Arithmetic.step g (Structure.Arithmetic.iter b g u))
            (Structure.Arithmetic.S_unique ha (Structure.Arithmetic.S_pred ha) h)))
        (Eq.refl (Structure.Arithmetic.step g (Structure.Arithmetic.iter b g u)))))

Complexity: 1549 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.S, Structure.Arithmetic.Serial, Structure.Arithmetic.Univalent, Structure.Arithmetic.Z, Structure.Arithmetic.iter, Structure.Arithmetic.step

Proof dependencies: Structure.Arithmetic.S_pred, Structure.Arithmetic.S_unique, Structure.Arithmetic.iter_eq, Structure.Arithmetic.pred

Lean core dependencies: Eq, Eq.mpr, Not, congrArg, dif_neg, dite, id

Used by: Structure.Arithmetic.fixedPoint_iter

TipStructure.Arithmetic.fixedPoint_iter

Reading iter as a relation answers the primitive specification.

theorem Structure.Arithmetic.fixedPoint_iter.{u_1, u_2} {U : Type u_1} {V : Type u_2}
  [Structure.Arithmetic.Arith U] (b : V) (g : V → V → Prop) [Structure.Arithmetic.Serial g]
  [Structure.Arithmetic.Univalent g] :
  Structure.Arithmetic.FixedPoint (Structure.Arithmetic.Primitive b g) fun a v =>
    v = Structure.Arithmetic.iter b g a

Show details

fun {U} {V} [Structure.Arithmetic.Arith U] b g [Structure.Arithmetic.Serial g]
    [Structure.Arithmetic.Univalent g] =>
  {
    self :=
      funext fun a =>
        funext fun v =>
          propext
            (if ha : Structure.Arithmetic.Z a then
              Eq.mpr
                (id
                  (congrArg
                    (fun _a =>
                      Structure.Arithmetic.Primitive b g
                          (fun a v => v = Structure.Arithmetic.iter b g a) a v ↔
                        v = _a)
                    (Structure.Arithmetic.iter_base b g ha)))
                {
                  mp := fun a_1 =>
                    Or.casesOn a_1 (fun h => And.casesOn h fun left right => right ▸ Eq.refl v)
                      fun h => And.casesOn h fun ha' right => absurd ha ha',
                  mpr := fun a_1 => a_1 ▸ Or.inl ⟨ha, rfl⟩ }
            else
              Eq.mpr
                (id
                  (congrArg
                    (fun _a =>
                      Structure.Arithmetic.Primitive b g
                          (fun a v => v = Structure.Arithmetic.iter b g a) a v ↔
                        v = _a)
                    (Structure.Arithmetic.iter_step b g ha (Structure.Arithmetic.S_pred ha))))
                {
                  mp := fun a_1 =>
                    Or.casesOn a_1 (fun h => And.casesOn h fun hz right => absurd hz ha) fun h =>
                      And.casesOn h fun left right =>
                        Exists.casesOn right fun u h =>
                          Exists.casesOn h fun w h =>
                            And.casesOn h fun hu right =>
                              And.casesOn right fun left hg =>
                                Eq.ndrec (motive := fun w =>
                                  g w v →
                                    v =
                                      Structure.Arithmetic.step g
                                        (Structure.Arithmetic.iter b g
                                          (Structure.Arithmetic.pred ha)))
                                  (fun hg =>
                                    Structure.Arithmetic.eq_the
                                      (Eq.mp
                                        (congrArg (fun _a => g (Structure.Arithmetic.iter b g _a) v)
                                          (Structure.Arithmetic.S_unique ha hu
                                            (Structure.Arithmetic.S_pred ha)))
                                        hg))
                                  (Eq.symm left) hg,
                  mpr := fun a_1 =>
                    Eq.symm a_1 ▸
                      Or.inr
                        ⟨ha,
                          Exists.intro (Structure.Arithmetic.pred ha)
                            (Exists.intro
                              (Structure.Arithmetic.iter b g (Structure.Arithmetic.pred ha))
                              ⟨Structure.Arithmetic.S_pred ha,
                                ⟨rfl,
                                  Structure.Arithmetic.step_spec g
                                    (Structure.Arithmetic.iter b g
                                      (Structure.Arithmetic.pred ha))⟩⟩)⟩ }) }

Complexity: 5131 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.FixedPoint, Structure.Arithmetic.Primitive, Structure.Arithmetic.Serial, Structure.Arithmetic.Univalent, Structure.Arithmetic.iter

Proof dependencies: Structure.Arithmetic.S, Structure.Arithmetic.S_pred, Structure.Arithmetic.S_unique, Structure.Arithmetic.Z, Structure.Arithmetic.eq_the, Structure.Arithmetic.instDefOfSerialOfUnivalent, Structure.Arithmetic.iter_base, Structure.Arithmetic.iter_step, Structure.Arithmetic.pred, Structure.Arithmetic.step, Structure.Arithmetic.step_spec

Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.symm, Exists, Iff, Not, absurd, congrArg, dite, funext, id, rfl

Used by: Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.rec_primitive

ImportantStructure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent

A primitive specification defines a relation: iter answers it, and any two answers agree by induction along the descent to a zero.

instance Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent.{u_1, u_2}
  {U : Type u_1} {V : Type u_2} [Structure.Arithmetic.Arith U] (b : V) (g : V → V → Prop)
  [Structure.Arithmetic.Serial g] [Structure.Arithmetic.Univalent g] :
  Structure.Arithmetic.Def (Structure.Arithmetic.FixedPoint (Structure.Arithmetic.Primitive b g))

Show details

fun {U} {V} [Structure.Arithmetic.Arith U] b g [Structure.Arithmetic.Serial g]
    [Structure.Arithmetic.Univalent g] =>
  {
    ex :=
      Exists.intro (fun a v => v = Structure.Arithmetic.iter b g a)
        (Structure.Arithmetic.fixedPoint_iter b g),
    uniq := fun R R' hR hR' =>
      have key := fun a =>
        WellFounded.induction Structure.Arithmetic.lt_wf a fun a ih v =>
          Eq.mpr
            (id
              (congrArg (fun _a => _a a v ↔ R' a v) (Eq.symm Structure.Arithmetic.FixedPoint.self)))
            (Eq.mpr
              (id
                (congrArg (fun _a => Structure.Arithmetic.Primitive b g R a v ↔ _a a v)
                  (Eq.symm Structure.Arithmetic.FixedPoint.self)))
              (if ha : Structure.Arithmetic.Z a then
                of_eq_true
                  (Eq.trans
                    (congr
                      (congrArg Iff
                        (Eq.trans
                          (congr
                            (congrArg Or
                              (Eq.trans (congrFun' (congrArg And (eq_true ha)) (v = b))
                                (true_and (v = b))))
                            (Eq.trans
                              (congr
                                (congrArg And
                                  (Eq.trans (congrArg Not (eq_true ha)) not_true_eq_false))
                                (congrArg Exists (funext fun u => exists_and_left._simp_1)))
                              (false_and (∃ u, Structure.Arithmetic.S u a ∧ ∃ x, R u x ∧ g x v))))
                          (or_false (v = b))))
                      (Eq.trans
                        (congr
                          (congrArg Or
                            (Eq.trans (congrFun' (congrArg And (eq_true ha)) (v = b))
                              (true_and (v = b))))
                          (Eq.trans
                            (congr
                              (congrArg And
                                (Eq.trans (congrArg Not (eq_true ha)) not_true_eq_false))
                              (congrArg Exists (funext fun u => exists_and_left._simp_1)))
                            (false_and (∃ u, Structure.Arithmetic.S u a ∧ ∃ x, R' u x ∧ g x v))))
                        (or_false (v = b))))
                    (iff_self (v = b)))
              else
                Eq.mpr
                  (id
                    (congr
                      (congrArg Iff
                        (Eq.trans
                          (congr
                            (congrArg Or
                              (Eq.trans (congrFun' (congrArg And (eq_false ha)) (v = b))
                                (false_and (v = b))))
                            (Eq.trans
                              (congrFun'
                                (congrArg And
                                  (Eq.trans (congrArg Not (eq_false ha))
                                    Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent._simp_2))
                                (∃ u w, Structure.Arithmetic.S u a ∧ R u w ∧ g w v))
                              (true_and (∃ u w, Structure.Arithmetic.S u a ∧ R u w ∧ g w v))))
                          (false_or (∃ u w, Structure.Arithmetic.S u a ∧ R u w ∧ g w v))))
                      (Eq.trans
                        (congr
                          (congrArg Or
                            (Eq.trans (congrFun' (congrArg And (eq_false ha)) (v = b))
                              (false_and (v = b))))
                          (Eq.trans
                            (congrFun'
                              (congrArg And
                                (Eq.trans (congrArg Not (eq_false ha))
                                  Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent._simp_2))
                              (∃ u w, Structure.Arithmetic.S u a ∧ R' u w ∧ g w v))
                            (true_and (∃ u w, Structure.Arithmetic.S u a ∧ R' u w ∧ g w v))))
                        (false_or (∃ u w, Structure.Arithmetic.S u a ∧ R' u w ∧ g w v)))))
                  {
                    mp := fun a_1 =>
                      Exists.casesOn a_1 fun u h =>
                        Exists.casesOn h fun w h =>
                          And.casesOn h fun hu right =>
                            And.casesOn right fun hw hg =>
                              Exists.intro u
                                (Exists.intro w
                                  ⟨hu, ⟨(ih u (Structure.Arithmetic.S_lt ha hu) w).mp hw, hg⟩⟩),
                    mpr := fun a_1 =>
                      Exists.casesOn a_1 fun u h =>
                        Exists.casesOn h fun w h =>
                          And.casesOn h fun hu right =>
                            And.casesOn right fun hw hg =>
                              Exists.intro u
                                (Exists.intro w
                                  ⟨hu,
                                    ⟨(ih u (Structure.Arithmetic.S_lt ha hu) w).mpr hw, hg⟩⟩) }));
      funext fun a => funext fun v => propext (key a v) }

Complexity: 6132 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Def, Structure.Arithmetic.FixedPoint, Structure.Arithmetic.Primitive, Structure.Arithmetic.Serial, Structure.Arithmetic.Univalent

Inner dependencies: Structure.Arithmetic.S, Structure.Arithmetic.S_lt, Structure.Arithmetic.Z, Structure.Arithmetic.fixedPoint_iter, Structure.Arithmetic.iter, Structure.Arithmetic.lt_wf

Lean core dependencies: And, Eq, Eq.mpr, Eq.symm, Eq.trans, Exists, False, Iff, Not, Or, True, WellFounded.induction, congr, congrArg, congrFun', dite, eq_false, eq_true, false_and, false_or, funext, id, iff_self, not_false_iff, not_true_eq_false, of_eq_true, or_false, true_and

Used by: Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent, Structure.Arithmetic.rec_primitive

ImportantStructure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent

Every primitive specification is a recursive definition.

instance Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent.{u_1, u_2} {U : Type u_1}
  {V : Type u_2} [Structure.Arithmetic.Arith U] (b : V) (g : V → V → Prop)
  [Structure.Arithmetic.Serial g] [Structure.Arithmetic.Univalent g] :
  Structure.Arithmetic.PrimitiveRecursive b g

Show details

fun {U} {V} [Structure.Arithmetic.Arith U] b g [Structure.Arithmetic.Serial g]
    [Structure.Arithmetic.Univalent g] =>
  { toTotally := Structure.Arithmetic.instTotallyPrimitiveOfSerial b g,
    toUnivalently := Structure.Arithmetic.instUnivalentlyPrimitiveOfUnivalent b g,
    defines := inferInstance }

Complexity: 121 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.PrimitiveRecursive, Structure.Arithmetic.Serial, Structure.Arithmetic.Univalent

Inner dependencies: Structure.Arithmetic.Def, Structure.Arithmetic.FixedPoint, Structure.Arithmetic.Primitive, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.instTotallyPrimitiveOfSerial, Structure.Arithmetic.instUnivalentlyPrimitiveOfUnivalent

Lean core dependencies: inferInstance

Used by: Structure.Arithmetic.Exp, Structure.Arithmetic.Plus, Structure.Arithmetic.Times, Structure.Arithmetic.instSerialRecPrimitive, Structure.Arithmetic.instUnivalentRecPrimitive, Structure.Arithmetic.rec_base, Structure.Arithmetic.rec_primitive, Structure.Arithmetic.rec_step

TipStructure.Arithmetic.rec_primitive

What a primitive specification denotes is iter, read as a relation.

theorem Structure.Arithmetic.rec_primitive.{u_1, u_2} {U : Type u_1} {V : Type u_2}
  [Structure.Arithmetic.Arith U] (b : V) (g : V → V → Prop) [Structure.Arithmetic.Serial g]
  [Structure.Arithmetic.Univalent g] :
  Structure.Arithmetic.rec (Structure.Arithmetic.Primitive b g) = fun a v =>
    v = Structure.Arithmetic.iter b g a

Show details

fun {U} {V} [Structure.Arithmetic.Arith U] b g [Structure.Arithmetic.Serial g]
    [Structure.Arithmetic.Univalent g] =>
  Eq.symm (Structure.Arithmetic.eq_the (Structure.Arithmetic.fixedPoint_iter b g))

Complexity: 195 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Primitive, Structure.Arithmetic.Serial, Structure.Arithmetic.Univalent, Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent, Structure.Arithmetic.iter, Structure.Arithmetic.rec

Proof dependencies: Structure.Arithmetic.FixedPoint, Structure.Arithmetic.eq_the, Structure.Arithmetic.fixedPoint_iter, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.the

Lean core dependencies: Eq, Eq.symm

Used by: Structure.Arithmetic.instSerialRecPrimitive, Structure.Arithmetic.instUnivalentRecPrimitive

ImportantStructure.Arithmetic.instSerialRecPrimitive

instance Structure.Arithmetic.instSerialRecPrimitive.{u_1, u_2} {U : Type u_1} {V : Type u_2}
  [Structure.Arithmetic.Arith U] (b : V) (g : V → V → Prop) [Structure.Arithmetic.Serial g]
  [Structure.Arithmetic.Univalent g] :
  Structure.Arithmetic.Serial (Structure.Arithmetic.rec (Structure.Arithmetic.Primitive b g))

Show details

fun {U} {V} [Structure.Arithmetic.Arith U] b g [Structure.Arithmetic.Serial g]
    [Structure.Arithmetic.Univalent g] =>
  Eq.mpr
    (id
      (congrArg (fun _a => Structure.Arithmetic.Serial _a)
        (Structure.Arithmetic.rec_primitive b g)))
    { ex := fun a => Exists.intro (Structure.Arithmetic.iter b g a) rfl }

Complexity: 395 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Primitive, Structure.Arithmetic.Serial, Structure.Arithmetic.Univalent, Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent, Structure.Arithmetic.rec

Inner dependencies: Structure.Arithmetic.iter, Structure.Arithmetic.rec_primitive

Lean core dependencies: Eq, Eq.mpr, congrArg, id, rfl

Used by: Structure.Arithmetic.Exp, Structure.Arithmetic.Times, Structure.Arithmetic.exp_base, Structure.Arithmetic.exp_step, Structure.Arithmetic.times_base, Structure.Arithmetic.times_step

ImportantStructure.Arithmetic.instUnivalentRecPrimitive

instance Structure.Arithmetic.instUnivalentRecPrimitive.{u_1, u_2} {U : Type u_1} {V : Type u_2}
  [Structure.Arithmetic.Arith U] (b : V) (g : V → V → Prop) [Structure.Arithmetic.Serial g]
  [Structure.Arithmetic.Univalent g] :
  Structure.Arithmetic.Univalent (Structure.Arithmetic.rec (Structure.Arithmetic.Primitive b g))

Show details

fun {U} {V} [Structure.Arithmetic.Arith U] b g [Structure.Arithmetic.Serial g]
    [Structure.Arithmetic.Univalent g] =>
  Eq.mpr
    (id
      (congrArg (fun _a => Structure.Arithmetic.Univalent _a)
        (Structure.Arithmetic.rec_primitive b g)))
    { uniq := fun x x_1 x_2 hv hw => Eq.trans hv (Eq.symm hw) }

Complexity: 431 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Primitive, Structure.Arithmetic.Serial, Structure.Arithmetic.Univalent, Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent, Structure.Arithmetic.rec

Inner dependencies: Structure.Arithmetic.iter, Structure.Arithmetic.rec_primitive

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

Used by: Structure.Arithmetic.Exp, Structure.Arithmetic.Times, Structure.Arithmetic.exp_base, Structure.Arithmetic.exp_step, Structure.Arithmetic.times_base, Structure.Arithmetic.times_step

ImportantStructure.Arithmetic.rec_base

At a zero the denotation gives the base.

theorem Structure.Arithmetic.rec_base.{u_1, u_2} {U : Type u_1} {V : Type u_2}
  [Structure.Arithmetic.Arith U] (b : V) (g : V → V → Prop) [Structure.Arithmetic.Serial g]
  [Structure.Arithmetic.Univalent g] {a : U} {v : V} (ha : Structure.Arithmetic.Z a) :
  Structure.Arithmetic.rec (Structure.Arithmetic.Primitive b g) a v ↔ v = b

Show details

fun {U} {V} [Structure.Arithmetic.Arith U] b g [Structure.Arithmetic.Serial g]
    [Structure.Arithmetic.Univalent g] {a} {v} ha =>
  Eq.mpr
    (id
      (congrArg (fun _a => _a ↔ v = b)
        (Eq.symm
          (congrFun
            (congrFun (Structure.Arithmetic.rec_spec (Structure.Arithmetic.Primitive b g)) a) v))))
    (of_eq_true
      (Eq.trans
        (congrFun'
          (congrArg Iff
            (Eq.trans
              (congr
                (congrArg Or
                  (Eq.trans (congrFun' (congrArg And (eq_true ha)) (v = b)) (true_and (v = b))))
                (Eq.trans
                  (congr (congrArg And (Eq.trans (congrArg Not (eq_true ha)) not_true_eq_false))
                    (congrArg Exists (funext fun u => exists_and_left._simp_1)))
                  (false_and
                    (∃ u,
                      Structure.Arithmetic.S u a ∧
                        ∃ x,
                          Structure.Arithmetic.rec (Structure.Arithmetic.Primitive b g) u x ∧
                            g x v))))
              (or_false (v = b))))
          (v = b))
        (iff_self (v = b))))

Complexity: 2209 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Primitive, Structure.Arithmetic.Serial, Structure.Arithmetic.Univalent, Structure.Arithmetic.Z, Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent, Structure.Arithmetic.rec

Proof dependencies: Structure.Arithmetic.S, Structure.Arithmetic.rec_spec

Lean core dependencies: And, Eq, Eq.mpr, Eq.symm, Eq.trans, Exists, False, Iff, Not, Or, True, congr, congrArg, congrFun, congrFun', eq_true, false_and, funext, id, iff_self, not_true_eq_false, of_eq_true, or_false, true_and

Used by: Structure.Arithmetic.exp_base, Structure.Arithmetic.plus_base, Structure.Arithmetic.times_base

ImportantStructure.Arithmetic.rec_step

Elsewhere it gives a \(g\)-successor of the value at the predecessor.

theorem Structure.Arithmetic.rec_step.{u_1, u_2} {U : Type u_1} {V : Type u_2}
  [Structure.Arithmetic.Arith U] (b : V) (g : V → V → Prop) [Structure.Arithmetic.Serial g]
  [Structure.Arithmetic.Univalent g] {a u : U} {v : V} (ha : ¬Structure.Arithmetic.Z a)
  (hu : Structure.Arithmetic.S u a) :
  Structure.Arithmetic.rec (Structure.Arithmetic.Primitive b g) a v ↔
    ∃ w, Structure.Arithmetic.rec (Structure.Arithmetic.Primitive b g) u w ∧ g w v

Show details

fun {U} {V} [Structure.Arithmetic.Arith U] b g [Structure.Arithmetic.Serial g]
    [Structure.Arithmetic.Univalent g] {a u} {v} ha hu =>
  Eq.mpr
    (id
      (congrArg
        (fun _a =>
          _a ↔ ∃ w, Structure.Arithmetic.rec (Structure.Arithmetic.Primitive b g) u w ∧ g w v)
        (Eq.symm
          (congrFun
            (congrFun (Structure.Arithmetic.rec_spec (Structure.Arithmetic.Primitive b g)) a) v))))
    (Eq.mpr
      (id
        (congrFun'
          (congrArg Iff
            (Eq.trans
              (congr
                (congrArg Or
                  (Eq.trans (congrFun' (congrArg And (eq_false ha)) (v = b)) (false_and (v = b))))
                (Eq.trans
                  (congrFun'
                    (congrArg And
                      (Eq.trans (congrArg Not (eq_false ha))
                        Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent._simp_2))
                    (∃ u w,
                      Structure.Arithmetic.S u a ∧
                        Structure.Arithmetic.rec (Structure.Arithmetic.Primitive b g) u w ∧ g w v))
                  (true_and
                    (∃ u w,
                      Structure.Arithmetic.S u a ∧
                        Structure.Arithmetic.rec (Structure.Arithmetic.Primitive b g) u w ∧
                          g w v))))
              (false_or
                (∃ u w,
                  Structure.Arithmetic.S u a ∧
                    Structure.Arithmetic.rec (Structure.Arithmetic.Primitive b g) u w ∧ g w v))))
          (∃ w, Structure.Arithmetic.rec (Structure.Arithmetic.Primitive b g) u w ∧ g w v)))
      {
        mp := fun a_1 =>
          Exists.casesOn a_1 fun u' h =>
            Exists.casesOn h fun w h =>
              And.casesOn h fun hu' right =>
                And.casesOn right fun hw hg =>
                  Exists.intro w
                    ⟨Eq.mp
                        (congrArg
                          (fun _a =>
                            Structure.Arithmetic.rec (Structure.Arithmetic.Primitive b g) _a w)
                          (Structure.Arithmetic.S_unique ha hu' hu))
                        hw,
                      hg⟩,
        mpr := fun a_1 =>
          Exists.casesOn a_1 fun w h =>
            And.casesOn h fun hw hg => Exists.intro u (Exists.intro w ⟨hu, ⟨hw, hg⟩⟩) })

Complexity: 4899 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Primitive, Structure.Arithmetic.S, Structure.Arithmetic.Serial, Structure.Arithmetic.Univalent, Structure.Arithmetic.Z, Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent, Structure.Arithmetic.rec

Proof dependencies: Structure.Arithmetic.S_unique, Structure.Arithmetic.rec_spec

Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Exists, False, Iff, Not, Or, True, congr, congrArg, congrFun, congrFun', eq_false, false_and, false_or, id, true_and

Used by: Structure.Arithmetic.exp_step, Structure.Arithmetic.plus_step, Structure.Arithmetic.times_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.

definitionabbreviationlemmatheoremdeclared elsewheredependencyproof dependency

legend