## Stream: general

### Topic: structure equality from parts

#### Nicholas Scheel (Mar 21 2018 at 22:12):

Hi, I'm totally new here, I've spent about a day with Lean so far.

Currently I'm struggling to define a notion of equality for this structure (permutations aka bijective functions, which I represent with a function and its inverse, and the proof that they are inverses):

structure Perm (α : Type) :=
permute ::
(forward : α → α) (backward : α → α)
(are_inv : function.left_inverse forward backward ∧ function.right_inverse forward backward)


It appears that Lean understands refl enough to let me do the following:

def Perm.eq {α : Type}
: Π (p1 p2 : Perm α),
p1.forward = p2.forward →
p1.backward = p2.backward →
p1 = p1
| p1 p2 .(rfl) .(rfl) := rfl


but what I _really_ want is a proof that p1 = p2 at the end, but if I give it that type it complains that rfl : p1 = p1 not p1 = p2 (even though it looks like the compiler has enough information to determine p1 = p2 and has already unified them? idk)

I've looked in the standard library for similar examples but couldn't find any.

Would appreciate some pointers or help!

(my overall goal is to prove the group structure of permutations, which I think needs to be done through the components?)

#### Simon Hudon (Mar 21 2018 at 22:14):

You might want to build on top of equiv from mathlib.

#### Nicholas Scheel (Mar 21 2018 at 22:15):

in particular, if I try

.......
p1 = p2
| p1 p2 .(rfl) .(rfl) := _


I get the following message:

don't know how to synthesize placeholder
context:
α : Type,
Perm.eq : ∀ (p1 p2 : Perm α), p1.forward = p2.forward → p1.backward = p2.backward → p1 = p2,
p1 : Perm α
⊢ p1 = p1


Notice that only p1 is in scope and it wants a proof of p1 = p1, which is just rfl, but rfl won't actually unify in that environment when I try it.

#### Simon Hudon (Mar 21 2018 at 22:15):

| ⟨f₀,b₀,p₀⟩ ⟨f₁,b₁,p₁⟩ .(rfl) .(rfl) := rfl


#### Simon Hudon (Mar 21 2018 at 22:16):

| ⟨f₀,b₀,p₀⟩ ⟨._,._,._⟩ .(rfl) .(rfl) := rfl


I think that should work

#### Simon Hudon (Mar 21 2018 at 22:18):

The reason is that, to infer equality of the whole from equality of the parts, you need to pattern match on the whole. Then, the unification of the variables used for the components will translate into the patterns for the two wholes to be syntactically equal and this is where rfl works

#### Nicholas Scheel (Mar 21 2018 at 22:19):

hmm I'm still getting a cryptic error with both of those:

......
has type
∀ (forward_1 backward_1 : α → α)
(are_inv_1 : function.left_inverse forward_1 backward_1 ∧ function.right_inverse forward_1 backward_1),
{forward := forward, backward := backward, are_inv := are_inv}.forward =
{forward := forward_1, backward := backward_1, are_inv := are_inv_1}.forward →
{forward := forward, backward := backward, are_inv := are_inv}.backward =
{forward := forward_1, backward := backward_1, are_inv := are_inv_1}.backward →
{forward := forward, backward := backward, are_inv := are_inv} =
{forward := forward, backward := backward, are_inv := are_inv}
but is expected to have type
∀ (forward_1 backward_1 : α → α)
(are_inv_1 : function.left_inverse forward_1 backward_1 ∧ function.right_inverse forward_1 backward_1),
(λ (p2 : Perm α),
{forward := forward, backward := backward, are_inv := are_inv}.forward = p2.forward →
{forward := forward, backward := backward, are_inv := are_inv}.backward = p2.backward →
{forward := forward, backward := backward, are_inv := are_inv} = p2)
{forward := forward_1, backward := backward_1, are_inv := are_inv_1}


(I'm using https://leanprover.github.io/live/3.3.0/ btw)

#### Simon Hudon (Mar 21 2018 at 22:24):

I see. The problem is the . before rfl. I think the idea is that they are not irrelevant (or inferred from the context). They actually help you establish that p1 and p2 are identical:

def Perm.eq {α : Type}
: Π (p1 p2 : Perm α),
p1.forward = p2.forward →
p1.backward = p2.backward →
p1 = p2
| ⟨a,b,p⟩ ⟨._,._,._⟩ (rfl) (rfl) := rfl


#### Nicholas Scheel (Mar 21 2018 at 22:26):

aha! that seems to be working, thanks so much!

#### Kevin Buzzard (Mar 21 2018 at 22:27):

https://github.com/leanprover/mathlib/blob/master/data/equiv.lean

#### Kevin Buzzard (Mar 21 2018 at 22:27):

There are some spoilers for this sort of thing

#### Kevin Buzzard (Mar 21 2018 at 22:27):

Your Perm is the equiv on line 54

#### Kevin Buzzard (Mar 21 2018 at 22:30):

no, sorry, equiv can have different source and target. Your Perm is the perm on line 62

#### Nicholas Scheel (Mar 21 2018 at 22:31):

very cool, thanks for the link :) is that accessible in the online editor or no?

I think not

#### Simon Hudon (Mar 21 2018 at 22:33):

I think it is. The online version imports mathlib and I don't think equiv is too new

#### Kevin Buzzard (Mar 21 2018 at 22:33):

import data.equiv

#print equiv.perm



#### Kevin Buzzard (Mar 21 2018 at 22:34):

works in lean web editor

#### Simon Hudon (Mar 21 2018 at 22:34):

I just checked, it's there

#### Simon Hudon (Mar 21 2018 at 22:35):

@Kevin Buzzard I'm confused by your reaction to your own post. Which direction are you two pointing to?

#### Kevin Buzzard (Mar 21 2018 at 22:35):

I was trying to point to your comment :-)

#### Kevin Buzzard (Mar 21 2018 at 22:36):

Lean 3.4 should be with us soon, and perhaps they'll update the lean web editor so it runs 3.4. There was extensive discussion on gitter about getting everything to compile but in the end all the problems were solved IIRC.

#### Kevin Buzzard (Mar 21 2018 at 22:37):

https://gitter.im/leanprover_public/lean_js

#### Kevin Buzzard (Mar 21 2018 at 22:37):

probably-hard-to-find but useful link if you want to set it up yourself.

#### Kevin Buzzard (Mar 21 2018 at 22:39):

but if you're going to compile it I suppose you'd just be better off running it in an IDE :-) I think Scott compiled a more recent version of Lean and left it on an internet-facing server...

#### Simon Hudon (Mar 21 2018 at 22:41):

Was it hard to compile because of the new monadic code?

#### Mario Carneiro (Mar 21 2018 at 22:42):

No, that discussion predates the monad stuff by a while. I think it was just some JS compilation arcana

Oh fun!

#### Nicholas Scheel (Mar 21 2018 at 22:45):

I have a PureScript background – JS is weird :D

#### Kevin Buzzard (Mar 21 2018 at 22:45):

Yes, apparently taking a bunch of C++ code and compiling it into javascript isn't 100% straightforward

#### Nicholas Scheel (Mar 21 2018 at 22:46):

I have to say, the online editor is really slick I'm impressed!

#### Simon Hudon (Mar 21 2018 at 22:50):

So they actually translate the whole C++ code base to Java script and the whole thing runs in the browser? That's really cool :) I just assumed the code was sent to a server and sent back after verification.

#### Simon Hudon (Mar 21 2018 at 22:51):

I have to say, the online editor is really slick I'm impressed!

Microsoft has a few like that. It's a cool idea to get you started before you decide to install it

#### Kevin Buzzard (Mar 21 2018 at 22:55):

The moment you try and do something non-trivial in the lean web editor things slow to a crawl; the "recompile the entire file every time the user presses a key" gets old pretty quickly. But for small bits of experimentation I absolutely agree, it's very cute.

#### Nicholas Scheel (Mar 21 2018 at 22:57):

yeah, and a little debouncing would go a long ways ... but I'm patient with it ;)

#### Simon Hudon (Mar 21 2018 at 22:58):

It might just be a tease: the real thing is actually pretty fast and getting faster.

#### Simon Hudon (Mar 21 2018 at 22:59):

I think @Sebastian Ullrich should merge an incremental caching strategy pretty soon which will make things even smoother

#### Kevin Buzzard (Mar 21 2018 at 22:59):

The next step after Lean Web Editor is to try a nightly. Except that the current nightly might not work with mathlib. Is this now a problem that the community has solved?

#### Kevin Buzzard (Mar 21 2018 at 22:59):

What is this #travis stream anyway?

#### Simon Hudon (Mar 21 2018 at 23:00):

What is this #travis stream anyway?

Whenever someone commits to mathlib, we get the build report there.

#### Kevin Buzzard (Mar 21 2018 at 23:01):

Oh, so we still don't have access to e.g. a nightly build before all the monad refactoring stuff went in?

I mean core lean

#### Kevin Buzzard (Mar 21 2018 at 23:03):

There was an entire week from 13th to 20th March with no commits and Lean was working just fine for me. And now we have all this monad refactoring and everyone is assuming mathlib won't build any more

#### Simon Hudon (Mar 21 2018 at 23:05):

I think older nightlies should still be available. Don't you get a long list of nightlies on the site?

#### Simon Hudon (Mar 21 2018 at 23:06):

I think what we might need is for mathlib to publish Lean nightlies, a subset of all the nightlies for which mathlib passes.

#### Kevin Buzzard (Mar 21 2018 at 23:07):

I can pull the repo and checkout a random commit and compile, but I don't think I've ever seen a list of nightlies. Where are they?

#### Simon Hudon (Mar 21 2018 at 23:10):

I can't find it anymore. I wonder if they changed the way nightly works

#### Nicholas Scheel (Mar 21 2018 at 23:11):

here's my messy code as a whole if anyone is curious :wink: https://gist.github.com/MonoidMusician/b2792a2d9687dd627155996097ad97c1 (we talked about equivalence classes of functions with permutations in my combinatorics class, so I wanted to play around with the idea a little bit – in particular, equivalent surjective functions will have a unique (post-composed) permutation for the equivalence)
thanks again for the help!

#### Sebastian Ullrich (Mar 21 2018 at 23:14):

The nightly releases PR was merged today, though today's build has already failed because of broken setup... I'll test it tomorrow by having it build a custom pre-monad nightly

#### Simon Hudon (Mar 21 2018 at 23:15):

Are more than one nightly supposed to be available at any given time?

#### Kevin Buzzard (Mar 21 2018 at 23:15):

I've never seen more than one available

#### Kevin Buzzard (Mar 21 2018 at 23:15):

(per OS of course)

#### Simon Hudon (Mar 21 2018 at 23:16):

I should go offline: my dissertation doesn't write itself when I don't look at it :/ (no matter how long I look away)

#### Mario Carneiro (Mar 21 2018 at 23:16):

I think your definition of PostPermEquiv should use subtype (notation {x // p x})

#### Nicholas Scheel (Mar 21 2018 at 23:28):

okay, looks good – what's the difference? :)

#### Nicholas Scheel (Mar 21 2018 at 23:31):

ah, more specific to Prop?

#### Mario Carneiro (Mar 21 2018 at 23:36):

You also shouldn't need the n+2 case in the definition of swap and swap_involution

#### Mario Carneiro (Mar 21 2018 at 23:37):

Also, as Kevin says most of this theory is in data.equiv in mathlib, although we don't do anything with postperm stuff

#### Nicholas Scheel (Mar 21 2018 at 23:37):

hmm I get

non-exhaustive match, the following cases are missing:
swap ⟨nat.succ (nat.succ _), _⟩


#### Kevin Buzzard (Mar 21 2018 at 23:43):

| ⟨n+2, prf⟩ := ⟨n+2,prf⟩ works :-)

#### Mario Carneiro (Mar 21 2018 at 23:45):

Ah, I see, it would work except that the underlying inductive type nat.less_than_or_equal eliminates to Prop, so it can't be used to define an element of fin 2 (although it can be used to define an element of false which then defines an element of fin 2)

#### Mario Carneiro (Mar 21 2018 at 23:47):

You can also use absurd prf dec_trivial instead of that finis stuff

#### Nicholas Scheel (Mar 21 2018 at 23:49):

I will learn these voodoo tactics one day!

#### Kevin Buzzard (Mar 21 2018 at 23:49):

If you define swap (n+2) to be n+2 then you get to write

lemma  swap_involution : ∀ n, swap (swap n) = n
| ⟨0, _⟩ := rfl
| ⟨1, _⟩ := rfl
| ⟨n+2, prf⟩ := rfl
`

#### Nicholas Scheel (Mar 21 2018 at 23:51):

true, and that's essentially what the more general swapping does too

#### Nicholas Scheel (Mar 21 2018 at 23:53):

thanks for all the help!!

Last updated: Dec 20 2023 at 11:08 UTC