Existsi type mismatch between given term witness and...

Stream: new members

[Sara Fish]

Extremely basic question. In this simple example

def divides (a b : ℤ ) := ∃ k , b = a * k

lemma a_div_a : ∀ (a : ℤ), divides a a :=
begin
  intros a,
  unfold divides,
  existsi 1,
  refl,
end

I get the error

existsi tactic failed, type mismatch between given term witness and expected type

and I am not sure why. Why doesn't the goal turn into this?

 ⊢ ∃ (k : ℤ), a = a * k

After all, the "expected type" should be in ℤ and 1 is in ℤ.

[Andrew Elsey]

Not positive if it will solve your problem, but Lean is finicky about 1's and 0's. I think by default Lean'll assume 1 or 0 is a natural number. You'll have to cast 1 to the type you're expecting (i.e., (1 : Q)). Lifting may also work. It can be misleading as it's just written as 1 or 0 in the goal state, and you'd hope Lean can just figure out which type you're referring to.

[Kevin Buzzard]

existsi is quite a primitive tactic in core Lean which doesn't take any clues from the context about what kind of 1 it needs. If Lean sees a 1 with no extra clues it assumes it's a natural 1. The use tactic is a more sophisticated tactic available in mathlib so if you add import tactic to the top of your file then use 1 will work fine. refl won't work though :-)

[Kyle Miller]

@Sara Fish Elaborating what @Andrew Elsey said, here's how you can fix the proof:

lemma a_div_a : ∀ (a : ℤ), divides a a :=
begin
  intros a,
  unfold divides,
  existsi (1 : ℤ),
  rw mul_one,
end

Here's @Kevin Buzzard's suggestion:

import tactic

lemma a_div_a : ∀ (a : ℤ), divides a a :=
begin
  intros a,
  use 1,
  rw mul_one,
end

[Kyle Miller]

By the way, if a proof starts with intro, it's common practice to put the argument before the colon:

lemma a_div_a (a : ℤ) : divides a a :=
begin
  use 1,
  rw mul_one,
end

[Kyle Miller]

And if you want to compress it even more, you can use the constructor for Exists directly:

lemma a_div_a (a : ℤ) : divides a a := ⟨1, by rw mul_one⟩

Angle brackets are a way to use a constructor without specifying its name. Lean will try to figure out which one you mean.

[Sara Fish]

Thanks all! This was helpful.