Defining modulo as a primitive recursive function

Stream: lean4

[Rui Liu]

I'm trying to use lean to define primitive recursive functions as an inductive type. But I faced some problem when trying to define modulo after several check.

def Fin.cons {α : Type} {n : ℕ} (x : α) (f : Fin n → α) : Fin (n+1) → α
  | ⟨0, _⟩ => x
  | ⟨i+1, h⟩ => f ⟨i, Nat.lt_of_succ_lt_succ h⟩

def Fin.tail {α : Type} {n : ℕ} (f : Fin (n+1) → α) : Fin n → α
  | ⟨i, h⟩ => f ⟨i+1, Nat.succ_lt_succ h⟩

def Fin.list {α : Type} (l : List α) : Fin l.length → α := λ i => l[i]

inductive PrimRecFunc : (n : ℕ) → Type
  | zero : PrimRecFunc n
  | succ : PrimRecFunc 1
  | proj : Fin n → PrimRecFunc n
  | comp {m : ℕ} : PrimRecFunc m → (Fin m → PrimRecFunc n) → PrimRecFunc n
  | recr : PrimRecFunc n → PrimRecFunc (n+2) → PrimRecFunc (n+1)

def PrimRecFunc.eval : ∀ {n : ℕ}, PrimRecFunc n → (Fin n → ℕ) → ℕ
  | _, PrimRecFunc.zero => (λ _ => 0)
  | _, PrimRecFunc.succ => (λ xs => xs 0 + 1)
  | _, PrimRecFunc.proj i => (λ xs => xs i)
  | _, PrimRecFunc.comp f gs => (λ xs => f.eval (λ i => (gs i).eval xs))
  | _, PrimRecFunc.recr f g => (λ xs =>
    let x := xs 0
    let xs' := Fin.tail xs
    Nat.rec (f.eval xs') (λ c r => g.eval (Fin.cons c (Fin.cons r xs'))) x
  )

/-
 - pred(0) = 0
 - pred(x') = x
 -/
def PrimRecFunc.pred : PrimRecFunc 1 :=
  recr zero (proj 0)

/-
 - sub'(0, y) = y
 - sub'(x', y) = pred(sub'(x, y))
 -/
def PrimRecFunc.sub : PrimRecFunc 2 :=
  let sub' : PrimRecFunc 2 := recr (proj 0) (comp pred (Fin.list [proj 1]))
  comp sub' (Fin.list [proj 1, proj 0])

/-
 - mod(0, y) = 0
 - mod(x', y) = sub(mod(x, y)', y)
 -/
def PrimRecFunc.mod : PrimRecFunc 2 :=
  recr zero (comp sub (Fin.list [comp succ (Fin.list [proj 1]), proj 2]))

#eval mod.eval (Fin.list [8, 3]) -- Gives wrong result 0

I don't know where I got wrong. The pred and sub functions defined above seem to yield correct result always. Can somebody help check?

[Rui Liu]

I have also defined a bunch of other primitive recursive functions and all seem to give correct result:

def PrimRecFunc.const {n : ℕ} (c : ℕ) : PrimRecFunc n :=
  List.foldl (λ acc _ => comp succ (Fin.list [acc])) zero (List.range c)

/-
 - add(0, y) = y
 - add(x', y) = add(x, y)'
 -/
def PrimRecFunc.add : PrimRecFunc 2 :=
  recr (proj 0) (comp succ (Fin.list [proj 1]))

/-
 - mul(0, y) = 0
 - mul(x', y) = add(y, mul(x, y))
 -/
def PrimRecFunc.mul : PrimRecFunc 2 :=
  recr zero (comp add (Fin.list [proj 2, proj 1]))

/-
 - pow'(0, y) = 1
 - pow'(x', y) = mul(y, pow'(x, y))
 -/
def PrimRecFunc.pow : PrimRecFunc 2 :=
  let pow' : PrimRecFunc 2 := recr (const 1) (comp mul (Fin.list [proj 2, proj 1]))
  comp pow' (Fin.list [proj 1, proj 0])

[Rui Liu]

Also any suggestion on simplifying the code would be great!

[Aaron Liu]

I see you have written

/-
 - mod(0, y) = 0
 - mod(x', y) = sub(mod(x, y)', y)
 -/

Then

mod(8,3)
= sub(mod(7,3)',3)
= sub(sub(mod(6,3)',3)',3)
= sub(sub(sub(mod(5,3)',3)',3)',3)
= sub(sub(sub(sub(mod(4,3)',3)',3)',3)',3)
= sub(sub(sub(sub(sub(mod(3,3)',3)',3)',3)',3)',3)
= sub(sub(sub(sub(sub(sub(mod(2,3)',3)',3)',3)',3)',3)',3)
= sub(sub(sub(sub(sub(sub(sub(mod(1,3)',3)',3)',3)',3)',3)',3)',3)
= sub(sub(sub(sub(sub(sub(sub(sub(mod(0,3)',3)',3)',3)',3)',3)',3)',3)',3)
= sub(sub(sub(sub(sub(sub(sub(sub(1,3)',3)',3)',3)',3)',3)',3)',3)
= sub(sub(sub(sub(sub(sub(sub(1,3)',3)',3)',3)',3)',3)',3)
= sub(sub(sub(sub(sub(sub(1,3)',3)',3)',3)',3)',3)
= sub(sub(sub(sub(sub(1,3)',3)',3)',3)',3)
= sub(sub(sub(sub(1,3)',3)',3)',3)
= sub(sub(sub(1,3)',3)',3)
= sub(sub(1,3)',3)
= sub(1,3)
= 0

[Aaron Liu]

perhaps you actually want mod(x, y) = if x < y then 0 else mod(sub(x,y),y)'

[Aaron Liu]

I guess you'll have to special-case mod zero

[Rui Liu]

Ooops, thanks! Is there a way to let lean expand what you have done? Or did you do it manually?

[Rui Liu]

Ok I got this fixed, thanks @Aaron Liu

/-
 - sgn(0) = 0
 - sgn(x') = 1
 -/
def PrimRecFunc.sgn : PrimRecFunc 1 :=
  recr zero (const 1)

/-
 - sgn(0) = 1
 - sgn(x') = 0
 -/
def PrimRecFunc.sgn' : PrimRecFunc 1 :=
  recr (const 1) zero

/-
 - cond(c, x, y) = sgn(c) * x + sgn'(c) * y
 -/
def PrimRecFunc.cond : PrimRecFunc 3 :=
  comp add (Fin.list [comp mul (Fin.list [comp sgn (Fin.list [proj 0]), proj 1]),
                      comp mul (Fin.list [comp sgn' (Fin.list [proj 0]), proj 2])])

/-
 - eq(x, y) = sgn'((x - y) + (y - x))
 -/
def PrimRecFunc.eq : PrimRecFunc 2 :=
  comp sgn' (Fin.list [comp add (Fin.list [comp sub (Fin.list [proj 0, proj 1]),
                                           comp sub (Fin.list [proj 1, proj 0])])])

/-
 - mod(0, y) = 0
 - mod(x', y) = if mod(x, y)' = y then 0 else mod(x, y)'
 -/
def PrimRecFunc.mod : PrimRecFunc 2 :=
  let r' : PrimRecFunc 3 := comp succ (Fin.list [proj 1])
  recr zero (comp cond (Fin.list [comp eq (Fin.list [r', proj 2]), zero, r']))

[Rui Liu]

Any idea how to simplify the code? Ideally I'd like to get rid of the (Fin.list [...]) part :sweat_smile:

[Aaron Liu]

Well mathlib provides a ![a, b, c] notation for fin-vectors

[Aaron Liu]

it expands to Matrix.vecCons a (Matrix.vecCons b (Matrix.vecCons c Matrix.vecEmpty))

[Rui Liu]

That's great! Thanks for the tip!

[Matt Diamond]

@Rui Liu are you aware of Nat.Primrec? I assume you're building this from scratch on purpose but just figured I would mention it

[Rui Liu]

@Matt Diamond I'm not aware of that :sweat_smile: , that said, it's for my own learning so it would still be interested to build that myself. Thanks for mentioning!

[Rui Liu]

It's a bit different from what I built though. I build a N^k -> N prim recursive function, also the library one is defined as N -> N -> Prop, not sure whether that's handy to use when there's no type for the N -> N part...?

[Dexin Zhang]

There is a docs#Nat.Primrec' for N^k to N. Though the biggest difference is that docs#Nat.Primrec and docs#Nat.Primrec' are Prop, not Type...

[Rui Liu]

Curious is there a library definition of a general recursive function?

[Matt Diamond]

sure... docs#Nat.Partrec

[Matt Diamond]

there's also docs#Computable for computable functions

[Matt Diamond]

also note that there's docs#Primrec and docs#Partrec which utilize encoding/decoding to model primitive and partial recursive functions of types beyond the natural numbers

[Matt Diamond]

also take note of docs#Nat.Partrec.Code and docs#Nat.Partrec.Code.eval ... there's a lot of good stuff in the Computability library :slight_smile:

[Rui Liu]

With Nat.Primrec definition, how do you get the actual zero / succ / proj functions?

[Rui Liu]

I mean getting the function itself, instead of just the proof of the function being prim recursive ...?

[Matt Diamond]

as @Dexin Zhang mentioned, these are Prop-valued, which means the function is distinct from the proof that it's primitive recursive... so in a proof you'll have a function f : ℕ → ℕ along with hf : Nat.Primrec f

[Matt Diamond]

Nat.Partrec.Code and Nat.Partrec.Code.eval are closer to the way you've defined things, but that's for partial recursive functions

[Rui Liu]

So I guess the inductive type as defined doesn't give you the function? I will need to define my own separate zero function, then prove it's primitive recursive?

[Rui Liu]

Hmm.... this doesn't seem to work...? Is this something closer to what it should do?

inductive PrimRec : ∀ {n : ℕ}, (Vector ℕ n → ℕ) → Prop
  | zero : PrimRec (λ _ => 0)


def zero {n : ℕ} : Vector ℕ n → ℕ :=
  λ _ => 0

#check PrimRec.zero zero -- fail to type check?

[Matt Diamond]

in your case, the statement would be:

example (n : ℕ) : @PrimRec n zero := PrimRec.zero

[Matt Diamond]

it's a proof that zero is PrimRec, using your inductive type

[Rui Liu]

Thanks, would it be possible to have something that build the function up and the proof of the function being prim recursive at the same time? It's like two strands of things at the same time....?

[Matt Diamond]

do you mean your original approach with codes and eval? or something different?

[Rui Liu]

Something different... the eval approach has the drawback that you need to call that to get the function, ...and you don't have the proof object as a nice Prop. Ideally the function is just a plain lambda, and we get a separate proof object. However, we should be able to build both at the same time.

So I'm imagine something like...

(zero_func, zero_func_proof)
| succ
(succ_func, succ_func_proof)
| ...

[Rui Liu]

Maybe a structure?

[Matt Diamond]

in theory you could do something like this, where Lean figures out the function for you:

import Mathlib

def PrimRecFunc : Type := { f // Nat.Primrec f }

instance : FunLike PrimRecFunc ℕ ℕ :=
⟨Subtype.val, Subtype.val_injective⟩

def succFunction : PrimRecFunc :=
⟨_, Nat.Primrec.succ⟩

#eval succFunction 10

[Matt Diamond]

then you could define a bunch of functions like that for each of the constructors

[Rui Liu]

Hmmm.... this is a bit beyond my knowledge, I'm quite new to this tool :sweat_smile:

[Rui Liu]

structure PrimRecFunc {n : Nat} where
    func : Vector Nat n -> Nat
    proof : PrimRec func

Does something like this makes any sense?

[Matt Diamond]

yes, though that's similar to a Subtype, which was what I was constructing above (docs#Subtype)

[Rui Liu]

I will have a look, thanks!

[Rui Liu]

Hmmm... I now have the following definition, but don't know how to define the comp and recr case:

def ℕs (n : ℕ) := Fin n → ℕ

inductive PrimRec : ∀ {n : ℕ}, (ℕs n → ℕ) → Prop
  | zero : PrimRec (λ _ => 0)
  | succ : PrimRec (λ (xs : ℕs 1) => (xs 0).succ)
  | proj (i : Fin n) : PrimRec λ xs => xs i
  | comp {m : ℕ} (f : ℕs m → ℕ) (gs : Fin m → ℕs n → ℕ) :
      PrimRec f →
      (∀ i, PrimRec (gs i)) →
      PrimRec (λ xs => f (λ i => gs i xs))
  | recr (f : ℕs n → ℕ) (g : ℕs (n+2) → ℕ) :
      PrimRec f →
      PrimRec g →
      PrimRec (λ xs =>
        let x := xs 0
        let xs' := Fin.tail xs
        x.rec (f xs') (λ c r => g (Fin.cons c (Fin.cons r xs')))
      )

def PrimRecFn (n : ℕ) := {f : ℕs n → ℕ // PrimRec f}

def PrimRecFn.zero {n : ℕ} : PrimRecFn n :=
  ⟨_, PrimRec.zero⟩

def PrimRecFn.succ : PrimRecFn 1 :=
  ⟨_, PrimRec.succ⟩

def PrimRecFn.proj {n : ℕ} (i : Fin n) : PrimRecFn n :=
  ⟨_, PrimRec.proj i⟩

def PrimRecFn.comp {n m : ℕ} (f : PrimRecFn m) (gs : Fin m → PrimRecFn n) : PrimRecFn n :=
  ⟨λ xs => f.val (λ i => (gs i).val xs), PrimRec.comp f.property (λ i => (gs i).property)⟩  --- Doesn't work

Why is that not working?

[Matt Diamond]

The problem is that you're missing the first two arguments to PrimRec.comp (f and gs). You can either pass them in (underscores will work) or you can make them implicit in the definition, like this:

import Mathlib

def ℕs (n : ℕ) := Fin n → ℕ

inductive PrimRec : ∀ {n : ℕ}, (ℕs n → ℕ) → Prop
  | zero : PrimRec (λ _ => 0)
  | succ : PrimRec (λ (xs : ℕs 1) => (xs 0).succ)
  | proj {n} (i : Fin n) : PrimRec λ xs => xs i
  | comp {n} {m : ℕ} {f : ℕs m → ℕ} {gs : Fin m → ℕs n → ℕ} :
      PrimRec f →
      (∀ i, PrimRec (gs i)) →
      PrimRec (λ xs => f (λ i => gs i xs))
  | recr {n} (f : ℕs n → ℕ) (g : ℕs (n+2) → ℕ) :
      PrimRec f →
      PrimRec g →
      PrimRec (λ xs =>
        let x := xs 0
        let xs' := Fin.tail xs
        x.rec (f xs') (λ c r => g (Fin.cons c (Fin.cons r xs')))
      )

def PrimRecFn (n : ℕ) := {f : ℕs n → ℕ // PrimRec f}

def PrimRecFn.zero {n : ℕ} : PrimRecFn n :=
  ⟨_, PrimRec.zero⟩

def PrimRecFn.succ : PrimRecFn 1 :=
  ⟨_, PrimRec.succ⟩

def PrimRecFn.proj {n : ℕ} (i : Fin n) : PrimRecFn n :=
  ⟨_, PrimRec.proj i⟩

def PrimRecFn.comp {n m : ℕ} (f : PrimRecFn m) (gs : Fin m → PrimRecFn n) : PrimRecFn n :=
  ⟨_, PrimRec.comp f.property (λ i => (gs i).property)⟩

[Matt Diamond]

Implicit probably makes the most sense since they're already determined by the arguments that follow

[Matt Diamond]

that's also how docs#Nat.Primrec.comp is defined, with implicit function arguments

[Matt Diamond]

I would do the same for recr

[Rui Liu]

I got it implemented now, thanks! Another quick question, what's the difference between the argument before colon and after colon? For example:

def PrimRecFn.proj {n : ℕ} (i : Fin n) : PrimRecFn n :=
  ⟨_, PrimRec.proj i⟩

Why not write it as:

def PrimRecFn.proj {n : ℕ} : Fin n -> PrimRecFn n :=
  λ i => ⟨_, PrimRec.proj i⟩

[Rui Liu]

For example why the inductive type is defined as such?

inductive PrimRec : ∀ {n : ℕ}, (ℕs n → ℕ) → Prop

Why not

-- This doesn't work on the succ case, but I'm just curious what difference it makes here.
inductive PrimRec {n : ℕ} : (ℕs n → ℕ) → Prop

[Aaron Liu]

for inductives the left of the colon is always paramenters (free variable in every constructor) and the right can be indices (constructors can set it to anything)

[Rui Liu]

Ok thanks!