Zulip Chat Archive

Stream: general

Topic: Type class inference in forall


Arnoud van der Leer (Apr 25 2021 at 07:18):

Hi there, it's me again. I am trying to prove an equivalence about fields. One of these says "if R is a field, all morphisms to nonzero rings S are injective".

import algebra.field

universes u v

lemma p2 {R: Type u} [comm_ring R] (exists_pair_ne :  (x y : R), x  y) (h: is_field R) :  {S: Type v} [comm_ring S] (f: R →+* S), function.injective f := begin
  sorry,
end

However, Lean does not compile the (f: R →+* S) part with an error

failed to synthesize type class instance for
R : Type u,
_inst_1 : comm_ring R,
exists_pair_ne :  (x y : R), x  y,
h : is_field R,
S : Type v,
_inst_2 : comm_ring S
 semiring SLean

How should I fix this?

Note that the forall is part of a tfae, so I won't be able to get S and [comm_ring S] out of the forall.

Mario Carneiro (Apr 25 2021 at 07:19):

You need by exactI to pick up typeclass instances in binders

Mario Carneiro (Apr 25 2021 at 07:19):

lemma p2 {R: Type u} [comm_ring R] (exists_pair_ne :  (x y : R), x  y) (h: is_field R) :
   {S: Type v} [comm_ring S], by exactI  (f: R →+* S), function.injective f :=
begin
  ...

Arnoud van der Leer (Apr 25 2021 at 07:20):

That works. Thank you!

Kevin Buzzard (Apr 25 2021 at 08:03):

exists_pair_ne already exists in Lean, it's called something like nontrivial, but here you don't need it at all because it's implied by is_field.

Arnoud van der Leer (Apr 25 2021 at 10:05):

Ah, right. In this case it was a remnant of the bigger tfae that I forgot to remove when writing my minimal example.
I'll have a look at nontrivial. I just copied is_field.exists_pair_ne.

Eric Rodriguez (Apr 25 2021 at 10:21):

nontriviality may be helpful - great tactic :)

Anne Baanen (Apr 25 2021 at 12:08):

(Beware that most of the library is designed assuming your parameters look like {R : Type u} [field R] rather than {R : Type u} [comm_ring R] (h : is_field R), so you might save yourself some trouble by switching if that is possible.)


Last updated: Dec 20 2023 at 11:08 UTC