## Stream: general

### Topic: expr's with local constant

#### Chris Hughes (Jan 02 2019 at 18:43):

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

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


#### Chris Hughes (Jan 02 2019 at 18:59):

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

#### Patrick Massot (Jan 02 2019 at 19:05):

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

#### Rob Lewis (Jan 02 2019 at 19:06):

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 (Jan 02 2019 at 19:06):

tactic expr is good enough.

#### Patrick Massot (Jan 02 2019 at 19:08):

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

#### Rob Lewis (Jan 02 2019 at 19:08):

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 (Jan 02 2019 at 19:09):

It's difficult to be more precise without more context

#### Chris Hughes (Jan 02 2019 at 19:23):

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 (Jan 02 2019 at 19:30):

how do you intend to verify the result?

#### Chris Hughes (Jan 02 2019 at 19:31):

Some decidable instance.

#### Chris Hughes (Jan 02 2019 at 19:31):

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

#### Mario Carneiro (Jan 02 2019 at 19:32):

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 (Jan 02 2019 at 19:32):

how does that decidable instance work

#### Mario Carneiro (Jan 02 2019 at 19:33):

is it fast enough?

#### Chris Hughes (Jan 02 2019 at 19:33):

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

#### Chris Hughes (Jan 02 2019 at 19:34):

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 (Jan 02 2019 at 19:35):

so you only need the cardinalities, not the classes

Yeah.

#### Chris Hughes (Jan 02 2019 at 19:35):

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

#### Mario Carneiro (Jan 02 2019 at 19:36):

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 (Jan 02 2019 at 19:38):

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 (Jan 02 2019 at 19:38):

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 (Jan 02 2019 at 19:39):

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

#### Mario Carneiro (Jan 02 2019 at 19:40):

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

#### Chris Hughes (Jan 02 2019 at 19:43):

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 (Jan 02 2019 at 19:45):

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 (Jan 02 2019 at 19:47):

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

#### Mario Carneiro (Jan 02 2019 at 19:48):

and what is A5 for you?

#### Chris Hughes (Jan 02 2019 at 19:48):

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


withfin 5 instead of alpha

#### Mario Carneiro (Jan 02 2019 at 19:54):

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

#### Mario Carneiro (Jan 02 2019 at 19:56):

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 (Jan 02 2019 at 19:59):

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

#### Mario Carneiro (Jan 02 2019 at 20:00):

Actually the first step is calculating partitions of 5

#### Mario Carneiro (Jan 02 2019 at 20:02):

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 (Jan 02 2019 at 20:03):

(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 (Jan 02 2019 at 20:20):

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 (Jan 02 2019 at 20:24):

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

#### Kenny Lau (Jan 02 2019 at 20:24):

what's the expr for the real number pi?

#### Chris Hughes (Jan 02 2019 at 20:26):

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


#### Kenny Lau (Jan 02 2019 at 20:28):

but you only have the object now

#### Kenny Lau (Jan 02 2019 at 20:28):

you don't know how it was created

#### Kenny Lau (Jan 02 2019 at 20:28):

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

#### Kenny Lau (Jan 02 2019 at 20:29):

you can't possibly surject real -> expr

#### Chris Hughes (Jan 02 2019 at 20:29):

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

#### Chris Hughes (Jan 02 2019 at 20:29):

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

#### Kevin Buzzard (Jan 02 2019 at 20:32):

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 (Jan 02 2019 at 20:34):

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

#### Chris Hughes (Jan 02 2019 at 20:35):

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 (Jan 02 2019 at 20:36):

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

#### Chris Hughes (Jan 02 2019 at 20:38):

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 (Jan 02 2019 at 20:38):

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 (Jan 02 2019 at 20:39):

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

#### Kevin Buzzard (Jan 02 2019 at 20:39):

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

#### Kevin Buzzard (Jan 02 2019 at 20:39):

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

#### Kenny Lau (Jan 02 2019 at 20:39):

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

right.

#### Kevin Buzzard (Jan 02 2019 at 20:40):

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 (Jan 02 2019 at 20:41):

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

#### Kenny Lau (Jan 02 2019 at 20:41):

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

#### Chris Hughes (Jan 02 2019 at 20:45):

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

Last updated: May 11 2021 at 13:22 UTC