a puzzle

Stream: general

[Kenny Lau]

import tactic.simpa

set_option old_structure_cmd true

class nonzero (α : Type*) [has_zero α] [has_one α] : Prop :=
(zero_ne_one : (0 : α) ≠ 1)

@[simp] theorem one_ne_zero {α : Type*} [has_zero α] [has_one α] [nonzero α] : (1 : α) ≠ 0 :=
nonzero.zero_ne_one.symm

/-- Let's show some example instances -/
instance : nonzero ℕ :=
⟨dec_trivial⟩

/-- Let's show some example instances -/
instance : nonzero ℤ :=
⟨dec_trivial⟩

theorem test {R : Type*} [has_zero R] [has_one R] [nonzero R] : (1 : R) ≠ 0 :=
begin
  intro h,
  have : 1 = 0 := by simpa using h,
  exact one_ne_zero this,
end

[Kenny Lau]

(this is an #mwe)

[Kenny Lau]

question: the type of this is (1 : \N) = 0. what is going on?

[Kenny Lau]

(this is a minimzed version of https://github.com/leanprover-community/mathlib/blob/b013b2d6318b42e5ae49a4a588b1271e37809685/src/algebra/classical_lie_algebras.lean#L80-L89):

lemma sl_non_abelian (h : 1 < fintype.card n) : ¬lie_algebra.is_abelian ↥(sl n R) :=
begin
  rcases fintype.exists_pair_of_one_lt_card h with ⟨i, j, hij⟩,
  let A := Eb R i j hij,
  let B := Eb R j i hij.symm,
  intros c,
  have c' : A.val ⬝ B.val = B.val ⬝ A.val := by { rw [←sub_eq_zero, ←sl_bracket, c.abelian], refl, },
  have : 1 = 0 := by simpa [matrix.mul_val, hij] using (congr_fun (congr_fun c' i) i),
  exact one_ne_zero this,
end

[Johan Commelin]

Kenny Lau said:

question: the type of this is (1 : \N) = 0. what is going on?

Is simpa simply doing too much work?

[Johan Commelin]

Can you trace what it does?

[Kenny Lau]

(I know the answer: that's why the topic is called "a puzzle")

[Johan Commelin]

I see

[Mario Carneiro]

Why wouldn't the type be that? That's what you said it was

[Kenny Lau]

well when you write by simpa [something] using something_else you would suppose that simpa just converts something_else into the goal

[Kenny Lau]

this is kinda an example of an "evil" simpa usage

[Kenny Lau]

it looks like it does the job

[Johan Commelin]

No, I don't expect that

[Kenny Lau]

but it actually does a different job

[Kenny Lau]

this line:
have : 1 = 0 := by simpa [matrix.mul_val, hij] using (congr_fun (congr_fun c' i) i)

[Johan Commelin]

I expect it to simplify the goal as well

[Mario Carneiro]

simpa doesn't constrain the type of the goal at all

[Kenny Lau]

1 goal
n : Type u₁,
R : Type u₂,
h : 1 < fintype.card n,
i j : n,
hij : j ≠ i,
A : ↥(sl n R) := Eb R i j hij,
B : ↥(sl n R) := Eb R j i _,
c : is_abelian ↥(sl n R),
c' : A.val ⬝ B.val = B.val ⬝ A.val
⊢ false

[Mario Carneiro]

in fact I don't think any tactic would be able to stop it from getting the nat default

[Kenny Lau]

that's the tactic state before the line

[Kenny Lau]

when I read the line, I read "apply A * B and B * A to i i and simplify both sides to obtain 1 = 0"

[Kenny Lau]

as one would when reading that line

[Mario Carneiro]

I'm sayinh that when you write have : 1 = 0 := by ... lean has already decided that 1 is 1 : nat

[Kenny Lau]

I'm saying the one who wrote that line likely had that intention

[Kenny Lau]

and it accidentally worked

[Mario Carneiro]

sure, simp proves lots of surprise theorems

[Kenny Lau]

hey @Oliver Nash is online

[Mario Carneiro]

you are saying that simpa was able to unify (1 : nat) = 0 and (1 : R) = 0 because they are both false

[Kenny Lau]

right

[Mario Carneiro]

sounds legit

[Kenny Lau]

I'm just observing that this is a surprise

[Oliver Nash]

Kenny Lau said:

hey Oliver Nash is online

He is but he is also working so he shouldn't even be glancing at this thread! I will study it over lunch.

[Oliver Nash]

Kenny Lau said:

I'm saying the one who wrote that line likely had that intention

Just reading this more carefully now. I can at least confirm the intention of the one who wrote that line was as you suggest: mentally I was parsing 1 = 0 as (1: R) = 0 and thus had a bit of a difference of opinion with Lean which parses it as (1 : ℕ) = 0.

[Oliver Nash]

So I suppose what's happening in sl_non_abelian is that the simpa statement in fact succeeds in proving false given its hypotheses by using one_ne_zero but for R. It then uses this to prove what it was asked, namely (1 : ℕ) = 0. And then, rather ridiculously, we prove false again using one_ne_zero but for ℕ rather than R this time.

[Kenny Lau]

right

[Oliver Nash]

Indeed this seems right since I can replace the last two lines of that lemma with:

simpa [matrix.mul_val, hij] using (congr_fun (congr_fun c' i) i),

This is obviously better than the rather hilarious proof in place at present but I propose it might be best to finish as:

  have : (1 : R) = 0 := by simpa [matrix.mul_val, hij] using (congr_fun (congr_fun c' i) i),
  exact one_ne_zero this,

[Oliver Nash]

I can include this tidy up as part of some future PR, or else you might wish to just go for it right now?

[Oliver Nash]

Great find! I must now dash out for my lunchtime run.

[Kenny Lau]

I guess either way is ok