Zulip Chat Archive

Stream: general

Topic: by exact works, but not the term itself


view this post on Zulip Adam Topaz (Nov 27 2020 at 04:27):

import data.quot
variables {α : Type*} (r : α  α  Prop) (π : α  α)

inductive rel : α  α  Prop
| of {x y} : r x y  rel x y
| compat {x y} : rel x y  rel (π x) (π y)
| refl (x) : rel x x
| symm (x y) : rel x y  rel y x
| trans (x y z) : rel x y  rel y z  rel x z

def thing : setoid α := rel r π, rel.refl, rel.symm, rel.trans⟩⟩

def β := quotient (thing r π)

variable {γ : Type*}

-- This works.
def δ0 : β r π  β r π := @quotient.lift _ _ (thing r π) (λ a, quotient.mk' $ π a)
(by exact (λ x y h, quotient.sound' $ rel.compat h))

-- This fails.
def δ1 : β r π  β r π := @quotient.lift _ _ (thing r π) (λ a, quotient.mk' $ π a)
(λ x y h, quotient.sound' $ rel.compat h)

view this post on Zulip Adam Topaz (Nov 27 2020 at 04:28):

What's happening here? How come (by exact (λ x y h, quotient.sound' $ rel.compat h)) works but (λ x y h, quotient.sound' $ rel.compat h) doesn't?

view this post on Zulip Bryan Gin-ge Chen (Nov 27 2020 at 04:34):

Using by exact term causes Lean to delay the elaboration of term until the end, and this is sometimes more successful because more instances and other stuff have been figured out. Gabriel explained it better here.

view this post on Zulip Adam Topaz (Nov 27 2020 at 04:39):

That makes sense. Thanks @Bryan Gin-ge Chen

view this post on Zulip Kenny Lau (Nov 27 2020 at 05:54):

in other words, because Lean is weird and that's just how things work

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 08:04):

It's because elaboration is hard and just because humans know the order to do things doesn't mean that computers do.

view this post on Zulip Eric Wieser (Nov 27 2020 at 08:23):

How far into the expression can you push the by exact?

view this post on Zulip Adam Topaz (Nov 27 2020 at 13:18):

I think it's the rel.compat causing the issue here... So I think putting the exact to the left of rel.compat should work too

view this post on Zulip Adam Topaz (Nov 27 2020 at 13:18):

Is it possible to define \delta0 without any tactic mode and without any other definitions?

view this post on Zulip Eric Wieser (Nov 27 2020 at 13:24):

I can't seem to move the by exact at all

view this post on Zulip Adam Topaz (Nov 27 2020 at 13:24):

Oh

view this post on Zulip Eric Wieser (Nov 27 2020 at 13:26):

I suspect things are going wrong for you because setoid is usually used as a typeclass instance, and that's not what you're doing here

view this post on Zulip Eric Wieser (Nov 27 2020 at 13:27):

This works:

def δ0' : β r π  β r π :=
@quotient.lift _ _ (thing r π) (λ a, quotient.mk' $ π a)
(λ x y h, @quotient.sound' _ (thing r π) _ _ (rel.compat h))

view this post on Zulip Eric Wieser (Nov 27 2020 at 13:27):

Because it prevents quotient.sound' using typeclass search to find the setoid

view this post on Zulip Adam Topaz (Nov 27 2020 at 13:28):

quotient.sound' has no [...] in its type

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 13:28):

Adam Topaz said:

Is it possible to define \delta0 without any tactic mode and without any other definitions?

Why do you want to avoid tactic mode? You're filling in a proof so there's no harm in using tactic mode.

view this post on Zulip Adam Topaz (Nov 27 2020 at 13:29):

@Kevin Buzzard just for a sanity check

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 13:29):

quotient.sound uses typeclasses to find the equivalence relation, quotient.sound' uses unification.

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 13:30):

typeclasses are not appropriate here because the equivalence relation depends on the variable π.

view this post on Zulip Adam Topaz (Nov 27 2020 at 13:31):

And it's strange that @Eric Wieser 's definition works!

view this post on Zulip Reid Barton (Nov 27 2020 at 13:31):

I think it doesn't help that you build the second quotient with quotient.mk' and Lean has no way to see yet what kind of quotient it should be

view this post on Zulip Eric Wieser (Nov 27 2020 at 13:31):

def pre (π : α → α) := α would give you something you can stick a typeclass on

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 13:31):

Why is it strange? He's filling in the relation.

view this post on Zulip Adam Topaz (Nov 27 2020 at 13:32):

Oh nevermind thats right

view this post on Zulip Reid Barton (Nov 27 2020 at 13:32):

def δ1 : β r π  β r π := @quotient.lift _ _ (thing r π) (λ a, @quotient.mk' α (thing r π) $ π a)
(λ x y h, quotient.sound' (rel.compat h))   -- also works

view this post on Zulip Reid Barton (Nov 27 2020 at 13:32):

because you use @quotient.lift, Lean won't use the expected type of the whole body to elaborate the arguments

view this post on Zulip Reid Barton (Nov 27 2020 at 13:32):

so there is a bit of a puzzle for it to solve

view this post on Zulip Reid Barton (Nov 27 2020 at 13:33):

in quotient.mk', what quotient? in quotient.sound', what quotient?

view this post on Zulip Adam Topaz (Nov 27 2020 at 13:34):

But humans can figure it out from the type of Delta, so why can't lean?

view this post on Zulip Reid Barton (Nov 27 2020 at 13:34):

Lean is not a human

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 13:34):

It can, when you tell it to use a certain elaboration strategy (with by exact).

view this post on Zulip Reid Barton (Nov 27 2020 at 13:35):

I think what happens is (because of the outer @) Lean tries to elaborate all the arguments of quotient.lift before attempting to unify its type with the declared type of the definition

view this post on Zulip Reid Barton (Nov 27 2020 at 13:36):

and this strategy can't work because Lean would need to invent the term thing r π as the setoid on the target that it can prove using rel.compat

view this post on Zulip Reid Barton (Nov 27 2020 at 13:37):

if you stick by exact in a certain place then Lean says "we'll figure this stuff out later" and then once it looks at the type of the def it knows what to do

view this post on Zulip Adam Topaz (Nov 27 2020 at 13:37):

I see. So with Eric's code all lean has to do is unify the thing ... with the setoid.r

view this post on Zulip Reid Barton (Nov 27 2020 at 13:40):

I'm not sure why there isn't a quotient.lift' to go with mk' and sound'

view this post on Zulip Reid Barton (Nov 27 2020 at 13:41):

Sometimes (like here) it's annoying that using @ to specify some implicit argument also changes the overall elaboration strategy

view this post on Zulip Adam Topaz (Nov 27 2020 at 13:41):

I don't understand why setoid is a class anyway...

view this post on Zulip Reid Barton (Nov 27 2020 at 13:44):

With a quotient.lift' the natural thing with no @s or other funny business does work.

view this post on Zulip Reid Barton (Nov 27 2020 at 13:44):

I guess it just never came up before

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 13:44):

Adam Topaz said:

I don't understand why setoid is a class anyway...

The old answer was "because it's in core".

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 13:53):

def δ2 (q : β r π) : β r π := quotient.lift_on' q (λ a, quotient.mk' $ π a)
(λ x y h, @quotient.sound' _ (thing r π) _ _ (rel.compat h))

Only one @

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 13:53):

but I couldn't get it down to 0

view this post on Zulip Reid Barton (Nov 27 2020 at 13:57):

does this count?

local attribute [elab_with_expected_type] quotient.lift_on'

def δ1 (q : β r π) : β r π := quotient.lift_on' q (λ a, quotient.mk' $ π a)
(λ x y h, quotient.sound' (rel.compat h))

view this post on Zulip Reid Barton (Nov 27 2020 at 13:58):

for nondependent eliminators it's better not to use elab_as_eliminator I think

view this post on Zulip Reid Barton (Nov 27 2020 at 14:02):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/elab_as_eliminator/near/128740170

view this post on Zulip Adam Topaz (Nov 27 2020 at 14:05):

This works too

def δ1 : β r π  β r π := λ x, quotient.lift_on' x (λ a, quot.mk (thing r π).r $ π a)
(λ x y h, quot.sound $ rel.compat h)

view this post on Zulip Adam Topaz (Nov 27 2020 at 14:05):

But the mixing of quot and quotient might make some people uneasy...

view this post on Zulip Reid Barton (Nov 27 2020 at 14:12):

I think the name setoid itself (and not something along the lines of equivalence_relation) partly explains why it would be a class

view this post on Zulip Reid Barton (Nov 27 2020 at 14:13):

but since Lean has quotients, it's sort of a vestigial thing

view this post on Zulip Eric Wieser (Nov 27 2020 at 14:14):

Are there any guidelines for picking between quotient and quot in definitions?

view this post on Zulip Adam Topaz (Nov 27 2020 at 14:17):

One reason (and this is why I'm using quotient in my case) is that I want to use quotient.exact in a proof somewhere in a nontrivial way. And using quot.exact instead would be annoying.

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 14:22):

The definition of the free algebra on a monoid used quot I believe, because after you make the polynomial ring with a variable for every element of the monoid you have a clear idea about which relations you _want_, but you don't have a handle on the equivalence relation generated by those relations, so quot is forced on you.

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 14:23):

https://github.com/leanprover-community/mathlib/blob/f30200e5b17a3265b638103e7d47f8e4c83d6b07/src/linear_algebra/tensor_algebra.lean#L64

view this post on Zulip Adam Topaz (Nov 27 2020 at 14:25):

This is probably a better example:
https://github.com/leanprover-community/mathlib/blob/f30200e5b17a3265b638103e7d47f8e4c83d6b07/src/algebra/free_algebra.lean

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 14:25):

The issue that Amelia ran into with this definition was that now injectivity of MnR[M]M^{\otimes n}\to R[M] was not clear, and with no handle on the actual equivalence relation seemed very difficult to prove.

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 14:26):

Amelia is now making another model for the tensor algebra, as a direct sum of MnM^{\otimes n}. I found it interesting that even with the universal property and an explicit model, one still needed another model in order to prove some theorems (Amelia now has this second model in a branch of mathlib).

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 14:27):

On the other hand, in the representation theory of reductive groups, there is the theory of the Whittaker model and the theory of the Kirillov model, both of which are an explicit function space isomorphic to a given (generic) smooth admissible irreducible complex representation of (say) GL2(Qp)GL_2(\mathbb{Q}_p).

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 14:29):

Another approach would have been to put a grading on the gigantic gadget, proved that all the relations were between things of the same grading, deduced that the associated ideal was graded and then got an induced grading on the quotient.

view this post on Zulip Eric Wieser (Nov 27 2020 at 14:35):

Kevin Buzzard said:

The issue that Amelia ran into with this definition was that now injectivity of MnR[M]M^{\otimes n}\to R[M] was not clear, and with no handle on the actual equivalence relation seemed very difficult to prove.

I think I made a start on trying to prove this in #5034 via docs#free_algebra.equiv_monoid_algebra_free_monoid, but somehow got waylaid trying to prove docs#free_abelian_group.of was injective, which I couldn't do but also don't remember why I needed

view this post on Zulip Eric Wieser (Nov 27 2020 at 14:36):

But that's ultimately the case you describe, of needing another model

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 14:42):

I was quite surprised by this from a psychological point of view -- the model in my head was that the universal property tells you that there's at most one object with the properties you want, and the construction -- any construction -- tells you that there's at least one. Here there seemed to be a benefit of more than one construction.

view this post on Zulip Adam Topaz (Nov 27 2020 at 14:45):

The direct sum representation of the tensor algebra comes with its own headaches, right? For example, in proving associativity you need to show that two terms in a dependent type T n, n : nat, are equal for n = (a + b) + c and n = a + (b + c).

view this post on Zulip Adam Topaz (Nov 27 2020 at 14:45):

How did you avoid heq in this case?

view this post on Zulip Eric Wieser (Nov 27 2020 at 14:51):

In my experience facing that, the proofs aren't impossible, it just makes your theorem statement ugly

view this post on Zulip Eric Wieser (Nov 27 2020 at 14:53):

And using heq is not the end of the world

view this post on Zulip Kenny Lau (Nov 27 2020 at 14:58):

Eric Wieser said:

Kevin Buzzard said:

The issue that Amelia ran into with this definition was that now injectivity of MnR[M]M^{\otimes n}\to R[M] was not clear, and with no handle on the actual equivalence relation seemed very difficult to prove.

I think I made a start on trying to prove this in #5034 via docs#free_algebra.equiv_monoid_algebra_free_monoid, but somehow got waylaid trying to prove docs#free_abelian_group.of was injective, which I couldn't do but also don't remember why I needed

import group_theory.free_abelian_group

universe u

namespace free_abelian_group

open_locale classical

lemma of_injective (α : Type u) : function.injective (of : α  free_abelian_group α) :=
λ x y hoxy, classical.by_contradiction $ assume hxy : x  y,
let f : free_abelian_group α →+  := lift (λ z, if x = z then 1 else 0) in
have hfx1 : f (of x) = 1, from (lift.of _ _).trans $ if_pos rfl,
have hfy1 : f (of y) = 1, from hoxy  hfx1,
have hfy0 : f (of y) = 0, from (lift.of _ _).trans $ if_neg hxy,
one_ne_zero $ hfy1.symm.trans hfy0

end free_abelian_group

view this post on Zulip Adam Topaz (Nov 27 2020 at 15:01):

You can play the same trick to prove the map from M to the tensor algebra is injective by mapping into the square-zero algebra generrated by M.

view this post on Zulip Kenny Lau (Nov 27 2020 at 15:02):

#5109

view this post on Zulip Kenny Lau (Nov 27 2020 at 15:02):

but this doesn't scale to MnM^{\otimes n} -- you might as well have used the direct sum construction

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 15:03):

Amelia has been dealing with heq. Chris Hughes knows some techniques for taming heq, he has been working with it for years, and Chris and Amelia are amongst a group of Imperial students all living in the same house share at the minute, so she's in a great position to pick up tips!

view this post on Zulip Eric Wieser (Nov 27 2020 at 15:04):

@Kenny, is that PR'd anywhere?

view this post on Zulip Kenny Lau (Nov 27 2020 at 15:06):

is what PR'd anywhere?

view this post on Zulip Eric Wieser (Nov 27 2020 at 15:06):

The code snippet you pasted

view this post on Zulip Eric Wieser (Nov 27 2020 at 15:10):

(I now remember that I wanted to prove that in order to prove that docs#free_ring.of was injective)

view this post on Zulip Kenny Lau (Nov 27 2020 at 15:13):

no, it is not PR'd anywhere

view this post on Zulip Kenny Lau (Nov 27 2020 at 15:13):

feel free to PR it

view this post on Zulip Eric Wieser (Nov 27 2020 at 15:20):

#5131

view this post on Zulip Eric Wieser (Nov 27 2020 at 16:01):

Thanks for the hint @Kenny Lau, that strategy works to prove that free_algebra.ι is injective too

view this post on Zulip Kenny Lau (Nov 27 2020 at 16:01):

great

view this post on Zulip Eric Wieser (Nov 27 2020 at 16:03):

Kenny Lau said:

but this doesn't scale to MnM^{\otimes n} -- you might as well have used the direct sum construction

What is MnM^{\otimes n}?

view this post on Zulip Eric Wieser (Nov 27 2020 at 16:03):

Assuming that's just the nn-th tensor powers, I don't see where the direct sum fits in

view this post on Zulip Kenny Lau (Nov 27 2020 at 16:04):

because F(M)=n=0MnF(M) = \bigoplus_{n=0}^\infty M^{\otimes n}

view this post on Zulip Eric Wieser (Nov 27 2020 at 16:07):

Oh, were you talking about proving the injectivity of MnF(M)M^{\otimes n} \to F(M), which is difficult if you only have the universal property of F(M)F(M)?

view this post on Zulip Kenny Lau (Nov 27 2020 at 16:08):

yes

view this post on Zulip Eric Wieser (Nov 27 2020 at 16:09):

Well thankfully we can't even state that yet using the definitions currently in mathlib...

view this post on Zulip Eric Wieser (Jan 12 2021 at 17:00):

Adam Topaz said:

You can play the same trick to prove the map from M to the tensor algebra is injective by mapping into the square-zero algebra generrated by M.

Done in #5712. Handily this works for the exterior_algebra too.


Last updated: May 09 2021 at 19:11 UTC