Zulip Chat Archive

Stream: general

Topic: Extension showing goal for a separate lemma


Yakov Pechersky (Sep 08 2020 at 21:05):

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 (Sep 08 2020 at 21:05):

image.png

Reid Barton (Sep 08 2020 at 22:47):

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 (Sep 09 2020 at 04:23):

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

Johan Commelin (Sep 09 2020 at 04:24):

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

Yakov Pechersky (Sep 09 2020 at 12:19):

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

Yakov Pechersky (Sep 09 2020 at 12:19):

Because adding more lines to the last proof retains the bug

Floris van Doorn (Sep 09 2020 at 21:10):

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

Floris van Doorn (Sep 09 2020 at 21:11):

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 (Sep 09 2020 at 21:14):

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

Mario Carneiro (Sep 09 2020 at 22:02):

wow, how did you notice that? o.O

Floris van Doorn (Sep 09 2020 at 22:28):

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 (Sep 10 2020 at 01:37):

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

Bryan Gin-ge Chen (Nov 12 2020 at 21:45):

(Lean issue: lean#468)


Last updated: Dec 20 2023 at 11:08 UTC