Functional way to check if a value appears in the image

Stream: new members

[Nick Pilotti]

To get some practice with Lean I am trying to write some of the basic definitions of model theory. I have defined a term and I am trying to write a function that returns whether a particular variable occurs in a term. To to this I will need to recursively call the function on the list of terms that follow a function symbol. What would be the most concise functional way to implement something like this with the way I have defined things?

inductive term
| var : ℕ → term
| cnst : L.const → term
| func (n : ℕ) : L.functions n → (fin n → term) → term

/-- If a variable occurs in a term -/
def occurs_in_term : ℕ → term L → bool
| n (var m) := if n = m then true else false
| _ (cnst c) := false
| _ (func _ _ t) := -- TODO: Want to check true for something in range the range of t

[Mario Carneiro]

#backticks

[Mario Carneiro]

#mwe

[Mario Carneiro]

import data.nat.basic

def sig : Type := sorry
variable (L : sig)
def sig.const : sig → Type := sorry
def sig.functions : sig → ℕ → Type := sorry

inductive term
| var : ℕ → term
| cnst : L.const → term
| func (n : ℕ) : L.functions n → (fin n → term) → term
open term

/-- If a variable occurs in a term -/
def occurs_in_term (x : ℕ) : term L → bool
| (var m) := if x = m then true else false
| (cnst c) := false
| (func n _ t) := to_bool $ ∀ i, occurs_in_term (t i)

[Mario Carneiro]

@Nick Pilotti

[Nick Pilotti]

(deleted)

[Nick Pilotti]

Thank you, can you explain the meaning of to_bool $ ?

[Nick Pilotti]

open data.nat.basic

/-- Def 1.2.1. -/
structure language :=
(functions : ℕ → set char) (relations : ℕ → set char)

namespace language

/-- The type of constants in a given language. -/
@[nolint has_inhabited_instance] def const (L : language) := L.functions 0

/-- The language of number theory -/
def L_NT : language :=
  ⟨λ n,
  if      n = 0 then {'0'}
  else if n = 1 then {'S'}
  else if n = 2 then {'+', '⬝', 'E'}
  else {},
  λ n,
  if      n = 2 then {'<'}
  else {}⟩

def var : term L_NT := func 2 '+' (var 0) (cnst '0')

[Nick Pilotti]

I'm having another problem. Here I am trying to define a term but I get the error :

type mismatch at application
  func 2 '+'
term
  '+'
has type
  char
but is expected to have type
  ↥(?m_1.functions 2)

[Ruben Van de Velde]

$ is function application with low precedence, so these lines are equivalent:

| (func n _ t) := to_bool $ ∀ i, occurs_in_term (t i)
| (func n _ t) := to_bool (∀ i, occurs_in_term (t i))

[Nick Pilotti]

Thanks, and to_bool will convert a Prop into a bool I'm assuming? Does Lean compute this by iterating over all of the possible values of i?

[Mario Carneiro]

Yes. There is a decidability instance that says that if \forall i : fin n, decidable (f i) then decidable (\forall i : fin n, f i), and it works by iterating over all the elements of fin n

[Mario Carneiro]

the to_bool uses that decidability instance to turn the proposition into a bool

[Mario Carneiro]

docs#nat.decidable_forall_fin

[Nick Pilotti]

Oh ok, I think I can see what decidable means now.

[Mario Carneiro]

Oops, except this is not correct for the given definition since you are looking for any occurrence; it should use \exists instead of \forall

[Nick Pilotti]

So in the forall case it will be decidable only if the domain in finite?

[Mario Carneiro]

there is another decidability instance for that, of course

[Mario Carneiro]

Yes

[Nick Pilotti]

Good catch thanks

[Mario Carneiro]

Well in some cases it might be decidable for other reasons, for example divisibility of integers is defined using an unbounded existential but it is still decidable because of the theorem a | b <-> b % a = 0

[Nick Pilotti]

But decidable essentially means that is an instance somewhere which defines an algorithm to computer the answer? Something like that?

[Nick Pilotti]

So in the case of divisibility the algorithm would be division with remainder

[Nick Pilotti]

And forall would be to iterate through all the finite possibilities

[Mario Carneiro]

right

[Nick Pilotti]

Thanks for the help, I knew there had to be an elegant way to do this without having to write a for loop

[Nick Pilotti]

Can I get help on why this gives a type error as well?

/-- Def 1.2.1. -/
structure language :=
(functions : ℕ → set char) (relations : ℕ → set char)

namespace language

/-- The type of constants in a given language. -/
@[nolint has_inhabited_instance] def const (L : language) := L.functions 0

/-- The language of number theory -/
def L_NT : language :=
  ⟨λ n,
  if      n = 0 then {'0'}
  else if n = 1 then {'S'}
  else if n = 2 then {'+', '⬝', 'E'}
  else {},
  λ n,
  if      n = 2 then {'<'}
  else {}⟩

def var : term L_NT := func 2 '+' (var 0) (cnst '0')

[Mario Carneiro]

to be fair, there is a for loop (ish) involved, it's just buried in a library

[Nick Pilotti]

right, I just didn't have to write one myself

[Mario Carneiro]

again, see #mwe

[Nick Pilotti]

sorry

[Mario Carneiro]

your example is not self contained so I don't know what error you are talking about

[Nick Pilotti]

yes thank you, i forgot to include the definition of term

[Mario Carneiro]

The definition of L_NT is not going to compute very well, which means that you probably won't be able to write things like cnst '0'

[Mario Carneiro]

if I had to guess I think you should be writing cnst \<'0', _\> where _ is a proof that '0' \in L_NT 0

[Mario Carneiro]

which is probably by simp [L_NT]

[Mario Carneiro]

same for the '+'

[Nick Pilotti]

import data.nat.basic

namespace first_order

structure language :=
(functions : ℕ → set char) (relations : ℕ → set char)

namespace language

/-- The type of constants in a given language. -/
def const (L : language) := L.functions 0

/-- The language of number theory -/
def L_NT : language :=
  ⟨λ n,
  if      n = 0 then {'0'}
  else if n = 1 then {'S'}
  else if n = 2 then {'+', '⬝', 'E'}
  else {},
  λ n,
  if      n = 2 then {'<'}
  else {}⟩

variable (L : language)

/-- Def 1.3.1. -/
inductive term
| var           : ℕ → term
| cnst          : L.const → term
| func (n : ℕ)  : L.functions n → (fin n → term) → term

open term

def var : term L_NT := cnst '0'

end language

end first_order

[Mario Carneiro]

import data.matrix.notation
...
def var : term L_NT :=
func 2 ⟨'+', by norm_num [L_NT]⟩
  ![var 0, cnst ⟨'0', by simp [L_NT, const]⟩]

[Mario Carneiro]

If I were you I would define zero, add etc to make this nicer

[Mario Carneiro]

instance : has_zero (term L_NT) := ⟨cnst ⟨'0', by simp [L_NT, const]⟩⟩
def succ (x : term L_NT) : term L_NT := func 1 ⟨'S', by norm_num [L_NT]⟩ ![x]
instance : has_add (term L_NT) := ⟨λ x y, func 2 ⟨'+', by norm_num [L_NT]⟩ ![x, y]⟩
instance : has_mul (term L_NT) := ⟨λ x y, func 2 ⟨'⬝', by norm_num [L_NT]⟩ ![x, y]⟩
instance : has_pow (term L_NT) (term L_NT) := ⟨λ x y, func 2 ⟨'E', by norm_num [L_NT]⟩ ![x, y]⟩

def var : term L_NT := var 0 + 0

[Nick Pilotti]

I see, thank you

[Nick Pilotti]

What purpose does norm_num serve here?

[Mario Carneiro]

It is like simp, but it also knows how to solve equations involving numerals like 2 = 0 <-> false which come up when reducing your if statement definition

[Mario Carneiro]

If you used a match then I think simp alone would get it

[Nick Pilotti]

Ok got it

[Nick Pilotti]

So basically what lean expects is an element and then a proof that element is of the correct type?

[Nick Pilotti]

Is that what the notation ↥ means?

[Mario Carneiro]

This happens because when you wrote L.const → term , that doesn't immediately typecheck because L.const is a set, not a type

[Mario Carneiro]

it gets promoted ("coerced") to a type using subtype

[Mario Carneiro]

which is the type of pairs of an element x and a proof h : x \in A

[Nick Pilotti]

So is a set char really just a subtype of char?

[Mario Carneiro]

it is the collection of all predicates on char

[Mario Carneiro]

like the powerset

[Mario Carneiro]

er, that's the type itself

[Mario Carneiro]

an element of the type is some particular predicate on char

[Mario Carneiro]

and to apply the predicate on a particular element you write x \in A

[Mario Carneiro]

so you could have also written that inductive without any coercions like this:

inductive term
| var           : ℕ → term
| cnst          : ∀ x, x ∈ L.const → term
| func (n : ℕ)  : ∀ x, x ∈ L.functions n → (fin n → term) → term

[Mario Carneiro]

and now cnst takes the arguments separately rather than as a pair

instance : has_zero (term L_NT) := ⟨cnst '0' (by simp [L_NT, const])⟩

[Nick Pilotti]

I see

[Mario Carneiro]

The more leanish way to do this would be to just have a bespoke inductive type family for L_NT.functions

[Nick Pilotti]

Can you show an example of that?

[Nick Pilotti]

I see now

def set (α : Type u) := α → Prop

[Mario Carneiro]

import data.matrix.notation

namespace first_order

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

namespace language

/-- The type of constants in a given language. -/
def const (L : language) := L.functions 0

inductive L_NT_func : ℕ → Type
| zero : L_NT_func 0
| succ : L_NT_func 1
| add : L_NT_func 2
| mul : L_NT_func 2
| exp : L_NT_func 2

inductive L_NT_rel : ℕ → Type
| lt : L_NT_rel 2

/-- The language of number theory -/
def L_NT : language :=
  ⟨L_NT_func, L_NT_rel⟩

variable (L : language)

/-- Def 1.3.1. -/
inductive term
| var           : ℕ → term
| cnst          : L.const → term
| func {n : ℕ}  : L.functions n → (fin n → term) → term

open term

instance : has_zero (term L_NT) := ⟨cnst L_NT_func.zero⟩
def succ (x : term L_NT) : term L_NT := func L_NT_func.succ ![x]
instance : has_add (term L_NT) := ⟨λ x y, func L_NT_func.add ![x, y]⟩
instance : has_mul (term L_NT) := ⟨λ x y, func L_NT_func.mul ![x, y]⟩
instance : has_pow (term L_NT) (term L_NT) := ⟨λ x y, func L_NT_func.exp ![x, y]⟩

def var : term L_NT := var 0 + 0

end language

end first_order

[Nick Pilotti]

That looks nicer, thanks again

[Mario Carneiro]

By the way, I would also remove the cnst constructor and make it a definition like this:

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

def term.cnst {L : language} (c : L.const) : L.term := term.func c ![]
open term

[Mario Carneiro]

Otherwise, you will have cnst '0' and func '0' ![] and they are distinct

[Nick Pilotti]

What does ![] mean here?

[Mario Carneiro]

I'm using the notation from data.matrix.notation which makes it easy to write fin n -> A functions as if they were arrays

[Mario Carneiro]

I'm using them in add, succ etc as well

[Nick Pilotti]

Ok