Encoding FStar-like sets axiomatically

Stream: new members

[Pranav cs22b015]

Is there an approach in lean to define sets axiomatically / inductively? The definition I have in mind is close to the FStar implementation. I want to use such a definition to help SMT solvers such as Lean-Auto to solve complex problems related to sets, which the standard set definition in Lean struggles to offer. In Fstar, this is possible by defining certain SMT Patterns. Is there something similar to lean, where E-matching expressions can be given to tools such as auto and grind ?

[Aaron Liu]

Pranav cs22b015 said:

Is there an approach in lean to define sets axiomatically / inductively?

Can you clarify this?

[Pranav cs22b015]

Basically a definition without an underlying data structure - you can refer to the Fstar definition given above

[Aaron Liu]

sorry I don't know fstar

[Aaron Liu]

what do you mean "without an underlying data structure", is an underlying data structure bad?

[Aaron Liu]

sets in mathlib don't carry any "data" in compiled code

[Henrik Böving]

The definition in fstar seems to be a function a -> Bool to me isn't it? That's almost the same definition as in Lean except that we have a -> Prop. The particular definitions of intersection etc. also don't seem to be different to me.

[Henrik Böving]

Is there something similar to lean, where E-matching expressions can be given to tools such as auto and grind ?

Re this, I can't speak for auto but I would suggest reading the grind manual here

[Pranav cs22b015]

Aaron Liu said:

what do you mean "without an underlying data structure", is an underlying data structure bad?

I mean it in the sense of it being harder for SMT solvers to reason about

[Pranav cs22b015]

Henrik Böving said:

The definition in fstar seems to be a function a -> Bool to me isn't it? That's almost the same definition as in Lean except that we have a -> Prop. The particular definitions of intersection etc. also don't seem to be different to me.

Also, could you direct me to the lean definitions?

[Ilmārs Cīrulis]

That should be here: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Defs.html#Set

[Ilmārs Cīrulis]

For example, https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Defs.html#Set.union - and there click on "Equations"