Zulip Chat Archive

Stream: general

Topic: expr's with local constant


view this post on Zulip 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 : α)

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jan 02 2019 at 19:05):

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

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Jan 02 2019 at 19:06):

tactic expr is good enough.

view this post on Zulip Patrick Massot (Jan 02 2019 at 19:08):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jan 02 2019 at 19:09):

It's difficult to be more precise without more context

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jan 02 2019 at 19:30):

how do you intend to verify the result?

view this post on Zulip Chris Hughes (Jan 02 2019 at 19:31):

Some decidable instance.

view this post on Zulip Chris Hughes (Jan 02 2019 at 19:31):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jan 02 2019 at 19:32):

how does that decidable instance work

view this post on Zulip Mario Carneiro (Jan 02 2019 at 19:33):

is it fast enough?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 02 2019 at 19:35):

so you only need the cardinalities, not the classes

view this post on Zulip Chris Hughes (Jan 02 2019 at 19:35):

Yeah.

view this post on Zulip Chris Hughes (Jan 02 2019 at 19:35):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 02 2019 at 19:40):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Chris Hughes (Jan 02 2019 at 19:47):

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

view this post on Zulip Mario Carneiro (Jan 02 2019 at 19:48):

and what is A5 for you?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 02 2019 at 19:54):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 02 2019 at 19:59):

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

view this post on Zulip Mario Carneiro (Jan 02 2019 at 20:00):

Actually the first step is calculating partitions of 5

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jan 02 2019 at 20:24):

what's the expr for the real number pi?

view this post on Zulip Chris Hughes (Jan 02 2019 at 20:26):

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

view this post on Zulip Kenny Lau (Jan 02 2019 at 20:28):

but you only have the object now

view this post on Zulip Kenny Lau (Jan 02 2019 at 20:28):

you don't know how it was created

view this post on Zulip Kenny Lau (Jan 02 2019 at 20:28):

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

view this post on Zulip Kenny Lau (Jan 02 2019 at 20:29):

you can't possibly surject real -> expr

view this post on Zulip Chris Hughes (Jan 02 2019 at 20:29):

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

view this post on Zulip Chris Hughes (Jan 02 2019 at 20:29):

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

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Jan 02 2019 at 20:34):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Jan 02 2019 at 20:39):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 02 2019 at 20:39):

right.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jan 02 2019 at 20:41):

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

view this post on Zulip Kenny Lau (Jan 02 2019 at 20:41):

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

view this post on Zulip 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