How to define a term assignment function

Stream: new members

[Nick Pilotti]

My goal is to write some of model theory in Lean to get practice with the language. I am stuck trying to define a term assignment function, which is supposed to convert a term in a language into an element of some universe that is picked out by a structure. Here is what I've tried which does not compile and I'm not sure why.

structure language :=
(functions : ℕ → Type) (relations : ℕ → Type)

variable L : language

inductive term
| var           : ℕ → term
| func {n : ℕ}  : L.functions n → (fin n → term) → term

inductive formula
| eq          : term L → term L → formula
| rel {n : ℕ} : L.relations n → (fin n → term L) → formula
| neg         : formula → formula
| or          : formula → formula → formula
| all         : ℕ → formula → formula

variables (A : Type*) (iA : inhabited A)

/-- An L-structure -/
structure Structure [inhabited A] :=
(functions : Π {n : ℕ}, L.functions n → (fin n → A) → A)
(relations : Π {n : ℕ}, L.relations n → (fin n → A) → Prop)

variable 𝔸 : Structure L A

/-- Variable assignment function into A -/
def var_assign := ℕ → A

/-- Term assignment function -/
def term_assign := term L → A

set_option trace.eqn_compiler.elim_match true

/-- Term assignment function induced by s -/
/-- Doesn't compile -/
def term_assign_of_s (s : var_assign A) : term L → A :=
  λ t : term L,
  match t with
  | (var n)               := s n
  | (func n fsymb args)   := (𝔸.functions n fsymb) (term_assign_of_s ∘ args)
  end

[Alex J. Best]

I got a compiling version, but couldn't get it non-meta (ie. lean doesn't see why this terminates without help/rearanging)

structure language :=
(functions : ℕ → Type) (relations : ℕ → Type)

variable L : language

inductive term
| var           : ℕ → term
| func    {n : ℕ} : L.functions n → (fin n → term) → term

inductive formula
| eq          : term L → term L → formula
| rel {n : ℕ} : L.relations n → (fin n → term L) → formula
| neg         : formula → formula
| or          : formula → formula → formula
| all         : ℕ → formula → formula

variables (A : Type*) (iA : inhabited A)

/-- An L-structure -/
structure Structure [inhabited A] :=
(functions : Π {n : ℕ}, L.functions n → (fin n → A) → A)
(relations : Π {n : ℕ}, L.relations n → (fin n → A) → Prop)

variable 𝔸 : Structure L A

/-- Variable assignment function into A -/
def var_assign := ℕ → A

/-- Term assignment function -/
def term_assign := term L → A

set_option trace.eqn_compiler.elim_match true

meta def term_assign_of_s (s : var_assign A) : term L → A
| (term.var n)               := s n
| (term.func fsymb args)   := 𝔸.functions fsymb (term_assign_of_s ∘ args)

[Nick Pilotti]

What is meta doing here?

[Alex J. Best]

Its telling lean not to try and check that the recursion halts.

[Alex J. Best]

So its not really ideal to prove things about, but hopefully you can see the syntax changes to get the function defined at least

[Alex J. Best]

If you remove it you'll see the error message, maybe check out https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Unexpected.20occurence.20of.20recursive.20function/near/243769927

[Eric Wieser]

This works without meta:

def term_assign_of_s (s : var_assign A) : term L → A
| (term.var n)               := s n
| (term.func fsymb args)   := 𝔸.functions fsymb (λ x, term_assign_of_s (args x))

[Eric Wieser]

The equation compiler can't see through ∘

[Eric Wieser]

Or phrased in terms of the error message, it does not expect to see recursive functions without their full argument list

[Nick Pilotti]

Thank you. What is the reason you don't need to write a lambda function for matching on the term?

[Eric Wieser]

The rule is just that you're not allowed to have term_assign_of_s in the RHS unless it's of the form term_assign_of_s x

[Eric Wieser]

I don't understand your question

[Nick Pilotti]

I'm asking why don't I need to do this

def term_assign_of_s (s : var_assign A) : term L → A :=
  λ t : term L,
  match t with
  | (term.var n)               := s n
  | (term.func fsymb args)     := 𝔸.functions fsymb (λ x, term_assign_of_s (args x))
  end

[Mario Carneiro]

the syntax for def-match acts like a lambda followed by a match. What you wrote is mostly equivalent, except that for writing recursive functions the def-match syntax is mandatory

[Mario Carneiro]

by def-match I mean def foo (params...) : type | ... instead of def foo (params...) : type := ...

[Nick Pilotti]

Got it thanks

[Nick Pilotti]

I have another question. How can I overload syntax for formula without Lean getting confused with Prop. For example here I have overloaded = and Lean thinks that I have formula even though I want to be a Prop

structure language :=
(functions : ℕ → Type) (relations : ℕ → Type)

variable (L : language)

inductive term
| var           : ℕ → term
| func {n : ℕ}  : L.functions n → (fin n → term) → term

inductive formula
| eq          : term L → term L → formula
| rel {n : ℕ} : L.relations n → (fin n → term L) → formula
| neg         : formula → formula
| or          : formula → formula → formula
| all         : ℕ → formula → formula

infix ` = `:88   := formula.eq

open term
open formula

def occurs_in_term (n : ℕ) : term L → bool
| (var m)      := to_bool (n = m) /-- Lean thinks this is a formula when it should be a Prop -/
| (func _ t)   := to_bool $ ∃ i, occurs_in_term (t i)

[Mario Carneiro]

The general recommendation is to not do this. Use local notations and don't overload notations you want to use normally

[Mario Carneiro]

Lean 4 is much better at this kind of thing

[Nick Pilotti]

So just come up with different notation is what you're saying?

[Mario Carneiro]

yes

[Nick Pilotti]

Another notation related question

[Nick Pilotti]

Let's say I want to have something like v₁ recognized as the term var 1. Is there a way to do this with notation?

[Mario Carneiro]

notation `v` := var 1

[Mario Carneiro]

or even just def v := var 1

[Mario Carneiro]

you will probably want to scope it

[Nick Pilotti]

Is there any way to make it so that 1 is in the subscript?

[Nick Pilotti]

I'm guessing probably not

[Mario Carneiro]

you can make def v₁ := var 1 or notation `v₁` := var 1 just the same

[Mario Carneiro]

you will have to repeat this for any other subscripts you want to use but generally you won't need more than 0-3 or so

[Nick Pilotti]

Oh that makes sense

[Nick Pilotti]

Thanks once again

[Nick Pilotti]

How would one define an example of a Structure with this definition? Here I am trying to give an interpretation to the language of number theory and I have defined the meaning of functions with a specific number of arguments but I am having trouble putting it together at the end

structure language :=
(functions : ℕ → Type) (relations : ℕ → Type)

/-- The language of number theory -/
inductive NT_func : ℕ → Type
| zero : NT_func 0
| succ : NT_func 1
| add : NT_func 2
| mul : NT_func 2

inductive NT_rel : ℕ → Type
| lt : NT_rel 2

def NT : language :=
  ⟨NT_func, NT_rel⟩

variables (L : language) (A : Type*)

structure Structure [inhabited A] :=
(functions : Π {n : ℕ}, L.functions n → (fin n → A) → A)
(relations : Π {n : ℕ}, L.relations n → (fin n → A) → Prop)

def NT_func_zero : NT.functions 0 → (fin 0 → ℕ) → ℕ
| NT_func.zero n   := 0

def NT_func_one : NT.functions 1 → (fin 1 → ℕ) → ℕ
| NT_func.succ n   := (n 0) + 1

def NT_func_two : NT.functions 2 → (fin 2 → ℕ) → ℕ
| NT_func.add args := (args 0) + (args 1)
| NT_func.mul args := (args 0) * (args 1)

def NT_struct_func : Π {n : ℕ}, NT.functions n → (fin n → ℕ) → ℕ :=

[Mario Carneiro]

I would get rid of NT_func_zero, NT_func_one and NT_func_two and structure it like this:

def NT_struct_func : Π {n : ℕ}, NT.functions n → (fin n → ℕ) → ℕ
| _ NT_func.zero n   := 0
| _ NT_func.succ n   := (n 0) + 1
| _ NT_func.add args := (args 0) + (args 1)
| _ NT_func.mul args := (args 0) * (args 1)

[Nick Pilotti]

I was trying something like that originally but I was having trouble getting it to work. So the purpose of the first _ is to pattern match on the int part? Does that determine the value of the implicit parameter n?

[Nick Pilotti]

Also is there a reason Lean can't seem to find an exponentiation operator for Nat?

structure language :=
(functions : ℕ → Type) (relations : ℕ → Type)

/-- The language of number theory -/
inductive NT_func : ℕ → Type
| zero : NT_func 0
| succ : NT_func 1
| add : NT_func 2
| mul : NT_func 2
| exp : NT_func 2

inductive NT_rel : ℕ → Type
| lt : NT_rel 2

def NT : language :=
  ⟨NT_func, NT_rel⟩

variables (L : language) (A : Type*)

structure Structure [inhabited A] :=
(functions : Π {n : ℕ}, L.functions n → (fin n → A) → A)
(relations : Π {n : ℕ}, L.relations n → (fin n → A) → Prop)

def NT_struct_func : Π {n : ℕ}, NT.functions n → (fin n → ℕ) → ℕ
| _ NT_func.zero n   := 0
| _ NT_func.succ n   := (n 0) + 1
| _ NT_func.add args := (args 0) + (args 1)
| _ NT_func.mul args := (args 0) * (args 1)
| _ NT_func.exp args := (args 0) ^ (args 1)

[Mario Carneiro]

It's not pattern matching on the int exactly; it's an "inaccessible parameter"

[Mario Carneiro]

which means it has to be in the pattern match but its value is determined by the other parameters

[Mario Carneiro]

You need to import algebra.group_power to get exponentiation

[Nick Pilotti]

So without marking the existence of an inaccessible parameter with _ Lean will just assume that n is still just a variable?

[Mario Carneiro]

You need to put something there since the pattern match has three arguments

[Mario Carneiro]

you can also put .(0) in the first case if you want to be specific about the value that lean is inferring it to

[Nick Pilotti]

Ok got it, thanks

[Mario Carneiro]

the . is to say that we aren't pattern matching on the nat

[Mario Carneiro]

but you will almost never see that syntax used because _ always works in its place

[Nick Pilotti]

What is the reason for this type error?

import algebra.group_power

structure language :=
(functions : ℕ → Type) (relations : ℕ → Type)

/-- The language of number theory -/
inductive NT_func : ℕ → Type
| zero : NT_func 0
| succ : NT_func 1
| add : NT_func 2
| mul : NT_func 2
| exp : NT_func 2

inductive NT_rel : ℕ → Type
| lt : NT_rel 2

def NT : language :=
  ⟨NT_func, NT_rel⟩

variables (L : language) (A : Type*)

structure Structure [inhabited A] :=
(functions : Π {n : ℕ}, L.functions n → (fin n → A) → A)
(relations : Π {n : ℕ}, L.relations n → (fin n → A) → Prop)

/-- The usual intepretation of Number Theory -/
def NT_struct_func : Π {n : ℕ}, NT.functions n → (fin n → ℕ) → ℕ
| _ NT_func.zero n   := 0
| _ NT_func.succ n   := (n 0) + 1
| _ NT_func.add args := (args 0) + (args 1)
| _ NT_func.mul args := (args 0) * (args 1)
| _ NT_func.exp args := (args 0) ^ (args 1)

def NT_struct_rel : Π {n : ℕ}, NT.relations n → (fin n → ℕ) → Prop
| _ NT_rel.lt args   := (args 0) < (args 1)

def NT_struct : Structure NT ℕ :=
  ⟨NT_struct_func, NT_struct_rel⟩

[Nick Pilotti]

type mismatch at application
  Structure.mk NT_struct_func
term
  NT_struct_func
has type
  NT.functions ?m_1 → (fin ?m_1 → ℕ) → ℕ
but is expected to have type
  Π {n : ℕ}, NT.functions n → (fin n → ℕ) → ℕLean

[Nick Pilotti]

I would have thought there was no difference between these two types

[Nick Pilotti]

If I make n explicit it goes away

[Mario Carneiro]

This is how implicit arguments work. When you write NT_struct_func lean automatically inserts a _ for the implicit argument n here, resulting in @NT_struct_func _ which doesn't match the type expected by NT_struct.

[Mario Carneiro]

You can fix this by making the argument explicit like you did, or by using a "semi-implicit" binder {{n : nat}}, which acts like an implicit argument only if you supply the argument coming after n (here the relation), or by writing @NT_struct_func in NT_struct

[Nick Pilotti]

How would write an instance of has_repr for this?

structure language :=
(functions : ℕ → Type) (relations : ℕ → Type)

variable L : language

inductive term
| var           : ℕ → term
| func {n : ℕ}  : L.functions n → (fin n → term) → term

open term

instance : has_repr (term L) :=
⟨λ t,
match t with
| (var n)             := "v" ++ repr (n)
| (func fsymb args)   := (repr fsymb) ++ (repr args)
end⟩
end⟩