expr's with local constant

Stream: general

[Chris Hughes]

What's the best way of getting something a bit like this to work?

meta example {α : Type} [group α] : expr := `(1 : α)

[Chris Hughes]

I guess it would it be better for α to be an expression representing a type, instead of a type?

[Patrick Massot]

Do you really want an expr or would a tactic expr be good enough?

[Rob Lewis]

That's generally the right move, yes. There are ways to make something like this work with alpha being a type using reflected instances. Along the lines of

meta def my_def (α : Type) [h : group α] [h2 : reflected h] [h3 : reflected α] : expr := `(@has_one.one.{0} %%h3 %%h2)

But that's weird. What application do you have in mind?

[Chris Hughes]

tactic expr is good enough.

[Patrick Massot]

tactic.to_expr ```((1 : α)) should work then

[Rob Lewis]

For tactic expr and taking alpha as an expr, it's easy.

meta def my_def' (α : expr) : tactic expr :=
tactic.to_expr ``(1 : %%α)

If the check for a group instance is important, it's easy to add.

[Patrick Massot]

It's difficult to be more precise without more context

[Chris Hughes]

The context is, and I think I might be going about this the wrong way, is that I have a function that computes the conjugacy classes of a finite group as a finset (finset G). It's too slow for the kernel, but fast enough for the VM. I want to compute this in the VM, and then verify it does indeed return the conjugacy classes in the kernel. Do I have to go via expr for this?

[Mario Carneiro]

how do you intend to verify the result?

[Chris Hughes]

Some decidable instance.

[Chris Hughes]

Though I'm not at all sure this is a good approach.

[Mario Carneiro]

no, I mean what's the method you use to check that the result is correct, which is not the same as just calculating the classes?

[Mario Carneiro]

how does that decidable instance work

[Mario Carneiro]

is it fast enough?

[Chris Hughes]

I haven't written it yet. It probably won't be that much faster than computing it from scratch.

[Chris Hughes]

I'm trying to prove A5 is simple by the way, and there's a proof that says look at the cardinalities of the conjugacy classes.

[Mario Carneiro]

so you only need the cardinalities, not the classes

[Chris Hughes]

Yeah.

[Chris Hughes]

But I guess it's hard to verify the cardinalities without verifying the elements.

[Mario Carneiro]

what are you looking for in the cardinalities? Do you really need to calculate all of them or can you use a symmetry argument for the rest?

[Mario Carneiro]

I like to think of these kinds of problems as if I am a human mathematician who doesn't want to do too much calculation; theorem provers generally prefer those kinds of proofs, as opposed to the blasty proofs that make them sweat

[Chris Hughes]

The cardinalities are {1, 12, 12, 15, 20}. I was hoping to do a blasty proof that meant I didn't have to think.

[Chris Hughes]

The non blasty proofs pretty much involve looking at cycle shapes, which is quite a lot of work.

[Mario Carneiro]

isn't there some thing about 3-transpositions generating A5 that helps?

[Chris Hughes]

The version of that I've seen involves casing on the cycle type, and proving that whatever the cycle type of a non trivial element, there is a 3-cycle.

[Mario Carneiro]

You can still split the difference between the blasty stuff and some smarts. For example, you can calculate the order of a subgroup with only a few well chosen elements and non-elements, depending on the group

[Chris Hughes]

So I have to prove Screenshot-2019-01-02-at-19.44.58.png

[Mario Carneiro]

and what is A5 for you?

[Chris Hughes]

def alternating (α : Type*) [decidable_eq α] [fintype α] : Type* :=
is_group_hom.ker (sign : perm α → units ℤ)

withfin 5 instead of alpha

[Mario Carneiro]

I guess you can consider the orders of different elements in sigma

[Mario Carneiro]

They can't all be 1. If all are 1 or 2 it is (a b)(c d), if there is one with 3 it is (a b c); and if there is one with 5 it is (a b c d e). You have to argue that 4 is not possible, and (a b c) (d e) is not possible

[Mario Carneiro]

I think it is important to have some way to talk about cycles for this

[Mario Carneiro]

Actually the first step is calculating partitions of 5

[Mario Carneiro]

for a given partition you can say if it is even or odd and thus get the list 3+1+1, 2+2+1, 5 for possible cycle decompositions

[Mario Carneiro]

(I guess a partition is even if the sum of all the elements of the list decreased by 1 is even, so 3+1+1 sums to 2 so is included, while 3+2 sums to 3 and is excluded)

[Chris Hughes]

Here's one approach to verify the conjugacy classes. For the proof it suffices to prove that every conjugacy class I produce is a subset of a conjugacy class, it doesn't have to be equal. So it suffices to prove conjugacy of one element of each class with every other element, which I can do much more efficiently by intelligently finding the element, instead of searching. This is getting rather complicated now though.

[Chris Hughes]

In meta land, can I not just turn any object of any type into an expr really easily?

[Kenny Lau]

what's the expr for the real number pi?

[Chris Hughes]

meta def pi_expr : expr := `(real.pi)

[Kenny Lau]

but you only have the object now

[Kenny Lau]

you don't know how it was created

[Kenny Lau]

Point is there is uncountably many real numbers yet only countably many expr

[Kenny Lau]

you can't possibly surject real -> expr

[Chris Hughes]

Yeah, but it's meta, so who cares.

[Chris Hughes]

I won't be able to input those undefinable reals into my function.

[Kevin Buzzard]

There are abstract proofs that A_n is simple for all n>=5 but for just A_5 I always tell people to go for the counting proof. Can Lean really not count to 60?

[Chris Hughes]

What's the counting proof. The one I mentioned?

[Chris Hughes]

Naively computing conjugacy classes is quadratic time I think. Plus there's lots of little inefficiencies in the algorithm that I've written.

[Kevin Buzzard]

Naively computing conjugacy classes might be quadratic time, but 60^2 is still a lot less than a million.

[Chris Hughes]

But more than the kernel can handle apparently. You've got to erase duplicates as well, which increases the time quite a bit, so it's worse than quadratic I think.

[Kevin Buzzard]

I know something about abstract algorithms, and I know something about maths, but I have no idea how Lean implements abstract algorithms, or stores data types, so I am bewildered as to why all this is even an issue. I am pretty sure that I can write code which does this in gap and terminates very quickly.

[Chris Hughes]

My VM version takes 246ms. But the kernel is unbelievably slow.

[Kevin Buzzard]

From the point of view of abstract algorithms, stuff like erasing dupes can just be done with hash tables or whatever.

[Kevin Buzzard]

Maybe I am imagining what the VM does, not what the kernel does. I still don't really know the difference.

[Kenny Lau]

yeah but when you use hash tables in say PARI/GP you don't need to prove that it works

[Kevin Buzzard]

right.

[Kevin Buzzard]

but here the hash is just the list of where [1,2,3,4,5] go and proving that two lists are equal or not is not hard.

[Kenny Lau]

maybe we can store lemmas like 4 != 5 :P

[Kenny Lau]

I don't think there's any caching in Lean...

[Chris Hughes]

Imagine how bad it would be if I'd filtered all the functions to prove fintype_perm like some people suggested.