Proving a simple FOL syntax lemma

Stream: new members

[Jeremy Sorkin]

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]

unfold signature.formula.relation, simp will do it!

[Jeremy Sorkin]

Thanks a ton Eric!
I figured it was something super-simple but was absolutely stuck for hours.

[Bryan Gin-ge Chen]

You can usually combine unfold and simp: simp [signature.formula.relation] also works.