## Stream: general

### Topic: by exact works, but not the term itself

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


#### 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?

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

#### Adam Topaz (Nov 27 2020 at 04:39):

That makes sense. Thanks @Bryan Gin-ge Chen

#### Kenny Lau (Nov 27 2020 at 05:54):

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

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

#### Eric Wieser (Nov 27 2020 at 08:23):

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

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

#### Adam Topaz (Nov 27 2020 at 13:18):

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

#### Eric Wieser (Nov 27 2020 at 13:24):

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

Oh

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

#### 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))  #### Eric Wieser (Nov 27 2020 at 13:27): Because it prevents quotient.sound' using typeclass search to find the setoid #### Adam Topaz (Nov 27 2020 at 13:28): quotient.sound' has no [...] in its type #### 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. #### Adam Topaz (Nov 27 2020 at 13:29): @Kevin Buzzard just for a sanity check #### Kevin Buzzard (Nov 27 2020 at 13:29): quotient.sound uses typeclasses to find the equivalence relation, quotient.sound' uses unification. #### Kevin Buzzard (Nov 27 2020 at 13:30): typeclasses are not appropriate here because the equivalence relation depends on the variable π. #### Adam Topaz (Nov 27 2020 at 13:31): And it's strange that @Eric Wieser 's definition works! #### 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 #### Eric Wieser (Nov 27 2020 at 13:31): def pre (π : α → α) := α would give you something you can stick a typeclass on #### Kevin Buzzard (Nov 27 2020 at 13:31): Why is it strange? He's filling in the relation. #### Adam Topaz (Nov 27 2020 at 13:32): Oh nevermind thats right #### 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


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

#### Reid Barton (Nov 27 2020 at 13:32):

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

#### Reid Barton (Nov 27 2020 at 13:33):

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

#### Adam Topaz (Nov 27 2020 at 13:34):

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

#### Reid Barton (Nov 27 2020 at 13:34):

Lean is not a human

#### Kevin Buzzard (Nov 27 2020 at 13:34):

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

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

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

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

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

#### 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'

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

#### Adam Topaz (Nov 27 2020 at 13:41):

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

#### Reid Barton (Nov 27 2020 at 13:44):

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

#### Reid Barton (Nov 27 2020 at 13:44):

I guess it just never came up before

#### Kevin Buzzard (Nov 27 2020 at 13:44):

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

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

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 (Nov 27 2020 at 13:53): but I couldn't get it down to 0 #### 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))


#### Reid Barton (Nov 27 2020 at 13:58):

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

#### Reid Barton (Nov 27 2020 at 14:02):

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

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


#### Adam Topaz (Nov 27 2020 at 14:05):

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

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

#### Reid Barton (Nov 27 2020 at 14:13):

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

#### Eric Wieser (Nov 27 2020 at 14:14):

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

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

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

#### Kevin Buzzard (Nov 27 2020 at 14:23):

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

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

#### Kevin Buzzard (Nov 27 2020 at 14:25):

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 (Nov 27 2020 at 14:26):

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

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

#### 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 $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 (Nov 27 2020 at 14:36):

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

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

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

#### Adam Topaz (Nov 27 2020 at 14:45):

How did you avoid heq in this case?

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

#### Eric Wieser (Nov 27 2020 at 14:53):

And using heq is not the end of the world

#### 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 $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 (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.

#5109

#### Kenny Lau (Nov 27 2020 at 15:02):

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

#### 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!

#### Eric Wieser (Nov 27 2020 at 15:04):

@Kenny, is that PR'd anywhere?

#### Kenny Lau (Nov 27 2020 at 15:06):

is what PR'd anywhere?

#### Eric Wieser (Nov 27 2020 at 15:06):

The code snippet you pasted

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

#### Kenny Lau (Nov 27 2020 at 15:13):

no, it is not PR'd anywhere

#### Kenny Lau (Nov 27 2020 at 15:13):

feel free to PR it

#5131

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

great

#### Eric Wieser (Nov 27 2020 at 16:03):

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 (Nov 27 2020 at 16:03):

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

#### Kenny Lau (Nov 27 2020 at 16:04):

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

#### Eric Wieser (Nov 27 2020 at 16:07):

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

yes

#### Eric Wieser (Nov 27 2020 at 16:09):

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

#### Eric Wieser (Jan 12 2021 at 17:00):

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.