model finding

Stream: Is there code for X?

[Nathan Temple]

Hello, I'm sure this must be a beginner question, but I'm looking for a way to find a set of numbers that satisfy a set of first-order sentences. For example, I would like to specify numbers called "prime" (although I know this has already been done) with these first order sentences:

X ∈ ℕ
2 ≤ X ≤ 10
∀ Y ( (Y ∈ ℕ ∧ Y | X) → (Y=1 ∨ Y=X) ) -- the only divisors of X are 1 and X

And I would like it to print out “X=2,3,5 or 7”

[Adam Topaz]

The way to define this (or sets in general) is to use set builder notation. Take a look in #tpil for more info. In this case, we do have docs#nat.primes

[Adam Topaz]

That's the subtype of prime numbers. If you look at the code, you will see { ... // ... }. Using { ... | ... } will give you the set instead.

[Patrick Massot]

Adam, I think you're missing the point. Nathan wants Lean to compute the elements

[Adam Topaz]

Oh I missed the "print" part of the question! Sorrry

[Patrick Massot]

In principle this is possible of course but this is totally not the focus of the immense majority of people here. You will probably have much more luck with people using Coq.

[Adam Topaz]

In principle you could use a stream to mimic the lazy list definition that haskell lets you write (using a sieve).

[Nathan Temple]

Thank you kindly. I guess I am looking for a convenient way to find 'Finite models'. I will look into Coq.

[Yaël Dillies]

In that case you can do #eval (finset.range 11).filter nat.prime.

[Nathan Temple]

Thank you, I realize now that I am looking for more of a 'Satisfiability Modulo Theories' solver of which Z3 is one.

[Kyle Miller]

@Nathan Temple Here's your example in Z3 in Python:

from z3 import *

s = Solver()

x = Int('x')

s.add(And(2 <= x, x <= 10))

y = Int('y')
s.add(ForAll([y], Implies(And(y >= 1, x % y == 0), Or(y == 1, y == x))))

vals = []
while s.check() == sat:
    vals.append(s.model()[x].as_long())
    s.add(x != s.model()[x])

print("X =", ",".join(str(v) for v in vals))
# X = 2,3,5,7

(No guarantees this is idiomatic; I've only used it a couple times.)