## Stream: general

### Topic: result contains metavariables

#### Kevin Buzzard (Mar 18 2020 at 20:46):

I've been around for long enough to have seen the situation where you have no goals but end doesn't work because

tactic failed, result contains meta-variables
state:
no goals


You can try and get out of this hole with the recover tactic.

I've been playing with the category theory library this evening, and something pretty cool happened, and I have no idea why. We're in one of these situations where the goal should be relatively straightforward when you work out what it says. My strategy in such situations is to do a mass of unfolding, and when dsimp suddenly tidies a bunch of stuff up, save my position with show [blah] and then press on. So I managed to fill in a sorry this evening, and my first complete proof looked like this:

@[simp]
lemma right_unitor_hom {M : Module R} (r : R) (m : M) :
((ρ_ M).hom : M ⊗ 𝟙_ (Module R) ⟶ M) (m ⊗ₜ r) = r • m :=
begin
show (linear_equiv.to_linear_map (tensor_product.rid R ↥M)) (m ⊗ₜ[R] r) = r • m,
dunfold tensor_product.rid,
dunfold tensor_product.comm,
unfold_coes,
unfold linear_map.flip,
unfold_coes,
unfold linear_map.mk₂,
unfold tensor_product.mk,
dsimp,
unfold_coes,
--  unfold tensor_product.lift,
unfold linear_equiv.of_linear,
unfold linear_equiv.trans,
dunfold linear_equiv.to_linear_map,
dsimp,
unfold tensor_product.lid,
unfold linear_equiv.of_linear,
dsimp,
unfold_coes,
unfold linear_map.lsmul,
unfold linear_map.mk₂,
dsimp,
squeeze_simp, -- tensor_product.lift.tmul used here
show (tensor_product.lift
{to_fun := λ (a : R), {to_fun := λ (m : ↥M), a • m, add := _, smul := _}, add := _, smul := _}).to_fun
(r ⊗ₜ[R] m) =
r • m,
squeeze_simp, -- tensor_product.lift.tmul'
refl,
end


This proof is actually just two lines long -- each squeeze_simp just does one rewrite (tmul and tmul' are definitionally equal, one has to_fun in and the other has a coercion), and all the definitional unfolding is just to get things into a shape where the rewrite can happen. This proof compiles no problem. So then I refactored the proof so it was just show X, rw tensor_product.lift.tmul', show Y, rw tensor_product.lift.tmul':

lemma right_unitor_hom {M : Module R} (r : R) (m : M) :
((ρ_ M).hom : M ⊗ 𝟙_ (Module R) ⟶ M) (m ⊗ₜ r) = r • m :=
begin
show (tensor_product.lift
{to_fun := λ (a : R), {to_fun := λ (m : ↥M), a • m, add := _, smul := _}, add := _, smul := _}).to_fun
((tensor_product.lift
{to_fun := λ (m : ↥M), {to_fun := λ (m_1 : R), m_1 ⊗ₜ[R] m, add := _, smul := _},
smul := _}).to_fun
(m ⊗ₜ[R] r)) =
r • m,
rw tensor_product.lift.tmul',
show (tensor_product.lift
{to_fun := λ (a : R), {to_fun := λ (m : ↥M), a • m, add := _, smul := _}, add := _, smul := _}).to_fun
(r ⊗ₜ[R] m) =
r • m,
rw tensor_product.lift.tmul',
refl, -- no goals!
end


and I got the result contains metavariables error. I was really surprised when I tried recover though -- four goals, some of which weren't definitional. I killed them all and still I got the error! A second recover and they were finally gone. My proof ended up looking like this:

lemma right_unitor_hom {M : Module R} (r : R) (m : M) :
((ρ_ M).hom : M ⊗ 𝟙_ (Module R) ⟶ M) (m ⊗ₜ r) = r • m :=
begin
show (tensor_product.lift
{to_fun := λ (a : R), {to_fun := λ (m : ↥M), a • m, add := _, smul := _}, add := _, smul := _}).to_fun
((tensor_product.lift
{to_fun := λ (m : ↥M), {to_fun := λ (m_1 : R), m_1 ⊗ₜ[R] m, add := _, smul := _},
smul := _}).to_fun
(m ⊗ₜ[R] r)) =
r • m,
rw tensor_product.lift.tmul',
show (tensor_product.lift
{to_fun := λ (a : R), {to_fun := λ (m : ↥M), a • m, add := _, smul := _}, add := _, smul := _}).to_fun
(r ⊗ₜ[R] m) =
r • m,
rw tensor_product.lift.tmul',
refl, -- no goals!
recover, -- four goals!
simp, intros, congr', intros, ext, simp, apply tensor_product.tmul_add, -- no goals!
recover, -- two goals!
intros, rw tensor_product.smul_tmul c x m_1, simp, intros, apply tensor_product.add_tmul,
end


My question: How come I managed to avoid these six secret metavariables in my first proof? Where did they come from?

One cannot immediately reproduce this at home, but because of the new tooling it is much easier than before. The following commands (run in a directory where there's not a subdirectory called mathlib):

leanproject get mathlib
cd mathlib/
git checkout enriched
leanproject get-cache


will give you Scott's branch, fully compiled. The right_unitor_hom lemma is on line 149 of src/algebra/category/Module/monoidal.lean




#### Kevin Buzzard (Mar 18 2020 at 21:17):

Some of the random goals are I think the add := _ and smul := _. I tried replacing the first show with

  show (tensor_product.lift
{to_fun := λ (a : R), {to_fun := λ (m : ↥M), a • m, add := _, smul := _}, add := _, smul := _}).to_fun
((tensor_product.lift
{to_fun := _,
smul := _}).to_fun
(m ⊗ₜ[R] r)) =
r • m,


and I get

LEAN ASSERTION VIOLATION
File: /home/travis/build/leanprover-community/lean/src/frontends/lean/elaborator.cpp
Line: 3174
m_ctx.match(e, *val2)


Something is a bit weird here.

#### Bryan Gin-ge Chen (Mar 18 2020 at 21:18):

Looks like https://github.com/leanprover-community/lean/issues/123 again.

#### Kevin Buzzard (Mar 18 2020 at 21:22):

no, you can do set-theoretic trickery. Wait, we're on the wrong thread.

Last updated: May 16 2021 at 21:11 UTC