Stream: new members
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?
Mario Carneiro (Sep 10 2020 at 03:27):
Yes, but you need a definition of what a formula is to start with
Alexandre Rademaker (Sep 10 2020 at 03:32):
you mean, define formula as an inductive type?
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
Kenny Lau (Sep 10 2020 at 06:11):
just read flypitch
Alexandre Rademaker (Sep 10 2020 at 13:54):
What is that?
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