result contains metavariables

Stream: general

[Kevin Buzzard]

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 := _},
           add := _,
           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 := _},
           add := _,
           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]

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 := _,
           add := _,
           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
Task: /home/buzzard/Encfs/Computer_languages/Lean/lean-projects/mathlib/src/algebra/category/Module/monoidal.lean: Module.monoidal_category.right_unitor_hom
m_ctx.match(e, *val2)

Something is a bit weird here.

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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