Documentation

Mathlib.Computability.Primrec

The primitive recursive functions #

The primitive recursive functions are the least collection of functions ℕ → ℕ which are closed under projections (using the pair pairing function), composition, zero, successor, and primitive recursion (i.e. Nat.rec where the motive is C n := ℕ).

We can extend this definition to a large class of basic types by using canonical encodings of types as natural numbers (Gödel numbering), which we implement through the type class Encodable. (More precisely, we need that the composition of encode with decode yields a primitive recursive function, so we have the Primcodable type class for this.)

References #

@[reducible]
def Nat.unpaired {α : Sort u_1} (f : α) (n : ) :
α

Calls the given function on a pair of entries n, encoded via the pairing function.

Equations
Instances For
    inductive Nat.Primrec :
    ()Prop

    The primitive recursive functions ℕ → ℕ.

    Instances For
      theorem Nat.Primrec.of_eq {f : } {g : } (hf : Nat.Primrec f) (H : ∀ (n : ), f n = g n) :
      theorem Nat.Primrec.const (n : ) :
      Nat.Primrec fun (x : ) => n
      theorem Nat.Primrec.prec1 {f : } (m : ) (hf : Nat.Primrec f) :
      Nat.Primrec fun (n : ) => Nat.rec m (fun (y IH : ) => f (Nat.pair y IH)) n
      theorem Nat.Primrec.casesOn1 {f : } (m : ) (hf : Nat.Primrec f) :
      Nat.Primrec fun (x : ) => Nat.casesOn x m f
      theorem Nat.Primrec.casesOn' {f : } {g : } (hf : Nat.Primrec f) (hg : Nat.Primrec g) :
      Nat.Primrec (Nat.unpaired fun (z n : ) => Nat.casesOn n (f z) fun (y : ) => g (Nat.pair z y))
      theorem Nat.Primrec.add :
      Nat.Primrec (Nat.unpaired fun (x x_1 : ) => x + x_1)
      theorem Nat.Primrec.sub :
      Nat.Primrec (Nat.unpaired fun (x x_1 : ) => x - x_1)
      theorem Nat.Primrec.mul :
      Nat.Primrec (Nat.unpaired fun (x x_1 : ) => x * x_1)
      theorem Nat.Primrec.pow :
      Nat.Primrec (Nat.unpaired fun (x x_1 : ) => x ^ x_1)
      class Primcodable (α : Type u_1) extends Encodable :
      Type u_1

      A Primcodable type is an Encodable type for which the encode/decode functions are primitive recursive.

      Instances
        @[instance 10]
        Equations
        def Primcodable.ofEquiv (α : Type u_1) {β : Type u_2} [Primcodable α] (e : β α) :

        Builds a Primcodable instance from an equivalence to a Primcodable type.

        Equations
        Instances For
          instance Primcodable.option {α : Type u_1} [h : Primcodable α] :
          Equations
          def Primrec {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] (f : αβ) :

          Primrec f means f is primitive recursive (after encoding its input and output as natural numbers).

          Equations
          Instances For
            theorem Primrec.encode {α : Type u_1} [Primcodable α] :
            Primrec Encodable.encode
            theorem Primrec.decode {α : Type u_1} [Primcodable α] :
            Primrec Encodable.decode
            theorem Primrec.dom_denumerable {α : Type u_4} {β : Type u_5} [Denumerable α] [Primcodable β] {f : αβ} :
            theorem Primrec.option_some {α : Type u_1} [Primcodable α] :
            Primrec some
            theorem Primrec.of_eq {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {f : ασ} {g : ασ} (hf : Primrec f) (H : ∀ (n : α), f n = g n) :
            theorem Primrec.const {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] (x : σ) :
            Primrec fun (x_1 : α) => x
            theorem Primrec.id {α : Type u_1} [Primcodable α] :
            theorem Primrec.comp {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : βσ} {g : αβ} (hf : Primrec f) (hg : Primrec g) :
            Primrec fun (a : α) => f (g a)
            theorem Primrec.encode_iff {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {f : ασ} :
            (Primrec fun (a : α) => Encodable.encode (f a)) Primrec f
            theorem Primrec.ofNat_iff {α : Type u_4} {β : Type u_5} [Denumerable α] [Primcodable β] {f : αβ} :
            Primrec f Primrec fun (n : ) => f (Denumerable.ofNat α n)
            theorem Primrec.option_some_iff {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {f : ασ} :
            (Primrec fun (a : α) => some (f a)) Primrec f
            theorem Primrec.of_equiv {α : Type u_1} [Primcodable α] {β : Type u_4} {e : β α} :
            Primrec e
            theorem Primrec.of_equiv_symm {α : Type u_1} [Primcodable α] {β : Type u_4} {e : β α} :
            Primrec e.symm
            theorem Primrec.of_equiv_iff {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {β : Type u_4} (e : β α) {f : σβ} :
            (Primrec fun (a : σ) => e (f a)) Primrec f
            theorem Primrec.of_equiv_symm_iff {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {β : Type u_4} (e : β α) {f : σα} :
            (Primrec fun (a : σ) => e.symm (f a)) Primrec f
            instance Primcodable.prod {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] :
            Primcodable (α × β)
            Equations
            theorem Primrec.fst {α : Type u_3} {β : Type u_4} [Primcodable α] [Primcodable β] :
            Primrec Prod.fst
            theorem Primrec.snd {α : Type u_3} {β : Type u_4} [Primcodable α] [Primcodable β] :
            Primrec Prod.snd
            theorem Primrec.pair {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] {f : αβ} {g : αγ} (hf : Primrec f) (hg : Primrec g) :
            Primrec fun (a : α) => (f a, g a)
            theorem Primrec.list_get?₁ {α : Type u_1} [Primcodable α] (l : List α) :
            Primrec l.get?
            def Primrec₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] (f : αβσ) :

            Primrec₂ f means f is a binary primitive recursive function. This is technically unnecessary since we can always curry all the arguments together, but there are enough natural two-arg functions that it is convenient to express this directly.

            Equations
            Instances For
              def PrimrecPred {α : Type u_1} [Primcodable α] (p : αProp) [DecidablePred p] :

              PrimrecPred p means p : α → Prop is a (decidable) primitive recursive predicate, which is to say that decide ∘ p : α → Bool is primitive recursive.

              Equations
              Instances For
                def PrimrecRel {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] (s : αβProp) [(a : α) → (b : β) → Decidable (s a b)] :

                PrimrecRel p means p : α → β → Prop is a (decidable) primitive recursive relation, which is to say that decide ∘ p : α → β → Bool is primitive recursive.

                Equations
                Instances For
                  theorem Primrec₂.mk {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αβσ} (hf : Primrec fun (p : α × β) => f p.1 p.2) :
                  theorem Primrec₂.of_eq {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αβσ} {g : αβσ} (hg : Primrec₂ f) (H : ∀ (a : α) (b : β), f a b = g a b) :
                  theorem Primrec₂.const {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] (x : σ) :
                  Primrec₂ fun (x_1 : α) (x_2 : β) => x
                  theorem Primrec₂.pair {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] :
                  Primrec₂ Prod.mk
                  theorem Primrec₂.left {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] :
                  Primrec₂ fun (a : α) (x : β) => a
                  theorem Primrec₂.right {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] :
                  Primrec₂ fun (x : α) (b : β) => b
                  theorem Primrec₂.unpaired {α : Type u_1} [Primcodable α] {f : α} :
                  theorem Primrec₂.encode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αβσ} :
                  (Primrec₂ fun (a : α) (b : β) => Encodable.encode (f a b)) Primrec₂ f
                  theorem Primrec₂.option_some_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αβσ} :
                  (Primrec₂ fun (a : α) (b : β) => some (f a b)) Primrec₂ f
                  theorem Primrec₂.ofNat_iff {α : Type u_4} {β : Type u_5} {σ : Type u_6} [Denumerable α] [Denumerable β] [Primcodable σ] {f : αβσ} :
                  theorem Primrec₂.uncurry {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αβσ} :
                  theorem Primrec₂.curry {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α × βσ} :
                  theorem Primrec.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : γσ} {g : αβγ} (hf : Primrec f) (hg : Primrec₂ g) :
                  Primrec₂ fun (a : α) (b : β) => f (g a b)
                  theorem Primrec₂.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : βγσ} {g : αβ} {h : αγ} (hf : Primrec₂ f) (hg : Primrec g) (hh : Primrec h) :
                  Primrec fun (a : α) => f (g a) (h a)
                  theorem Primrec₂.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable δ] [Primcodable σ] {f : γδσ} {g : αβγ} {h : αβδ} (hf : Primrec₂ f) (hg : Primrec₂ g) (hh : Primrec₂ h) :
                  Primrec₂ fun (a : α) (b : β) => f (g a b) (h a b)
                  theorem PrimrecPred.comp {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : βProp} [DecidablePred p] {f : αβ} :
                  PrimrecPred pPrimrec fPrimrecPred fun (a : α) => p (f a)
                  theorem PrimrecRel.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {R : βγProp} [(a : β) → (b : γ) → Decidable (R a b)] {f : αβ} {g : αγ} :
                  PrimrecRel RPrimrec fPrimrec gPrimrecPred fun (a : α) => R (f a) (g a)
                  theorem PrimrecRel.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable δ] {R : γδProp} [(a : γ) → (b : δ) → Decidable (R a b)] {f : αβγ} {g : αβδ} :
                  PrimrecRel RPrimrec₂ fPrimrec₂ gPrimrecRel fun (a : α) (b : β) => R (f a b) (g a b)
                  theorem PrimrecPred.of_eq {α : Type u_1} [Primcodable α] {p : αProp} {q : αProp} [DecidablePred p] [DecidablePred q] (hp : PrimrecPred p) (H : ∀ (a : α), p a q a) :
                  theorem PrimrecRel.of_eq {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {r : αβProp} {s : αβProp} [(a : α) → (b : β) → Decidable (r a b)] [(a : α) → (b : β) → Decidable (s a b)] (hr : PrimrecRel r) (H : ∀ (a : α) (b : β), r a b s a b) :
                  theorem Primrec₂.swap {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αβσ} (h : Primrec₂ f) :
                  theorem Primrec₂.nat_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αβσ} :
                  theorem Primrec₂.nat_iff' {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αβσ} :
                  Primrec₂ f Primrec₂ fun (m n : ) => (Encodable.decode m).bind fun (a : α) => Option.map (f a) (Encodable.decode n)
                  theorem Primrec.to₂ {α : Type u_1} {β : Type u_2} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α × βσ} (hf : Primrec f) :
                  Primrec₂ fun (a : α) (b : β) => f (a, b)
                  theorem Primrec.nat_rec {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : αβ} {g : α × ββ} (hf : Primrec f) (hg : Primrec₂ g) :
                  Primrec₂ fun (a : α) (n : ) => Nat.rec (f a) (fun (n : ) (IH : (fun (x : ) => β) n) => g a (n, IH)) n
                  theorem Primrec.nat_rec' {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α} {g : αβ} {h : α × ββ} (hf : Primrec f) (hg : Primrec g) (hh : Primrec₂ h) :
                  Primrec fun (a : α) => Nat.rec (g a) (fun (n : ) (IH : (fun (x : ) => β) n) => h a (n, IH)) (f a)
                  theorem Primrec.nat_rec₁ {α : Type u_1} [Primcodable α] {f : αα} (a : α) (hf : Primrec₂ f) :
                  Primrec fun (t : ) => Nat.rec a f t
                  theorem Primrec.nat_casesOn' {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : αβ} {g : αβ} (hf : Primrec f) (hg : Primrec₂ g) :
                  Primrec₂ fun (a : α) (n : ) => Nat.casesOn n (f a) (g a)
                  theorem Primrec.nat_casesOn {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α} {g : αβ} {h : αβ} (hf : Primrec f) (hg : Primrec g) (hh : Primrec₂ h) :
                  Primrec fun (a : α) => Nat.casesOn (f a) (g a) (h a)
                  theorem Primrec.nat_casesOn₁ {α : Type u_1} [Primcodable α] {f : α} (a : α) (hf : Primrec f) :
                  Primrec fun (n : ) => Nat.casesOn n a f
                  theorem Primrec.nat_iterate {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α} {g : αβ} {h : αββ} (hf : Primrec f) (hg : Primrec g) (hh : Primrec₂ h) :
                  Primrec fun (a : α) => (h a)^[f a] (g a)
                  theorem Primrec.option_casesOn {α : Type u_1} {β : Type u_2} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable σ] {o : αOption β} {f : ασ} {g : αβσ} (ho : Primrec o) (hf : Primrec f) (hg : Primrec₂ g) :
                  Primrec fun (a : α) => Option.casesOn (o a) (f a) (g a)
                  theorem Primrec.option_bind {α : Type u_1} {β : Type u_2} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αOption β} {g : αβOption σ} (hf : Primrec f) (hg : Primrec₂ g) :
                  Primrec fun (a : α) => (f a).bind (g a)
                  theorem Primrec.option_bind₁ {α : Type u_1} {σ : Type u_5} [Primcodable α] [Primcodable σ] {f : αOption σ} (hf : Primrec f) :
                  Primrec fun (o : Option α) => o.bind f
                  theorem Primrec.option_map {α : Type u_1} {β : Type u_2} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αOption β} {g : αβσ} (hf : Primrec f) (hg : Primrec₂ g) :
                  Primrec fun (a : α) => Option.map (g a) (f a)
                  theorem Primrec.option_map₁ {α : Type u_1} {σ : Type u_5} [Primcodable α] [Primcodable σ] {f : ασ} (hf : Primrec f) :
                  theorem Primrec.option_iget {α : Type u_1} [Primcodable α] [Inhabited α] :
                  Primrec Option.iget
                  theorem Primrec.option_isSome {α : Type u_1} [Primcodable α] :
                  Primrec Option.isSome
                  theorem Primrec.option_getD {α : Type u_1} [Primcodable α] :
                  Primrec₂ Option.getD
                  theorem Primrec.bind_decode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αβOption σ} :
                  (Primrec₂ fun (a : α) (n : ) => (Encodable.decode n).bind (f a)) Primrec₂ f
                  theorem Primrec.map_decode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αβσ} :
                  (Primrec₂ fun (a : α) (n : ) => Option.map (f a) (Encodable.decode n)) Primrec₂ f
                  theorem Primrec.nat_add :
                  Primrec₂ fun (x x_1 : ) => x + x_1
                  theorem Primrec.nat_sub :
                  Primrec₂ fun (x x_1 : ) => x - x_1
                  theorem Primrec.nat_mul :
                  Primrec₂ fun (x x_1 : ) => x * x_1
                  theorem Primrec.cond {α : Type u_1} {σ : Type u_5} [Primcodable α] [Primcodable σ] {c : αBool} {f : ασ} {g : ασ} (hc : Primrec c) (hf : Primrec f) (hg : Primrec g) :
                  Primrec fun (a : α) => bif c a then f a else g a
                  theorem Primrec.ite {α : Type u_1} {σ : Type u_5} [Primcodable α] [Primcodable σ] {c : αProp} [DecidablePred c] {f : ασ} {g : ασ} (hc : PrimrecPred c) (hf : Primrec f) (hg : Primrec g) :
                  Primrec fun (a : α) => if c a then f a else g a
                  theorem Primrec.nat_le :
                  PrimrecRel fun (x x_1 : ) => x x_1
                  theorem Primrec.dom_bool {α : Type u_1} [Primcodable α] (f : Boolα) :
                  theorem Primrec.dom_bool₂ {α : Type u_1} [Primcodable α] (f : BoolBoolα) :
                  theorem PrimrecPred.not {α : Type u_1} [Primcodable α] {p : αProp} [DecidablePred p] (hp : PrimrecPred p) :
                  PrimrecPred fun (a : α) => ¬p a
                  theorem PrimrecPred.and {α : Type u_1} [Primcodable α] {p : αProp} {q : αProp} [DecidablePred p] [DecidablePred q] (hp : PrimrecPred p) (hq : PrimrecPred q) :
                  PrimrecPred fun (a : α) => p a q a
                  theorem PrimrecPred.or {α : Type u_1} [Primcodable α] {p : αProp} {q : αProp} [DecidablePred p] [DecidablePred q] (hp : PrimrecPred p) (hq : PrimrecPred q) :
                  PrimrecPred fun (a : α) => p a q a
                  theorem Primrec.beq {α : Type u_1} [Primcodable α] [DecidableEq α] :
                  Primrec₂ BEq.beq
                  theorem Primrec.eq {α : Type u_1} [Primcodable α] [DecidableEq α] :
                  theorem Primrec.nat_lt :
                  PrimrecRel fun (x x_1 : ) => x < x_1
                  theorem Primrec.option_guard {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : αβProp} [(a : α) → (b : β) → Decidable (p a b)] (hp : PrimrecRel p) {f : αβ} (hf : Primrec f) :
                  Primrec fun (a : α) => Option.guard (p a) (f a)
                  theorem Primrec.option_orElse {α : Type u_1} [Primcodable α] :
                  Primrec₂ fun (x x_1 : Option α) => HOrElse.hOrElse x fun (x : Unit) => x_1
                  theorem Primrec.list_findIdx₁ {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : αβBool} (hp : Primrec₂ p) (l : List β) :
                  Primrec fun (a : α) => List.findIdx (p a) l
                  theorem Primrec.list_indexOf₁ {α : Type u_1} [Primcodable α] [DecidableEq α] (l : List α) :
                  Primrec fun (a : α) => List.indexOf a l
                  theorem Primrec.dom_fintype {α : Type u_1} {σ : Type u_5} [Primcodable α] [Primcodable σ] [Finite α] (f : ασ) :
                  def Primrec.PrimrecBounded {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] (f : αβ) :

                  A function is PrimrecBounded if its size is bounded by a primitive recursive function

                  Equations
                  Instances For
                    theorem Primrec.nat_findGreatest {α : Type u_1} [Primcodable α] {f : α} {p : αProp} [(x : α) → (n : ) → Decidable (p x n)] (hf : Primrec f) (hp : PrimrecRel p) :
                    Primrec fun (x : α) => Nat.findGreatest (p x) (f x)
                    theorem Primrec.of_graph {α : Type u_1} [Primcodable α] {f : α} (h₁ : Primrec.PrimrecBounded f) (h₂ : PrimrecRel fun (a : α) (b : ) => f a = b) :

                    To show a function f : α → ℕ is primitive recursive, it is enough to show that the function is bounded by a primitive recursive function and that its graph is primitive recursive

                    theorem Primrec.nat_div :
                    Primrec₂ fun (x x_1 : ) => x / x_1
                    theorem Primrec.nat_mod :
                    Primrec₂ fun (x x_1 : ) => x % x_1
                    theorem Primrec.nat_double :
                    Primrec fun (n : ) => 2 * n
                    theorem Primrec.nat_double_succ :
                    Primrec fun (n : ) => 2 * n + 1
                    instance Primcodable.sum {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] :
                    Equations
                    instance Primcodable.list {α : Type u_1} [Primcodable α] :
                    Equations
                    theorem Primrec.sum_inl {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] :
                    Primrec Sum.inl
                    theorem Primrec.sum_inr {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] :
                    Primrec Sum.inr
                    theorem Primrec.sum_casesOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : αβ γ} {g : αβσ} {h : αγσ} (hf : Primrec f) (hg : Primrec₂ g) (hh : Primrec₂ h) :
                    Primrec fun (a : α) => Sum.casesOn (f a) (g a) (h a)
                    theorem Primrec.list_cons {α : Type u_1} [Primcodable α] :
                    Primrec₂ List.cons
                    theorem Primrec.list_casesOn {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αList β} {g : ασ} {h : αβ × List βσ} :
                    Primrec fPrimrec gPrimrec₂ hPrimrec fun (a : α) => List.casesOn (f a) (g a) fun (b : β) (l : List β) => h a (b, l)
                    theorem Primrec.list_foldl {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αList β} {g : ασ} {h : ασ × βσ} :
                    Primrec fPrimrec gPrimrec₂ hPrimrec fun (a : α) => List.foldl (fun (s : σ) (b : β) => h a (s, b)) (g a) (f a)
                    theorem Primrec.list_reverse {α : Type u_1} [Primcodable α] :
                    Primrec List.reverse
                    theorem Primrec.list_foldr {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αList β} {g : ασ} {h : αβ × σσ} (hf : Primrec f) (hg : Primrec g) (hh : Primrec₂ h) :
                    Primrec fun (a : α) => List.foldr (fun (b : β) (s : σ) => h a (b, s)) (g a) (f a)
                    theorem Primrec.list_head? {α : Type u_1} [Primcodable α] :
                    Primrec List.head?
                    theorem Primrec.list_headI {α : Type u_1} [Primcodable α] [Inhabited α] :
                    Primrec List.headI
                    theorem Primrec.list_tail {α : Type u_1} [Primcodable α] :
                    Primrec List.tail
                    theorem Primrec.list_rec {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αList β} {g : ασ} {h : αβ × List β × σσ} (hf : Primrec f) (hg : Primrec g) (hh : Primrec₂ h) :
                    Primrec fun (a : α) => List.recOn (f a) (g a) fun (b : β) (l : List β) (IH : σ) => h a (b, l, IH)
                    theorem Primrec.list_get? {α : Type u_1} [Primcodable α] :
                    Primrec₂ List.get?
                    theorem Primrec.list_getD {α : Type u_1} [Primcodable α] (d : α) :
                    Primrec₂ fun (l : List α) (n : ) => l.getD n d
                    theorem Primrec.list_getI {α : Type u_1} [Primcodable α] [Inhabited α] :
                    Primrec₂ List.getI
                    theorem Primrec.list_append {α : Type u_1} [Primcodable α] :
                    Primrec₂ fun (x x_1 : List α) => x ++ x_1
                    theorem Primrec.list_concat {α : Type u_1} [Primcodable α] :
                    Primrec₂ fun (l : List α) (a : α) => l ++ [a]
                    theorem Primrec.list_map {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αList β} {g : αβσ} (hf : Primrec f) (hg : Primrec₂ g) :
                    Primrec fun (a : α) => List.map (g a) (f a)
                    theorem Primrec.list_join {α : Type u_1} [Primcodable α] :
                    Primrec List.join
                    theorem Primrec.list_bind {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αList β} {g : αβList σ} (hf : Primrec f) (hg : Primrec₂ g) :
                    Primrec fun (a : α) => (f a).bind (g a)
                    theorem Primrec.optionToList {α : Type u_1} [Primcodable α] :
                    Primrec Option.toList
                    theorem Primrec.listFilterMap {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αList β} {g : αβOption σ} (hf : Primrec f) (hg : Primrec₂ g) :
                    Primrec fun (a : α) => List.filterMap (g a) (f a)
                    theorem Primrec.list_length {α : Type u_1} [Primcodable α] :
                    Primrec List.length
                    theorem Primrec.list_findIdx {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : αList β} {p : αβBool} (hf : Primrec f) (hp : Primrec₂ p) :
                    Primrec fun (a : α) => List.findIdx (p a) (f a)
                    theorem Primrec.list_indexOf {α : Type u_1} [Primcodable α] [DecidableEq α] :
                    Primrec₂ List.indexOf
                    theorem Primrec.nat_strong_rec {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] (f : ασ) {g : αList σOption σ} (hg : Primrec₂ g) (H : ∀ (a : α) (n : ), g a (List.map (f a) (List.range n)) = some (f a n)) :
                    theorem Primrec.listLookup {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] [DecidableEq α] :
                    Primrec₂ List.lookup
                    theorem Primrec.nat_omega_rec' {β : Type u_2} {σ : Type u_4} [Primcodable β] [Primcodable σ] (f : βσ) {m : β} {l : βList β} {g : βList σOption σ} (hm : Primrec m) (hl : Primrec l) (hg : Primrec₂ g) (Ord : ∀ (b b' : β), b' l bm b' < m b) (H : ∀ (b : β), g b (List.map f (l b)) = some (f b)) :
                    theorem Primrec.nat_omega_rec {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] (f : αβσ) {m : αβ} {l : αβList β} {g : αβ × List σOption σ} (hm : Primrec₂ m) (hl : Primrec₂ l) (hg : Primrec₂ g) (Ord : ∀ (a : α) (b b' : β), b' l a bm a b' < m a b) (H : ∀ (a : α) (b : β), g a (b, List.map (f a) (l a b)) = some (f a b)) :
                    def Primcodable.subtype {α : Type u_1} [Primcodable α] {p : αProp} [DecidablePred p] (hp : PrimrecPred p) :

                    A subtype of a primitive recursive predicate is Primcodable.

                    Equations
                    Instances For
                      instance Primcodable.fin {n : } :
                      Equations
                      instance Primcodable.vector {α : Type u_1} [Primcodable α] {n : } :
                      Equations
                      instance Primcodable.finArrow {α : Type u_1} [Primcodable α] {n : } :
                      Primcodable (Fin nα)
                      Equations
                      theorem Primcodable.mem_range_encode {α : Type u_1} [Primcodable α] :
                      PrimrecPred fun (n : ) => n Set.range Encodable.encode
                      instance Primcodable.ulower {α : Type u_1} [Primcodable α] :
                      Equations
                      theorem Primrec.subtype_val {α : Type u_1} [Primcodable α] {p : αProp} [DecidablePred p] {hp : PrimrecPred p} :
                      Primrec Subtype.val
                      theorem Primrec.subtype_val_iff {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : βProp} [DecidablePred p] {hp : PrimrecPred p} {f : αSubtype p} :
                      (Primrec fun (a : α) => (f a)) Primrec f
                      theorem Primrec.subtype_mk {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : βProp} [DecidablePred p] {hp : PrimrecPred p} {f : αβ} {h : ∀ (a : α), p (f a)} (hf : Primrec f) :
                      Primrec fun (a : α) => f a,
                      theorem Primrec.option_get {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : αOption β} {h : ∀ (a : α), (f a).isSome = true} :
                      Primrec fPrimrec fun (a : α) => (f a).get
                      theorem Primrec.ulower_down {α : Type u_1} [Primcodable α] :
                      Primrec ULower.down
                      theorem Primrec.ulower_up {α : Type u_1} [Primcodable α] :
                      Primrec ULower.up
                      theorem Primrec.fin_val_iff {α : Type u_1} [Primcodable α] {n : } {f : αFin n} :
                      (Primrec fun (a : α) => (f a)) Primrec f
                      theorem Primrec.fin_val {n : } :
                      Primrec fun (i : Fin n) => i
                      theorem Primrec.fin_succ {n : } :
                      Primrec Fin.succ
                      theorem Primrec.vector_toList {α : Type u_1} [Primcodable α] {n : } :
                      Primrec Vector.toList
                      theorem Primrec.vector_toList_iff {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {n : } {f : αVector β n} :
                      (Primrec fun (a : α) => (f a).toList) Primrec f
                      theorem Primrec.vector_cons {α : Type u_1} [Primcodable α] {n : } :
                      Primrec₂ Vector.cons
                      theorem Primrec.vector_length {α : Type u_1} [Primcodable α] {n : } :
                      Primrec Vector.length
                      theorem Primrec.vector_head {α : Type u_1} [Primcodable α] {n : } :
                      Primrec Vector.head
                      theorem Primrec.vector_tail {α : Type u_1} [Primcodable α] {n : } :
                      Primrec Vector.tail
                      theorem Primrec.vector_get {α : Type u_1} [Primcodable α] {n : } :
                      Primrec₂ Vector.get
                      theorem Primrec.list_ofFn {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {n : } {f : Fin nασ} :
                      (∀ (i : Fin n), Primrec (f i))Primrec fun (a : α) => List.ofFn fun (i : Fin n) => f i a
                      theorem Primrec.vector_ofFn {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {n : } {f : Fin nασ} (hf : ∀ (i : Fin n), Primrec (f i)) :
                      Primrec fun (a : α) => Vector.ofFn fun (i : Fin n) => f i a
                      theorem Primrec.vector_get' {α : Type u_1} [Primcodable α] {n : } :
                      Primrec Vector.get
                      theorem Primrec.vector_ofFn' {α : Type u_1} [Primcodable α] {n : } :
                      Primrec Vector.ofFn
                      theorem Primrec.fin_app {σ : Type u_4} [Primcodable σ] {n : } :
                      theorem Primrec.fin_curry₁ {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {n : } {f : Fin nασ} :
                      Primrec₂ f ∀ (i : Fin n), Primrec (f i)
                      theorem Primrec.fin_curry {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {n : } {f : αFin nσ} :
                      inductive Nat.Primrec' {n : } :
                      (Vector n)Prop

                      An alternative inductive definition of Primrec which does not use the pairing function on ℕ, and so has to work with n-ary functions on ℕ instead of unary functions. We prove that this is equivalent to the regular notion in to_prim and of_prim.

                      Instances For
                        theorem Nat.Primrec'.to_prim {n : } {f : Vector n} (pf : Nat.Primrec' f) :
                        theorem Nat.Primrec'.of_eq {n : } {f : Vector n} {g : Vector n} (hf : Nat.Primrec' f) (H : ∀ (i : Vector n), f i = g i) :
                        theorem Nat.Primrec'.const {n : } (m : ) :
                        Nat.Primrec' fun (x : Vector n) => m
                        theorem Nat.Primrec'.head {n : } :
                        Nat.Primrec' Vector.head
                        theorem Nat.Primrec'.tail {n : } {f : Vector n} (hf : Nat.Primrec' f) :
                        Nat.Primrec' fun (v : Vector n.succ) => f v.tail
                        def Nat.Primrec'.Vec {n : } {m : } (f : Vector nVector m) :

                        A function from vectors to vectors is primitive recursive when all of its projections are.

                        Equations
                        Instances For
                          theorem Nat.Primrec'.nil {n : } :
                          Nat.Primrec'.Vec fun (x : Vector n) => Vector.nil
                          theorem Nat.Primrec'.cons {n : } {m : } {f : Vector n} {g : Vector nVector m} (hf : Nat.Primrec' f) (hg : Nat.Primrec'.Vec g) :
                          Nat.Primrec'.Vec fun (v : Vector n) => f v ::ᵥ g v
                          theorem Nat.Primrec'.comp' {n : } {m : } {f : Vector m} {g : Vector nVector m} (hf : Nat.Primrec' f) (hg : Nat.Primrec'.Vec g) :
                          Nat.Primrec' fun (v : Vector n) => f (g v)
                          theorem Nat.Primrec'.comp₁ (f : ) (hf : Nat.Primrec' fun (v : Vector 1) => f v.head) {n : } {g : Vector n} (hg : Nat.Primrec' g) :
                          Nat.Primrec' fun (v : Vector n) => f (g v)
                          theorem Nat.Primrec'.comp₂ (f : ) (hf : Nat.Primrec' fun (v : Vector 2) => f v.head v.tail.head) {n : } {g : Vector n} {h : Vector n} (hg : Nat.Primrec' g) (hh : Nat.Primrec' h) :
                          Nat.Primrec' fun (v : Vector n) => f (g v) (h v)
                          theorem Nat.Primrec'.prec' {n : } {f : Vector n} {g : Vector n} {h : Vector (n + 2)} (hf : Nat.Primrec' f) (hg : Nat.Primrec' g) (hh : Nat.Primrec' h) :
                          Nat.Primrec' fun (v : Vector n) => Nat.rec (g v) (fun (y IH : ) => h (y ::ᵥ IH ::ᵥ v)) (f v)
                          theorem Nat.Primrec'.pred :
                          Nat.Primrec' fun (v : Vector 1) => v.head.pred
                          theorem Nat.Primrec'.add :
                          Nat.Primrec' fun (v : Vector 2) => v.head + v.tail.head
                          theorem Nat.Primrec'.sub :
                          Nat.Primrec' fun (v : Vector 2) => v.head - v.tail.head
                          theorem Nat.Primrec'.mul :
                          Nat.Primrec' fun (v : Vector 2) => v.head * v.tail.head
                          theorem Nat.Primrec'.if_lt {n : } {a : Vector n} {b : Vector n} {f : Vector n} {g : Vector n} (ha : Nat.Primrec' a) (hb : Nat.Primrec' b) (hf : Nat.Primrec' f) (hg : Nat.Primrec' g) :
                          Nat.Primrec' fun (v : Vector n) => if a v < b v then f v else g v
                          theorem Nat.Primrec'.natPair :
                          Nat.Primrec' fun (v : Vector 2) => Nat.pair v.head v.tail.head
                          theorem Nat.Primrec'.encode {n : } :
                          Nat.Primrec' Encodable.encode
                          theorem Nat.Primrec'.sqrt :
                          Nat.Primrec' fun (v : Vector 1) => v.head.sqrt
                          theorem Nat.Primrec'.unpair₁ {n : } {f : Vector n} (hf : Nat.Primrec' f) :
                          Nat.Primrec' fun (v : Vector n) => (Nat.unpair (f v)).1
                          theorem Nat.Primrec'.unpair₂ {n : } {f : Vector n} (hf : Nat.Primrec' f) :
                          Nat.Primrec' fun (v : Vector n) => (Nat.unpair (f v)).2
                          theorem Nat.Primrec'.of_prim {n : } {f : Vector n} :
                          theorem Nat.Primrec'.prim_iff₁ {f : } :
                          (Nat.Primrec' fun (v : Vector 1) => f v.head) Primrec f
                          theorem Nat.Primrec'.prim_iff₂ {f : } :
                          (Nat.Primrec' fun (v : Vector 2) => f v.head v.tail.head) Primrec₂ f