Printing a Finset

Stream: Is there code for X?

[Dhruv Chaurasiya]

Hi,
I have started learning theorem proving in Lean as a part of my coursework. I have a type X which is an abbreviation to Lean.Name

I also have a Finset X (Finset of type X), where Finset is as defined in Mathlib.Data.Basic.Finset

I am looking for a method to print this finset, and send the contents of this finset to a out.txt file.

[Kenny Lau]

import Mathlib

def myFinset : Finset ℕ :=
  (Finset.range 10).image (· ^ 2)

#eval myFinset
-- outputs: {0, 1, 4, 9, 16, 25, 36, 49, 64, 81}

[Kenny Lau]

but what are you doing with Lean.Name?

[Aaron Liu]

docs#IO.FS.withFile might be useful

[Aaron Liu]

The instances for printing a finset are all unsafe (you could sort it first but...)

[Dhruv Chaurasiya]

Kenny Lau said:

but what are you doing with Lean.Name?

So for my task, i have some sets, say set1, set2, set3. These have different type of properties and the elements of set1 have some relation r1 with elements of set2, and r2 with elements of set3 and so on.

For an example my Finset could be {"uid","sid","cid"} where uid is the name of set containings user_ids, sid and cid are defined similarly, and user with id1 follows some special properties,

[Kenny Lau]

I wouldn't recommend doing metaprogramming when you're just starting out

[Kenny Lau]

just use the set uid instead of the name "uid"

[Dhruv Chaurasiya]

Can you please elaborate on the metaprogramming, and are you suggesting that I use a Set named uid and store all the user_id's there? I may not know all the Sets i have to create beforehand and also all their contents, like in between the execution I might have to introduce some extra Set because I got more information.

[Kenny Lau]

can you give me more context? how are you storing the user ids? what is uid?

[Aaron Liu]

please don't use names like this

[Aaron Liu]

you can store a list of all the finsets instead

[Dhruv Chaurasiya]

User Id is a generic example here.

The problem statements goes like this.

I will have some facts which are predicates.

So a fact would look like A(set1,set2 ... set n), here A is a property which takes its input from set1 set2 ... set n.

I would get these properties as inputs, for example A(a1,a2), where a1 belongs to set1 and a2 belongs to set2. The statement A(a1,a2) means a1 and a2 are related by property A.

I can have a arbitrary numbers of these properties each having their different domain.

Then I would be provided with some relations between these properties, like for an example A(a1) <= B(a1,a2) for all a1.

I have to create a lattice which represents all such relations.

[Aaron Liu]

definitely don't need names for this

[Aaron Liu]

but depending on what kind of domain you allow this could be tricky

[Kenny Lau]

I don't know how you even learnt about Lean.Name, just don't use it

[Dhruv Chaurasiya]

If you guys say so, there might be some other way to do it ,
In my problem i would require a lattice structure and then some extra constraints on that lattice. Only inputs I would get is sets with all there elements, the predicates i mentioned (A(a1,a2)) and the relation between those predicates (A(a1) <= B(a1,a2)).

Then I have to prove some theorems related to them and construct some other structures on top of the lattice.

I thought finsets would help me model these relationships. If you could suggest anything else, that would be appreciated

[Aaron Liu]

what's the ordering?

[Aaron Liu]

sounds like some sort of presented lattice?

[Dhruv Chaurasiya]

The ordering is not fixed, Let me give an example from my paper, say we have 3 properties U, A,P

We have U(a1) <= A(a1,b) for all a1, where b is anything approved by the domain of A

A(a1,b) <= B(a2,b) for all b

P(a1,b1) <= P(a1,b1) for all a1

We in our inputs would get all valid U(a1), A(a1,b1) and P(a1,b1).

We have a top and bottom defined, so lub and glb are well defined.

We have to construct the lattice for this scenario, and then I have some other properties to prove. My initial goal is to devise a method which takes this rules as an input and generates me a lattice structure which I could use later on. We could have any number of such relations and any number of predicates.

[Aaron Liu]

is the goal to construct the lattice?

[Aaron Liu]

what are your domains allowed to be

[Aaron Liu]

is the collection of allowed domains fixed throughout the construction

[Aaron Liu]

this sounds like some sort of presented lattice

[Dhruv Chaurasiya]

Initial goal, yes. But it's step 1 for my work. Then I have some 10 lemmas I need to prove for a general lattice, and then 1 big theorem which has around 12 cases.

[Dhruv Chaurasiya]

Yes the domains are fixed once given.

[Aaron Liu]

are these concrete properties

[Aaron Liu]

or are they more like signatures

[Dhruv Chaurasiya]

Please elaborate on signatures?

[Aaron Liu]

Like the form of a predicate without an actual predicate behind it https://ncatlab.org/nlab/show/signature+(in+logic)

[Aaron Liu]

Maybe you could just say what you're doing

[Aaron Liu]

and I could look it up online

[Dhruv Chaurasiya]

I am proving some results on secure information flow, it's a new work yet to be published. My supervisor asked me to formalize all the proofs using Lean before we go for publishing.

And the properties are Signatures.

[Aaron Liu]

knowing what I know right now I would suggest you have

• a type ι representing your types
• a type Pred representing your predicates
• a function numArgs : Pred → Nat giving the arity of each predicate
• a function argTypes : (p : Pred) → Fin (numArgs p) → ι giving the type of each argument

[Dhruv Chaurasiya]

sounds good, i would try to implement this method. Thanks