How do I make a type class instance of a finset

Stream: new members

[Lars Ericson]

This works:

import data.finset.basic
def X := fin 3
instance X_has_one : has_one X := fin.has_one

This does not work:

import data.finset.basic
def X : set ℕ := ({1, 2, 3} : finset ℕ)
def X_one : X := 1
instance X_has_one : has_one X := { one := X_one }

Is there a way to make it work? The main error is

failed to synthesize type class instance for
⊢ has_one ↥X
All Messages (1)

and I don't know how to make a type class instance of

structure finset (α : Type*) :=
(val : multiset α)
(nodup : nodup val)

[Alex J. Best]

Well the only way lean knows what the symbol 1 means is via a has_one instance, so what you've written is circular.

[Alex J. Best]

By writing X_one : X you are coercing the set of naturals X into a type, which is what the up arrow means

[Alex J. Best]

This type is then the subtype {x : nat // x \in {1,2,3} so to make an element we give a pair of a natural number, and a proof it is in the set {1,2,3}

[Alex J. Best]

def X_one : X := ⟨1,set.mem_insert 1 (λ (b : ℕ), b = 2 ∨ list.mem b [3])⟩

works (via library search so the proof is kinda random)

[Alex J. Best]

To make a finset you must provide both these fields like this:

def my_finset : finset ℕ := { val := {1,2},
  nodup := multiset.erase_dup_eq_self.mp rfl}

once again i used library search to find a proof of the second, in general what you write for nodup will depend on the form of val

[Lars Ericson]

Thanks @Alex J. Best , from your advice, this works:

import data.finset.basic
def X : set ℕ := ({1, 2, 3} : finset ℕ)
def X_one : X := ⟨1,set.mem_insert 1 (λ (b : ℕ), b = 2 ∨ list.mem b [3])⟩
instance X_has_one : has_one X := { one := X_one }

[Lars Ericson]

(deleted)

[Mario Carneiro]

set.mem_insert 1 (λ (b : ℕ), b = 2 ∨ list.mem b [3])

wow that's a really unique way to write 1 \in {1,2,3}

[Mario Carneiro]

The theorem you are claiming is false

[Mario Carneiro]

it is not true that {1} \cap \empty = {1}

[Yakov Pechersky]

I think Lars wants 1 to be univ

[Lars Ericson]

DONE, thanks!

import data.finset.basic

def X : set ℕ := ({1, 2, 3} : finset ℕ)

def PX_mul (x y : set X) : set X := (x ∩ y : set X)
instance PX_has_mul : has_mul (set X) := ⟨ PX_mul ⟩

theorem PX_mul_assoc (x y z : set X) :  (x * y) * z = x * (y * z) := inf_assoc

instance PX_semigroup : semigroup (set X) := ⟨ PX_mul, PX_mul_assoc ⟩

instance PX_has_one : has_one (set X) := { one := set.univ }  -- OK

lemma PX_one_mul : (∀ a : set X, 1 * a = a) :=
begin
  intro,
  exact top_inf_eq,
end

lemma PX_mul_one : (∀ a : set X, a * 1 = a) :=
begin
  intro,
  exact inf_top_eq,
end

instance PX_monoid : monoid (set X) :=
{
  one := PX_has_one.one,
  mul := PX_mul,
  mul_assoc := PX_mul_assoc,
  one_mul := PX_one_mul,
  mul_one := PX_mul_one
}

[Kevin Buzzard]

import tactic

def X : set ℕ := {1, 2, 3}

...

would be a saner way to start. This has nothing to do with finsets.

[Kevin Buzzard]

and

instance PX_monoid : monoid (set X) :=
{
  one := 1,
  mul := (*),
...

is a better way to finish, because you want to stick as much as possible to has_mul.mul and has_one.one rather than anything defeq to them.

[Kevin Buzzard]

You should learn the trick of moving stuff before the colon in the statements of the lemmas; this saves you having to intro in the proofs, which saves a line. In fact with stuff like mul_one you don't even need to use tactic mode with this trick:

lemma PX_mul_one (a : set X) : a * 1 = a := inf_top_eq

Finally, instead of all this PX_ stuff you should just go into a namespace and call your lemmas what they want to be called, e.g. mul_one. Rigidly sticking to the naming conventions makes everyone's lives easier.

[Lars Ericson]

Thank you @Kevin Buzzard here is the revised example. It doesn't require import tactic. When would I use that?

import data.finset.basic

namespace finite_monoid_example

def X : set ℕ := ({1, 2, 3} : finset ℕ)
def mul (x y : set X) : set X := (x ∩ y : set X)
instance : has_mul (set X) := ⟨ mul ⟩
lemma mul_assoc (x y z : set X) : (x * y) * z = x * (y * z) := inf_assoc
instance : has_one (set X) := ⟨ set.univ ⟩
lemma one_mul (a : set X) : 1 * a = a := top_inf_eq
lemma mul_one (a : set X): a * 1 = a := inf_top_eq

instance : monoid (set X) :=
{
  one := 1,
  mul := (*),
  mul_assoc := mul_assoc,
  one_mul := one_mul,
  mul_one := mul_one
}

end finite_monoid_example

[Kevin Buzzard]

Importing finsets for the sole reason of creating a finset and then instantly coercing it to a set seems a bit crazy to me. I imported tactic because I import this every time I use Lean. I imported it on this occasiont simply because it gave me stuff like monoid.

[Lars Ericson]

@Kevin Buzzard , for self-training, I am filling out finite nontrivial concrete set examples for each box in this picture:

Screenshot-from-2020-12-12-09-15-45.png

I find filling out each box to be a challenge. I am using two representations of the finite concrete nontrivial set {0,1,2} because they sometimes work exactly the same and sometimes don't, so I learn little bits of stuff when they work differently. The two representations are def X := fin 3 and def X : set ℕ := ({0,1,2} : finset ℕ). You could view these exercises as redundant, trivial and a bit crazy. I still find them hard to perform correctly.

I'm not trying to come up with anything new. I'm just trying to learn how to work with lean. I never took an algebra course in college. I only understand things that I can program. When I am done, if quizzed on the street, I should be able to tell the difference between a canonically ordered additive monoid and a commutative semiring, and I should be able to give practical, simple, nontrivial examples of each structure.

[Mario Carneiro]

You will find it a lot easier to use examples like int rather than finite sets

[Kevin Buzzard]

My point is simply that you are using finset to make a set, and you can just make the set directly with the same notation {1,2,3}.

[Mario Carneiro]

not sure if your picture goes as far as ordered rings but I can tell you {1,2,3} isn't one

[Kevin Buzzard]

The naturals will be a nice example of pretty much all of these. I wrote the natural number game by trying to construct loads of typeclass instances on the naturals and then it was just a case of sorting everything into some kind of order which didn't introduce too many tactics all at once

[Kevin Buzzard]

I was genuinely stunned to find that I could construct the commutative semiring instance on nat with just rw, refl and induction. I mentioned this to Jeremy and he laughed at me :-) and said something about equational theories which I didn't understand. mathematicians don't really need to understand mathematics in some sense

[Kevin Buzzard]

I mean they don't need to understand the way it works under the hood

[Kevin Buzzard]

On the other hand proving it was a partial order needed loads of tactics

[Lars Ericson]

Most of these work for ℕ as one-liners. The point of the {0,1,2} or {1,2,3} examples is that they make me do a little more work. Also, if I try to do ordered ring with {1,2,3} and it doesn't go through, then I have to think harder about ordered rings and if there is a nontrivial finite example and then construct that. I say nontrivial in the Lean technical sense because it makes it a little more challenging. I.e. there are probably trivial instances of ordered ring that are provable with less effort, but not in a way that generalizes. I feel like {0,1,2} proofs are more likely to generalize to the ℕ case, so I get more intuition from doing them than from doing proofs for trivial sets.

I'm trying to firm up my mathematical education by going through these kinds of exercises. I am building up a vocabulary I haven't yet acquired. I don't know enough to easily see that {1,2,3} isn't an ordered ring. Lean is perfect in that regard because every assumption about an object can be clearly stated and clearly verified. There is no hand-waving. I see it as a mental prosthetic which will help me acquire and learn how to work with concepts that were previously too daunting or mysterious to approach, like the construction of the reals or the Lebesgue integral.

[Kevin Buzzard]

Learning mathematics by doing it in Lean seems very difficult. My successful students at Imperial are the ones who know the maths already and learn formalising by formalising mathematics they can do already on paper.

[Kevin Buzzard]

Two educationalists did a study on one of my courses and this was one of their main conclusions.

[Kevin Buzzard]

Next term I'm going to be teaching undergraduate mathematics in lean to PhD students and I'm very excited about this because here everyone will know all the mathematical material already so it will be a very different experience to what people like Heather, Patrick and I have experienced before

[Lars Ericson]

My self-assessment is that what I am doing (stepping through these exercises) is the path most likely to give me insight.

I have a practical goal, which is to teach friends about strong and weak numerical approximations of stochastic processes using various kinds of discretizations involving stochastic Taylor series expansions of Ito and Stratonovich integrals. Formalizing and checking definitions related to this in Lean seems to me like the shortest path to being able to explain the material to others.

That may seem a little far-fetched, but I feel like Lean will give me a bionic exoskeleton comfort level that I wouldn't have otherwise. For example, if I were told to prove that the β in the following construction was a measurable function, in Lean I feel like I would have a shot, and the result would be rigorous. If I had to do it completely on my own by hand, I would have no such confidence:

Screenshot-from-2020-12-13-21-18-06.png

[Yakov Pechersky]

I think a possible fear is that two things could be happening. There's stumbling to solve the problems at hand without seeing why related constructions don't satisfy the same constraints. Or there's cargo culting proofs from one topic to another. Both lead to an understanding that's not as deep as one would like, or could get from a larger mathematical training. That's not to say that it's easy to get that training, or that it's a given that deep understanding comes easily. Just pointing out potential pitfalls.

[Yakov Pechersky]

Those could be some of the things Kevin is referring to, in the students that had more difficulty in being successful.

[Lars Ericson]

The back story here is that I'm 61 years old and I've worked with computer algebra systems and theorem proving systems quite a bit, including Macsyma, Maple, Mathematica, Axiom, SymPy, Edinburgh LCF back in the day, CAML and implementations of real algebraic number arithmetic including Sturm sequences, resultants, and Grobner bases and decision procedures for sublanguages of set theory. Most of the time I am cargo culting. I know real mathematicians with larger and proper mathematical training when I see them. I know I don't have that training. But I do have a little bit of common sense and I know that I've learned something over the last several weeks by trying to get things to go in Lean, if only that you don't like putting names on things when you don't have to and you like to organize around measurable spaces but you don't like to organize around sigma algebras. There is no chance, at my age, in my career, with my practical options, that I will have the time or resources to go back to school and get proper training. Not that any mathematician would want me. At one point I wanted to pick up the family and go study with Jordan Stoyanov, an itinerant mathematician retired from Newcastle. My wife threw a fit. She likes a big house. So I do what I can. Lean and Zulip are a gift from God in that respect. To some extent things like EdX and Coursera can be helpful, and I've been there, but for some reason, the MOOC world is full of interesting exotic topics but a solid and thorough curriculum in core mathematics is just not there. So I do what I can, and what comes easily. Printing a graph of Lean definitions and then trying to find concrete instances that satisfy each definition is something that fits my skill set and temperament. It's not math maybe, but I find it satisfying. It's what I can do. It may or not be fruitful for me individually. It won't matter to anybody else if it is or isn't. I'm not trying to cure cancer here, just scratch my own personal itch.