Extension showing goal for a separate lemma

Stream: general

[Yakov Pechersky]

I have tried to work this down to a #mwe. Deleting any line or inserting empty lines will remove this bug. It might be only on my VSCode and extension version. Unclear.

In a new file, paste the following. Place your cursor on the comma indicated. The goal shown has nothing to do with the lemma being proved at that point.

import data.fin
import data.matrix.notation
import tactic.ring_exp

open_locale big_operators

variables {n : ℕ} {R : Type*} [field R]

variables {A : matrix (fin (n + 2)) (fin (n + 2)) R}

-- example : (∑ x, ∑ y, A 0 x * (-1) ^ (x : ℕ) * A 1 (x.succ_above y) * (-1) ^ (y : ℕ)) =
--           -(∑ x, ∑ y, A 1 x * (-1) ^ (x : ℕ) * A 0 (x.succ_above y) * (-1) ^ (y : ℕ)) :=
-- begin
--   simp_rw ←finset.sum_neg_distrib,
--   ring_exp,
--   rw fin.sum_univ_cast_succ,
--   rw @fin.sum_univ_cast_succ _ _ (n + 1),
--   congr,
--   ext x,
--   congr' 1 with y,
--   simp,
--   swap,
--   ext y,
--   simp,
-- end


lemma inv_ite {α : Type*} (P : Prop) [decidable P] (f : α → α) (hinv : function.involutive f) (x : α) :
  ite P x (f x) = f (ite (¬ P) (x) (f x)) :=
begin
  rw apply_ite f,
  by_cases h : P,
  { rw [if_pos h, if_neg (not_not.mpr h), hinv x] },
  { rw [if_pos h, if_neg h] },
end

example (k : R) (x y : ℕ) (hne : x ≠ y) : ite (y < x) (k : R) (-k) = - ite (x < y) k (-k) :=
begin
  rw inv_ite _ _ neg_involutive,
  rcases (lt_trichotomy x y) with h|h|h,
  { rw [if_pos h, if_pos],
    exact (not_lt_of_lt h) },
  { exact absurd h hne },
  { rw [if_neg (not_lt_of_lt h), if_neg],
    exact (not_not.mpr h) }
end

lemma test (k : R) (x y : ℕ) (hne : x ≠ y) : ite (y < x) (k : R) (-k) = - ite (x < y) k (-k) :=
begin
  rw inv_ite _ _ neg_involutive,
  rcases (lt_trichotomy x y) with h|h|h,
  { rw [if_pos h, if_pos],
    exact (not_lt_of_lt h) },
  { exact absurd h hne },
  { rw [if_neg (not_lt_of_lt h), if_neg],
    exact (not_not.mpr h) }
end

example (x : fin (n + 1)) (y : fin n) : (-1 : R) ^ (x : ℕ) * (-1) ^ ((x.succ_above y) : ℕ)
  = (-1) ^ ((x + y) : ℕ) * ite ((y : ℕ) < x) 1 (-1) :=
begin
  unfold fin.succ_above,
  rw apply_ite coe,
  convert test ((-1 : R) ^ ((x + y) : ℕ)) x (x.succ_above y) (fin.vne_of_ne (fin.succ_above_ne x y).symm),
  simp [pow_add, fin.succ_above], --place cursor on terminal comma
end

example : (∑ x : fin (n + 2), ∑ y : fin (n + 1), A 0 (x.succ_above y)) = ∑ x, ∑ y, ite (x ≠ y) (A 0 y) 0 :=
begin
  congr' 1 with x,
end

[Yakov Pechersky]

image.png

[Reid Barton]

I can reproduce this in emacs, so I think it's a Lean server mode bug. It seems to be very sensitive to the exact positions involved.

[Johan Commelin]

Oooh wow, if it is reproducable in emacs...

[Johan Commelin]

I mean, then it must be a feature instead of a bug, right?

[Yakov Pechersky]

My guess is that it has something to do with congr' 1 with x.

[Yakov Pechersky]

Because adding more lines to the last proof retains the bug

[Floris van Doorn]

This looks like a problem with the pattern `[ ... ] used in the definition on tactic.congr'.

[Floris van Doorn]

Note that the bug only happens on line 65, column 33, which is exactly the place where the first `[ ... ] occurs in the definition of tactic.congr'.

[Floris van Doorn]

and indeed, it also happens on line 66, column 17, which is another occurrence of `[ ... ] .

[Mario Carneiro]

wow, how did you notice that? o.O

[Floris van Doorn]

Mostly by minimizing the example further (emptying lines above the occurrence), trying to replace it with a simpler tactic (the bug still happened with tactic.congr' instead of congr'), and then suspiciously it didn't happen when I defined tactic.congr2 with the same implementation as tactic.congr'.

[Johan Commelin]

Whut? This is really sick... Kudos to Floris!

[Bryan Gin-ge Chen]

(Lean issue: lean#468)