theorem Nat.pos_of_eq_one {n : ℕ} (h : n = 1) : 0 < n

def Nat.isEqNat (n m : ℕ) : ℕ

Equations

• n.isEqNat m = if n = m then 1 else 0

def Nat.isLtNat (n m : ℕ) : ℕ

Equations

• n.isLtNat m = if n < m then 1 else 0

def Nat.isLeNat (n m : ℕ) : ℕ

Equations

• n.isLeNat m = if n ≤ m then 1 else 0

def Nat.isDvdNat (n m : ℕ) : ℕ

Equations

• n.isDvdNat m = if n ∣ m then 1 else 0

@[simp]

theorem Nat.isEqNat_pos_iff {n m : ℕ} : 0 < n.isEqNat m ↔ n = m

@[simp]

theorem Nat.isLtNat_pos_iff {n m : ℕ} : 0 < n.isLtNat m ↔ n < m

@[simp]

theorem Nat.isLeNat_pos_iff {n m : ℕ} : 0 < n.isLeNat m ↔ n ≤ m

@[simp]

theorem Nat.isDvdNat_pos_iff {n m : ℕ} : 0 < n.isDvdNat m ↔ n ∣ m

def Nat.inv (n : ℕ) : ℕ

Equations

• n.inv = n.isEqNat 0

def Nat.pos (n : ℕ) : ℕ

Equations

• n.pos = Nat.isLtNat 0 n

@[simp]

theorem Nat.inv_zero : inv 0 = 1

@[simp]

theorem Nat.inv_iff_ne_zero {n : ℕ} : n.inv = 0 ↔ 0 < n

@[simp]

theorem Nat.inv_ne_zero {n : ℕ} (h : n ≠ 0) : n.inv = 0

@[simp]

theorem Nat.pos_zero : pos 0 = 0

@[simp]

theorem Nat.pos_ne_zero {n : ℕ} (h : n ≠ 0) : n.pos = 1

def Nat.and (n m : ℕ) : ℕ

Equations

• n.and m = Nat.isLtNat 0 (n * m)

def Nat.or (n m : ℕ) : ℕ

Equations

• n.or m = Nat.isLtNat 0 (n + m)

theorem Nat.and_eq (n m : ℕ) : n.and m = if 0 < n ∧ 0 < m then 1 else 0

theorem Nat.and_eq_one (n m : ℕ) : n.and m = 1 ↔ 0 < n ∧ 0 < m

theorem Nat.or_eq (n m : ℕ) : n.or m = if 0 < n ∨ 0 < m then 1 else 0

@[simp]

theorem Nat.and_pos_iff (n m : ℕ) : 0 < n.and m ↔ 0 < n ∧ 0 < m

@[simp]

theorem Nat.or_pos_iff (n m : ℕ) : 0 < n.or m ↔ 0 < n ∨ 0 < m

@[simp]

theorem Nat.inv_pos_iff (n : ℕ) : 0 < n.inv ↔ ¬0 < n

@[simp]

theorem Nat.pos_pos_iff (n : ℕ) : 0 < n.pos ↔ 0 < n

def Nat.ball (n : ℕ) (φ : ℕ → ℕ) : ℕ

Equations

• n.ball φ = Nat.rec 1 (fun (n ih : ℕ) => (φ n).pos.and ih) n

@[simp]

theorem Nat.ball_pos_iff {φ : ℕ → ℕ} {n : ℕ} : 0 < n.ball φ ↔ ∀ m < n, 0 < φ m

@[simp]

theorem Nat.ball_eq_zero_iff {φ : ℕ → ℕ} {n : ℕ} : n.ball φ = 0 ↔ ∃ m < n, φ m = 0

theorem Nat.ball_pos_iff_eq_one {φ : ℕ → ℕ} {n : ℕ} : n.ball φ = 1 ↔ 0 < n.ball φ

inductive Nat.ArithPart₁ {n : ℕ} : (List.Vector ℕ n →. ℕ) → Prop

• zero {n : ℕ} : ArithPart₁ fun (x : List.Vector ℕ n) => 0
• one {n : ℕ} : ArithPart₁ fun (x : List.Vector ℕ n) => 1
• add {n : ℕ} (i j : Fin n) : ArithPart₁ ↑fun (v : List.Vector ℕ n) => v.get i + v.get j
• mul {n : ℕ} (i j : Fin n) : ArithPart₁ ↑fun (v : List.Vector ℕ n) => v.get i * v.get j
• proj {n : ℕ} (i : Fin n) : ArithPart₁ ↑fun (v : List.Vector ℕ n) => v.get i
• equal {n : ℕ} (i j : Fin n) : ArithPart₁ ↑fun (v : List.Vector ℕ n) => (v.get i).isEqNat (v.get j)
• lt {n : ℕ} (i j : Fin n) : ArithPart₁ ↑fun (v : List.Vector ℕ n) => (v.get i).isLtNat (v.get j)
• comp {m n : ℕ} {f : List.Vector ℕ n →. ℕ} (g : Fin n → List.Vector ℕ m →. ℕ) : ArithPart₁ f → (∀ (i : Fin n), ArithPart₁ (g i)) → ArithPart₁ fun (v : List.Vector ℕ m) => (List.Vector.mOfFn fun (i : Fin n) => g i v) >>= f
• rfind {n : ℕ} {f : List.Vector ℕ (n + 1) → ℕ} : ArithPart₁ ↑f → ArithPart₁ fun (v : List.Vector ℕ n) => Nat.rfind fun (n_1 : ℕ) => Part.some (decide (f (n_1 ::ᵥ v) = 0))

def Nat.Arith₁ {n : ℕ} (f : List.Vector ℕ n → ℕ) : Prop

Equations

• Nat.Arith₁ f = Nat.ArithPart₁ ↑f

theorem Nat.ArithPart₁.to_partrec' {n : ℕ} {f : List.Vector ℕ n →. ℕ} (hf : ArithPart₁ f) : Partrec' f

theorem Nat.ArithPart₁.of_eq {n : ℕ} {f g : List.Vector ℕ n →. ℕ} (hf : ArithPart₁ f) (H : ∀ (i : List.Vector ℕ n), f i = g i) : ArithPart₁ g

theorem Nat.ArithPart₁.bind {n : ℕ} (f : List.Vector ℕ n → ℕ →. ℕ) (hf : ArithPart₁ fun (v : List.Vector ℕ (n + 1)) => f v.tail v.head) {g : List.Vector ℕ n →. ℕ} (hg : ArithPart₁ g) : ArithPart₁ fun (v : List.Vector ℕ n) => (g v).bind (f v)

theorem Nat.ArithPart₁.map {n : ℕ} (f : List.Vector ℕ n → ℕ → ℕ) (hf : Arith₁ fun (v : List.Vector ℕ (n + 1)) => f v.tail v.head) {g : List.Vector ℕ n →. ℕ} (hg : ArithPart₁ g) : ArithPart₁ fun (v : List.Vector ℕ n) => Part.map (f v) (g v)

theorem Nat.ArithPart₁.comp₁ (f : ℕ →. ℕ) (hf : ArithPart₁ fun (v : List.Vector ℕ 1) => f (v.get 0)) {n : ℕ} {g : List.Vector ℕ n → ℕ} (hg : Arith₁ g) : ArithPart₁ fun (v : List.Vector ℕ n) => f (g v)

theorem Nat.ArithPart₁.comp₂ (f : ℕ → ℕ →. ℕ) (hf : ArithPart₁ fun (v : List.Vector ℕ 2) => f (v.get 0) (v.get 1)) {n : ℕ} {g h : List.Vector ℕ n → ℕ} (hg : Arith₁ g) (hh : Arith₁ h) : ArithPart₁ fun (v : List.Vector ℕ n) => f (g v) (h v)

theorem Nat.ArithPart₁.rfind' {n : ℕ} {f : ℕ → List.Vector ℕ n → ℕ} (h : Arith₁ fun (v : List.Vector ℕ (n + 1)) => f v.head v.tail) : ArithPart₁ fun (v : List.Vector ℕ n) => Nat.rfind fun (n : ℕ) => Part.some (decide (f n v = 0))

theorem Nat.ArithPart₁.rfind'₁ {n : ℕ} (i : Fin n) {f : ℕ → ℕ → ℕ} (h : Arith₁ fun (v : List.Vector ℕ 2) => f (v.get 0) (v.get 1)) : ArithPart₁ fun (v : List.Vector ℕ n) => Nat.rfind fun (n_1 : ℕ) => Part.some (decide (f n_1 (v.get i) = 0))

theorem Nat.Arith₁.of_eq {n : ℕ} {f g : List.Vector ℕ n → ℕ} (hf : Arith₁ f) (H : ∀ (i : List.Vector ℕ n), f i = g i) : Arith₁ g

theorem Nat.Arith₁.zero {n : ℕ} : Arith₁ fun (x : List.Vector ℕ n) => 0

theorem Nat.Arith₁.one {n : ℕ} : Arith₁ fun (x : List.Vector ℕ n) => 1

theorem Nat.Arith₁.add {n : ℕ} (i j : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => v.get i + v.get j

theorem Nat.Arith₁.mul {n : ℕ} (i j : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => v.get i * v.get j

theorem Nat.Arith₁.proj {n : ℕ} (i : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => v.get i

theorem Nat.Arith₁.head {n : ℕ} : Arith₁ fun (v : List.Vector ℕ (n + 1)) => v.head

theorem Nat.Arith₁.equal {n : ℕ} (i j : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => (v.get i).isEqNat (v.get j)

theorem Nat.Arith₁.lt {n : ℕ} (i j : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => (v.get i).isLtNat (v.get j)

theorem Nat.Arith₁.comp {m n : ℕ} {f : List.Vector ℕ n → ℕ} (g : Fin n → List.Vector ℕ m → ℕ) (hf : Arith₁ f) (hg : ∀ (i : Fin n), Arith₁ (g i)) : Arith₁ fun (v : List.Vector ℕ m) => f (List.Vector.ofFn fun (i : Fin n) => g i v)

def Nat.Arith₁.Vec {n m : ℕ} (f : List.Vector ℕ n → List.Vector ℕ m) : Prop

Equations

• Nat.Arith₁.Vec f = ∀ (i : Fin m), Nat.Arith₁ fun (v : List.Vector ℕ n) => (f v).get i

theorem Nat.Arith₁.nil {n : ℕ} : Vec fun (x : List.Vector ℕ n) => List.Vector.nil

theorem Nat.Arith₁.cons {n m : ℕ} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ n → List.Vector ℕ m} (hf : Arith₁ f) (hg : Vec g) : Vec fun (v : List.Vector ℕ n) => f v ::ᵥ g v

theorem Nat.Arith₁.tail {n : ℕ} {f : List.Vector ℕ n → ℕ} (hf : Arith₁ f) : Arith₁ fun (v : List.Vector ℕ n.succ) => f v.tail

theorem Nat.Arith₁.comp' {n m : ℕ} {f : List.Vector ℕ m → ℕ} {g : List.Vector ℕ n → List.Vector ℕ m} (hf : Arith₁ f) (hg : Vec g) : Arith₁ fun (v : List.Vector ℕ n) => f (g v)

theorem Nat.Arith₁.comp₁ (f : ℕ → ℕ) (hf : Arith₁ fun (v : List.Vector ℕ 1) => f (v.get 0)) {n : ℕ} {g : List.Vector ℕ n → ℕ} (hg : Arith₁ g) : Arith₁ fun (v : List.Vector ℕ n) => f (g v)

theorem Nat.Arith₁.comp₂ (f : ℕ → ℕ → ℕ) (hf : Arith₁ fun (v : List.Vector ℕ 2) => f (v.get 0) (v.get 1)) {n : ℕ} {g h : List.Vector ℕ n → ℕ} (hg : Arith₁ g) (hh : Arith₁ h) : Arith₁ fun (v : List.Vector ℕ n) => f (g v) (h v)

theorem Nat.Arith₁.succ {n : ℕ} (i : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => v.get i + 1

theorem Nat.Arith₁.const {n : ℕ} (m : ℕ) : Arith₁ fun (x : List.Vector ℕ n) => m

theorem Nat.Arith₁.inv {n : ℕ} (i : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => (v.get i).inv

theorem Nat.Arith₁.pos {n : ℕ} (i : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => (v.get i).pos

theorem Nat.Arith₁.and {n : ℕ} (i j : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => (v.get i).and (v.get j)

theorem Nat.Arith₁.or {n : ℕ} (i j : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => (v.get i).or (v.get j)

theorem Nat.Arith₁.le {n : ℕ} (i j : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => (v.get i).isLeNat (v.get j)

theorem Nat.Arith₁.if_pos {n : ℕ} {f g h : List.Vector ℕ n → ℕ} (hf : Arith₁ f) (hg : Arith₁ g) (hh : Arith₁ h) : Arith₁ fun (v : List.Vector ℕ n) => if 0 < f v then g v else h v

theorem Nat.Arith₁.to_arith₁ {n : ℕ} {f : List.Vector ℕ n → ℕ} (h : Arith₁ f) : ArithPart₁ fun (x : List.Vector ℕ n) => ↑(some (f x))

theorem Nat.ArithPart₁.rfindPos {n : ℕ} {f : List.Vector ℕ (n + 1) → ℕ} (h : Arith₁ f) : ArithPart₁ fun (v : List.Vector ℕ n) => Nat.rfind fun (n_1 : ℕ) => Part.some (decide (0 < f (n_1 ::ᵥ v)))

theorem Nat.ArithPart₁.rfindPos₁ {n : ℕ} (i : Fin n) {f : ℕ → ℕ → ℕ} (h : Arith₁ fun (v : List.Vector ℕ 2) => f (v.get 0) (v.get 1)) : ArithPart₁ fun (v : List.Vector ℕ n) => Nat.rfind fun (n_1 : ℕ) => Part.some (decide (0 < f n_1 (v.get i)))

theorem Nat.ArithPart₁.inv_fun {n : ℕ} (i : Fin n) (f : ℕ → ℕ) (hf : Arith₁ fun (v : List.Vector ℕ 1) => f (v.get 0)) : ArithPart₁ fun (v : List.Vector ℕ n) => Nat.rfind fun (x : ℕ) => Part.some (decide (f x ≤ v.get i ∧ v.get i < f (x + 1)))

theorem Nat.ArithPart₁.implicit_fun {n : ℕ} (i : Fin n) (f : List.Vector ℕ n → ℕ → ℕ) (hf : Arith₁ fun (v : List.Vector ℕ (n + 1)) => f v.tail v.head) : ArithPart₁ fun (v : List.Vector ℕ n) => Nat.rfind fun (x : ℕ) => Part.some (decide (f v x ≤ v.get i ∧ v.get i < f v (x + 1)))

theorem Nat.Arith₁.sqrt {n : ℕ} (i : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => (v.get i).sqrt

theorem Nat.Arith₁.sub {n : ℕ} (i j : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => v.get i - v.get j

theorem Nat.Arith₁.pair {n : ℕ} (i j : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => pair (v.get i) (v.get j)

theorem Nat.Arith₁.unpair₁ {n : ℕ} (i : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => (unpair (v.get i)).1

theorem Nat.Arith₁.unpair₂ {n : ℕ} (i : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => (unpair (v.get i)).2

theorem Nat.Arith₁.dvd {n : ℕ} (i j : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => (v.get i).isDvdNat (v.get j)

theorem Nat.Arith₁.rem {n : ℕ} (i j : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => v.get i % v.get j

theorem Nat.Arith₁.beta {n : ℕ} (i j : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => (v.get i).beta (v.get j)

theorem Nat.Arith₁.ball {n : ℕ} {φ : List.Vector ℕ n → ℕ → ℕ} (hp : Arith₁ fun (v : List.Vector ℕ (n + 1)) => φ v.tail v.head) (i : Fin n) : Arith₁ fun (v : List.Vector ℕ n) => (v.get i).ball (φ v)

def Nat.Arith₁.recSequence {n : ℕ} (f : List.Vector ℕ n → ℕ) (g : List.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : List.Vector ℕ n) : List ℕ

Equations

• Nat.Arith₁.recSequence f g z v = List.ofFn fun (i : Fin (z + 1)) => Nat.recOn (↑i) (f v) fun (y IH : ℕ) => g (y ::ᵥ IH ::ᵥ v)

theorem Nat.Arith₁.beta_unbeta_recSequence_eq {n : ℕ} (f : List.Vector ℕ n → ℕ) (g : List.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : List.Vector ℕ n) (m : ℕ) (hm : m < z + 1) : (unbeta (recSequence f g z v)).beta m = rec (f v) (fun (y IH : ℕ) => g (y ::ᵥ IH ::ᵥ v)) m

theorem Nat.Arith₁.beta_unbeta_recSequence_zero {n : ℕ} (f : List.Vector ℕ n → ℕ) (g : List.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : List.Vector ℕ n) : (unbeta (recSequence f g z v)).beta 0 = f v

theorem Nat.Arith₁.beta_unbeta_recSequence_succ {n : ℕ} (f : List.Vector ℕ n → ℕ) (g : List.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : List.Vector ℕ n) {m : ℕ} (hm : m < z) : (unbeta (recSequence f g z v)).beta (m + 1) = g (m ::ᵥ (unbeta (recSequence f g z v)).beta m ::ᵥ v)

theorem Nat.Arith₁.beta_eq_rec {n m : ℕ} (f : List.Vector ℕ n → ℕ) (g : List.Vector ℕ (n + 2) → ℕ) {z : ℕ} {v : List.Vector ℕ n} (h0 : z.beta 0 = f v) (hs : ∀ i < m, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v)) : z.beta m = rec (f v) (fun (y IH : ℕ) => g (y ::ᵥ IH ::ᵥ v)) m

theorem Nat.Arith₁.prec {n : ℕ} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ (n + 2) → ℕ} (hf : Arith₁ f) (hg : Arith₁ g) : Arith₁ fun (v : List.Vector ℕ (n + 1)) => rec (f v.tail) (fun (y IH : ℕ) => g (y ::ᵥ IH ::ᵥ v.tail)) v.head

theorem Nat.Arith₁.of_primrec {n : ℕ} {f : List.Vector ℕ n → ℕ} (hf : Primrec' f) : Arith₁ f

theorem Nat.ArithPart₁.of_partrec {n : ℕ} {f : List.Vector ℕ n →. ℕ} (hf : Partrec' f) : ArithPart₁ f

inductive Nat.ArithPart₁.Code : ℕ → Type

• zero (n : ℕ) : Code n
• one (n : ℕ) : Code n
• add {n : ℕ} (i j : Fin n) : Code n
• mul {n : ℕ} (i j : Fin n) : Code n
• proj {n : ℕ} (i : Fin n) : Code n
• equal {n : ℕ} (i j : Fin n) : Code n
• lt {n : ℕ} (i j : Fin n) : Code n
• comp {m n : ℕ} : Code n → (Fin n → Code m) → Code m
• rfind {n : ℕ} : Code (n + 1) → Code n

instance Nat.ArithPart₁.instInhabitedCode (k : ℕ) : Inhabited (Code k)

Equations

• Nat.ArithPart₁.instInhabitedCode k = { default := Nat.ArithPart₁.Code.zero k }

inductive Nat.ArithPart₁.Code.eval {n : ℕ} : Code n → (List.Vector ℕ n →. ℕ) → Prop

• zero {n : ℕ} : (Code.zero n).eval fun (x : List.Vector ℕ n) => 0
• one {n : ℕ} : (Code.one n).eval fun (x : List.Vector ℕ n) => 1
• add {n : ℕ} (i j : Fin n) : (Code.add i j).eval fun (v : List.Vector ℕ n) => ↑(some (v.get i + v.get j))
• mul {n : ℕ} (i j : Fin n) : (Code.mul i j).eval fun (v : List.Vector ℕ n) => ↑(some (v.get i * v.get j))
• proj {n : ℕ} (i : Fin n) : (Code.proj i).eval fun (v : List.Vector ℕ n) => ↑(some (v.get i))
• equal {n : ℕ} (i j : Fin n) : (Code.equal i j).eval fun (v : List.Vector ℕ n) => ↑(some ((v.get i).isEqNat (v.get j)))
• lt {n : ℕ} (i j : Fin n) : (Code.lt i j).eval fun (v : List.Vector ℕ n) => ↑(some ((v.get i).isLtNat (v.get j)))
• comp {m n : ℕ} (c : Code n) (d : Fin n → Code m) (f : List.Vector ℕ n →. ℕ) (g : Fin n → List.Vector ℕ m →. ℕ) : c.eval f → (∀ (i : Fin n), (d i).eval (g i)) → (c.comp d).eval fun (v : List.Vector ℕ m) => (List.Vector.mOfFn fun (i : Fin n) => g i v) >>= f
• rfind {n : ℕ} (c : Code (n + 1)) (f : List.Vector ℕ (n + 1) → ℕ) : c.eval ↑f → c.rfind.eval fun (v : List.Vector ℕ n) => Nat.rfind fun (n_1 : ℕ) => Part.some (decide (f (n_1 ::ᵥ v) = 0))

theorem Nat.ArithPart₁.exists_code {n : ℕ} {f : List.Vector ℕ n →. ℕ} : ArithPart₁ f → ∃ (c : Code n), c.eval f