Zulip Chat Archive

Stream: new members

Topic: Proving a simple FOL syntax lemma


view this post on Zulip 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!

view this post on Zulip Eric Rodriguez (Apr 15 2021 at 16:00):

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

view this post on Zulip 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.

view this post on Zulip 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