# Zulip Chat Archive

## Stream: new members

### Topic: Proving a simple FOL syntax lemma

#### Jeremy Sorkin (Apr 15 2021 at 15:47):

Hi everybody! My name is Jeremy Sorkin and I am a Math and Computer Science double major at the College of Wooster. I am very new to Lean, as I have only just started looking into it for a research project.

I have been trying to formalize some basic First-order Logic into Lean and was wondering if you guys could help me close a very trivial goal that I’ve been stuck on.

I’ve written a function `signature.formula.relation`

that takes as input a Natural number `n`

and FOL formula $\phi$ and returns the set of relational symbols of arity `n`

that occur in $\phi$:

```
def signature.formula.relation {σ : signature} (n : ℕ) : σ.formula → set (σ.nrary n)
| ( @signature.formula.relational σ n2 r v) :=
begin
by_cases h1 : n = n2,
rw h1,
exact insert r ∅,
exact ∅,
end
| ( signature.formula.for_all x φ) := φ.relation
| ( signature.formula.if_then φ ψ) := (φ.relation) ∪ (ψ.relation)
| ( signature.formula.equation t₁ t₂) := ∅
| signature.formula.false := ∅
```

I want to prove a very trivial result about my function which is: if I give it a formula of the form “r t1 t2 … tn” where r is a relational symbol of arity n and ti are all terms, then r is in the set signature.formula.relation (r t1 t2 … tn) n :

```
example {σ : signature} {α : Type u} [nonempty α]
(n : ℕ) (r : σ.nrary n) (v : fin n → σ.term)
: r ∈ signature.formula.relation n (signature.formula.relational r v) :=
begin
sorry,
end
```

It’s a really trivial result because, since r is a relational symbol of arity n it is by definition in the set signature.formula.relation (r t1 t2 … tn) n, however after a good couple hours I still haven’t been able to get anywhere.

Here is a minimum working example:

```
import data.set.lattice tactic.find tactic.tidy tactic.ring
universe u
namespace logic
open list tactic set
@[derive inhabited]
structure signature : Type (u+1) :=
(functional_symbol : Type u := pempty)
(relational_symbol : Type u := pempty)
(modality : Type u := pempty)
(vars : Type u := ulift ℕ)
(dec_vars : decidable_eq vars . apply_instance)
(arity : functional_symbol → ℕ := λ_, 0)
(rarity : relational_symbol → ℕ := λ_, 0)
(marity : modality → ℕ := λ_, 0)
-- the type of functional symbols of arity n
def signature.nary (σ : signature) (n : ℕ) := subtype {f : σ.functional_symbol | σ.arity f = n}
-- the type of relational symbols of arity n
def signature.nrary (σ : signature) (n : ℕ) := subtype {r : σ.relational_symbol | σ.rarity r = n}
inductive signature.term (σ : signature)
| var : σ.vars → signature.term
| app {n : ℕ} (f : σ.nary n) (v : fin n → signature.term) : signature.term
inductive signature.formula (σ : signature)
| relational {n : ℕ} (r : σ.nrary n) (v : fin n → σ.term) : signature.formula
| for_all : σ.vars → signature.formula → signature.formula
| if_then : signature.formula → signature.formula → signature.formula
| equation (t₁ t₂ : σ.term) : signature.formula
| false : signature.formula
def signature.formula.relation {σ : signature} (n : ℕ) : σ.formula → set (σ.nrary n)
| ( @signature.formula.relational σ n2 r v) :=
begin
by_cases h1 : n = n2,
rw h1,
exact insert r ∅,
exact ∅,
end
| ( signature.formula.for_all x φ) := φ.relation
| ( signature.formula.if_then φ ψ) := (φ.relation) ∪ (ψ.relation)
| ( signature.formula.equation t₁ t₂) := ∅
| signature.formula.false := ∅
example {σ : signature} {α : Type u} [nonempty α]
(n : ℕ) (r : σ.nrary n) (v : fin n → σ.term)
: r ∈ signature.formula.relation n (signature.formula.relational r v) :=
begin
sorry,
end
end logic
```

Thanks again guys!

#### Eric Rodriguez (Apr 15 2021 at 16:00):

`unfold signature.formula.relation, simp`

will do it!

#### Jeremy Sorkin (Apr 15 2021 at 16:22):

Thanks a ton Eric!

I figured it was something super-simple but was absolutely stuck for hours.

#### Bryan Gin-ge Chen (Apr 15 2021 at 16:45):

You can usually combine `unfold`

and `simp`

: `simp [signature.formula.relation]`

also works.

Last updated: May 14 2021 at 06:16 UTC