by exact works, but not the term itself

Stream: general

[Adam Topaz]

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)

[Adam Topaz]

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?

[Bryan Gin-ge Chen]

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.

[Adam Topaz]

That makes sense. Thanks @Bryan Gin-ge Chen

[Kenny Lau]

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Eric Wieser]

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

[Adam Topaz]

Oh

[Eric Wieser]

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

[Eric Wieser]

This works:

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

[Eric Wieser]

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

[Adam Topaz]

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

[Kevin Buzzard]

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.

[Adam Topaz]

@Kevin Buzzard just for a sanity check

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Adam Topaz]

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

[Reid Barton]

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

[Eric Wieser]

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

[Kevin Buzzard]

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

[Adam Topaz]

Oh nevermind thats right

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Adam Topaz]

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

[Reid Barton]

Lean is not a human

[Kevin Buzzard]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Adam Topaz]

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

[Reid Barton]

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

[Reid Barton]

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

[Adam Topaz]

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

[Reid Barton]

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

[Reid Barton]

I guess it just never came up before

[Kevin Buzzard]

Adam Topaz said:

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

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

[Kevin Buzzard]

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 @

[Kevin Buzzard]

but I couldn't get it down to 0

[Reid Barton]

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))

[Reid Barton]

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

[Reid Barton]

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

[Adam Topaz]

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)

[Adam Topaz]

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

[Reid Barton]

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

[Reid Barton]

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

[Eric Wieser]

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

[Adam Topaz]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Adam Topaz]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Amelia is now making another model for the tensor algebra, as a direct sum of $M^{\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).

[Kevin Buzzard]

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) $GL_2(\mathbb{Q}_p)$.

[Kevin Buzzard]

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.

[Eric Wieser]

Kevin Buzzard said:

The issue that Amelia ran into with this definition was that now injectivity of $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

[Eric Wieser]

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

[Kevin Buzzard]

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.

[Adam Topaz]

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).

[Adam Topaz]

How did you avoid heq in this case?

[Eric Wieser]

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

[Eric Wieser]

And using heq is not the end of the world

[Kenny Lau]

Eric Wieser said:

Kevin Buzzard said:

The issue that Amelia ran into with this definition was that now injectivity of $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

[Adam Topaz]

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.

[Kenny Lau]

#5109

[Kenny Lau]

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

[Kevin Buzzard]

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!

[Eric Wieser]

@Kenny, is that PR'd anywhere?

[Kenny Lau]

is what PR'd anywhere?

[Eric Wieser]

The code snippet you pasted

[Eric Wieser]

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

[Kenny Lau]

no, it is not PR'd anywhere

[Kenny Lau]

feel free to PR it

[Eric Wieser]

#5131

[Eric Wieser]

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

[Kenny Lau]

great

[Eric Wieser]

Kenny Lau said:

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

What is $M^{\otimes n}$?

[Eric Wieser]

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

[Kenny Lau]

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

[Eric Wieser]

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

[Kenny Lau]

yes

[Eric Wieser]

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

[Eric Wieser]

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.