Zulip Chat Archive

Stream: new members

Topic: Expressing the size of structures in FOL


view this post on Zulip Alexandre Rademaker (Sep 10 2020 at 02:54):

In FOL we can express that a structure must have a size n for a given n. A template for produce such a sentence can be easily defined using n variables. Can we define a function in Lean to produce such sentence given a n?

view this post on Zulip Mario Carneiro (Sep 10 2020 at 03:27):

Yes, but you need a definition of what a formula is to start with

view this post on Zulip Alexandre Rademaker (Sep 10 2020 at 03:32):

you mean, define formula as an inductive type?

view this post on Zulip Mario Carneiro (Sep 10 2020 at 03:39):

Yes. Something like this:

import data.list.defs

inductive fmla
| true : fmla
| eq :     fmla
| not : fmla  fmla
| and : fmla  fmla  fmla
| all : fmla  fmla

def fmla.conj : list fmla  fmla := list.foldl fmla.and fmla.true

def at_least_n (n : ) : fmla :=
fmla.all^[n] $ fmla.conj $ do
  j  list.range n,
  i  list.range j,
  [(fmla.eq i j).not]

#reduce at_least_n 3

view this post on Zulip Kenny Lau (Sep 10 2020 at 06:11):

just read flypitch

view this post on Zulip Alexandre Rademaker (Sep 10 2020 at 13:54):

What is that?

view this post on Zulip Alexandre Rademaker (Sep 10 2020 at 13:57):

You are probably taking about https://flypitch.github.io/about/, right? My point is really much simpler. I am reacting to a student question on a want to procure FOL formulas from templates in Lean


Last updated: May 18 2021 at 16:25 UTC