rw: equality is not an equality

Stream: general

[Kevin Buzzard]

I've never seen anything like this before. rw h2 on line 26 fails because it claims h2 is not an equality. But it is, and rw h2.symm.symm works fine. What's going on?

def fibZ : ℕ → ℤ
| 0 := 0
| 1 := 1
| (n + 2) := fibZ n + fibZ (n + 1)

@[simp] lemma fibZ_0 : fibZ 0 = 0 := rfl
@[simp] lemma fibZ_1 : fibZ 1 = 1 := rfl
@[simp] lemma fibZ_succ_succ (n : ℕ) : fibZ (n + 2) = fibZ n + fibZ (n + 1) := rfl

lemma induction2 (P : ℕ → Prop) (h0 : P 0) (h1 : P 1)
  (hind : ∀ d : ℕ, P d → P(d+1) → P(d+2)) : ∀ n, P n := sorry

lemma fibZ_m_n (m n : ℕ) : fibZ(m+n+1)=fibZ(m+1)*fibZ(n+1)+fibZ(m)*fibZ(n) :=
begin
  apply induction2 _ _ _ _ n,
  { simp},
  { show fibZ (m + 2) = fibZ (m + 1) * 1 + fibZ m * 1 ,
    rw fibZ_succ_succ,
    simp [add_comm]},
  { -- inductive step
    intros d h1 h2,
    show fibZ (m + (d + 1) + 2) = fibZ (m + 1) * fibZ ((d + 1) + 2) + fibZ m * fibZ (d + 2),
    rw fibZ_succ_succ d,
    rw fibZ_succ_succ (d+1),
    rw fibZ_succ_succ (m+(d+1)),
  --  rw h2, -- "lemma is not an equality or iff"    <---- is this a bug?
    rw h2.symm.symm, -- works fine
    rw [←add_assoc m],
    rw h1.symm.symm,
    simp [mul_add, mul_comm, add_comm, add_assoc, mul_assoc],
    ac_refl,
  }
end

[Mario Carneiro]

it's probably an instantiated metavariable

[Kevin Buzzard]

you mean a variable?

[Mario Carneiro]

no

[Kevin Buzzard]

oh

[Mario Carneiro]

It has type h2 : ?m where ?m := a = b or somesuch

[Kevin Buzzard]

how do I test for this?

[Mario Carneiro]

this is pretty printed as h2 : a = b but rw is fussy about it in this particular case

[Kevin Buzzard]

but pp.all doesn't show it me, right?

[Kevin Buzzard]

simp at h2 before the rewrite fixes it

[Kevin Buzzard]

So did I write bad code to get this situation?

[Kevin Buzzard]

my code looks really innocuous and fine

[Kevin Buzzard]

if I change apply induction2 _ _ _ _ n to refine induction2 _ _ _ _ n the problem goes away

[Chris Hughes]

What is an instantiated metavariable?

[Mario Carneiro]

lemma fibZ_m_n (m n : ℕ) : fibZ(m+n+1)=fibZ(m+1)*fibZ(n+1)+fibZ(m)*fibZ(n) :=
begin
  apply induction2 _ _ _ _ n,
  { simp},
  { show fibZ (m + 2) = fibZ (m + 1) * 1 + fibZ m * 1 ,
    rw fibZ_succ_succ,
    simp [add_comm]},
  { -- inductive step
    intros d h1 h2,
    show fibZ (m + (d + 1) + 2) = fibZ (m + 1) * fibZ ((d + 1) + 2) + fibZ m * fibZ (d + 2),
    rw fibZ_succ_succ d,
    rw fibZ_succ_succ (d+1),
    rw fibZ_succ_succ (m+(d+1)),
    (do t ← tactic.to_expr```(h2) >>= tactic.infer_type,
      -- t ← tactic.instantiate_mvars t, -- uncomment this line
      tactic.trace (expr.to_raw_fmt t)
      -- (app (mvar _mlocal._fresh.378.4796 _mlocal._fresh.378.4796 (const 2 []))
      --   (app (app (app (app (const has_add.add [0]) (const nat [])) (const nat.has_add []))
      --   (local_const 0._fresh.378.6836 d (const 1 []))) (app (app (const has_one.one [0])
      --   (const nat [])) (const nat.has_one []))))
    ),
    -- rw h2, -- "lemma is not an equality or iff"    <---- is this a bug?
    rw h2.symm.symm, -- works fine
    rw [←add_assoc m],
    rw h1.symm.symm,
    simp [mul_add, mul_comm, add_comm, add_assoc, mul_assoc],
    ac_refl,
  }
end

[Mario Carneiro]

expr.to_raw_fmt is like the super verbose version of pp.all

[Mario Carneiro]

it shows you exactly what constructors of the expr type are being used

[Mario Carneiro]

As you can see, it starts (app (mvar ...

[Kenny Lau]

then where is the information stored that ?m_2 is eq?

[Mario Carneiro]

in the local context, not somewhere easily accessible to lean except through builtins like instantiate_mvars

[Kenny Lau]

can we tell intro to instantiate metavariables?

[Mario Carneiro]

I haven't looked at what is causing the problem in the first place in this case

[Mario Carneiro]

The only metavariable that intro instantiates is the goal. It doesn't have to solve any unification problems

[Mario Carneiro]

It might make things clearer to replace the first line with:

  have := induction2 _ _ _ _ n, apply this,

After the have, the state is

5 goals
m n : ℕ,
this : ?m_1 n
⊢ fibZ (m + n + 1) = fibZ (m + 1) * fibZ (n + 1) + fibZ m * fibZ n

m n : ℕ
⊢ ℕ → Prop

m n : ℕ
⊢ ?m_1 0

m n : ℕ
⊢ ?m_1 1

m n : ℕ
⊢ ∀ (d : ℕ), ?m_1 d → ?m_1 (d + 1) → ?m_1 (d + 2)

The thing that will eventually become the type of h2 is here ?m_1 (d + 1)

[Kevin Buzzard]

The problem is somehow with the apply on the first line.

[Kevin Buzzard]

yeah, that. refine fixes it.

[Mario Carneiro]

Because refine knows the expected type, and apply doesn't, elaboration happens in a different order here

[Mario Carneiro]

apply is doing the above two stage process, while refine never creates ?m_1 (d + 1) because it already knows what ?m_1 is

[Kevin Buzzard]

When I saw the underscores I thought about maybe making induction2_on and applying that instead; I don't know if that would have fixed the problem.

[Kevin Buzzard]

[this code is for pedagogical purposes]

[Mario Carneiro]

Notice that the variable in question is pretty far from apply's strike zone. It's in a subterm of a different goal

[Mario Carneiro]

I'm not sure if this is a factor, but there is a performance penalty for instantiate_mvars because it has to traverse the whole term, while most tactics try to keep track of where all the metavariables are so that they don't have to go hunting

[Mario Carneiro]

But the check in rw is just plain broken. It's pattern matching on the expr and assumes that an mvar is not an eq. This is a very common pattern, but it is not safe against rogue terms with instantiated mvars

[Mario Carneiro]

Here's another example that often comes up for me:

example (n : ℕ) (h : n + n ≠ 0) : n ≠ 0 :=
begin
  refine mt (λ hz, _) h,
  rw hz -- rewrite tactic failed, lemma is not an equality nor a iff
end

[Mario Carneiro]

The type of hz is an instantiated metavariable here because it is unknown when it is created by the lambda and is solved by the h to its right

[Patrick Massot]

I think you complain periodically about that one. Couldn't you change that in Lean 3.13?

[Patrick Massot]

(I lost track of what it the next version)

[Mario Carneiro]

instantiated mvars or the rw check?

[Patrick Massot]

The rw check

[Mario Carneiro]

I know nothing about the code in question but it shouldn't be hard

[Patrick Massot]

I think you already found the offending line at some point

[Mario Carneiro]

I'm building lean now, if I can remember how to do that

[Bhavik Mehta]

I've seen this a couple of times but only very recently

[Mario Carneiro]

lean#213

[Reid Barton]

BTW, this "instantiation" is more formally known as zonking