Lean cannot show `1 = 1`

Stream: new members

[Hanting Zhang]

There is a weird bug where Lean cannot understand that 1 = 1. I'm somewhat aware that this is has something to do with Lean not inferring the correct instances... I think? Anyways, what is the best way to debug things of type a = a? There are several more of these in my half-done proof. :cry:

import ring_theory.polynomial.basic

universes u v
open_locale big_operators
open polynomial finset

namespace vieta

variables {α : Type u} [comm_ring α] [integral_domain α]
variables {n : ℕ} {r : ℕ → α} {f : polynomial α}

noncomputable instance has_coe_poly : has_coe α (polynomial α) := ⟨λ a, monomial 0 a⟩

@[simp] lemma powerset_len_zero {α : Type u}(s : finset α) : powerset_len 0 s = {∅} := by sorry

lemma coeff_poly_from_roots :
  ∀ (k : ℕ), k ≤ n → coeff (∏ i in range n, (X - (r i : polynomial α))) k
  = ∑ A in (powerset_len (n - k) (range n)), (∏ j in A, r j) :=
begin
  induction n with n ih,
  { simp only [nat.nat_zero_eq_zero, le_zero_iff_eq, nat.zero_sub, forall_eq, range_zero],
    rw [prod_empty, coeff_one_zero, powerset_len_zero ∅, sum_singleton, prod_empty],
    sorry }, -- 1 = 1 ???
  { sorry }
end

end vieta

[Alex J. Best]

By adding the assumptions comm_ring and integral_domainyou've inadvertently put two ring structures on the same type, this is not good and will lead to all sorts of problems like this, try removing the comm_ring assumption, as it is implied by integral domain

[Kenny Lau]

you can also find out that the 1 comes from different ring structures by clicking enough things in the infoview.

[Alex J. Best]

(deleted)

[Johan Commelin]

@Hanting Zhang there are different ways of defining new instances in lean/mathlib. We have instances of the form:

• R is a ring
• R is an integral domain
• G is a group
• K is a field

but also instances of the form

• topological_group G, which mean: assume that in the context there is [topological_space G] and [group G], and then [topological_group G] will assert that these two assumptions play well together: addition and inverse are continuous

[Johan Commelin]

So in the latter case, you will write [topological_space G] [group G] [topological_group G] and this will not put two different group structures on G.

[Hanting Zhang]

@Kenny Lau Hmm... I don't see any difference when clicking through. Is there some second layer of meta-data I should be able to see?

[Johan Commelin]

But in the former case, writing [ring R] and [integral_domain R] will put two ring structures on R that have nothing to do with each other. In particular, you can't prove 1 = 1.

[Bryan Gin-ge Chen]

Kenny Lau said:

you can also find out that the 1 comes from different ring structures by clicking enough things in the infoview.

You have to click quite a bit, but it works!

Screen-Shot-2021-01-06-at-3.39.56-AM.png

Screen-Shot-2021-01-06-at-3.40.32-AM.png

[Kenny Lau]

2021-01-06-9.png 2021-01-06-8.png

[Hanting Zhang]

Ah ok. @Johan Commelin Thanks for the explanation. I suspected it might have something to do with instances. Is there any way to check if instances play well together?

[Johan Commelin]

you'll have to check their definitions

[Johan Commelin]

you'll notice that integral_domain uses extends comm_ring, whereas topological_group has assumptions [topological_space G] before the colon.

[Hanting Zhang]

Ok, that makes sense, thanks!

[Kevin Buzzard]

I'm afraid that right now you have to look these things up yourself, and we see this sort of mistake often made by beginners, because they are in no position to figure it out themselves and we're not doing very well at documenting/explaining it right now. Sorry.

[Kenny Lau]

or you can try removing the comm_ring instance and see if Lean complains about it.

[Eric Wieser]

If you run the congr tactic on your 1=1 goal, I think it would have revealed the problem and saved you the clicks

[Johan Commelin]

but that assumes you know about the congr tactic... :wink: