I'm trying to use Lean to prove congruence modulo a subgroup K of a group G is an equivalence relation. I'm working pretty closely off of the example given in Sheet 1 of Section 6 of the Formalizing Mathematics worksheets.
First, I've imported the following at the top of my file:
import tactic
import group_theory.subgroup.basic
import group_theory.coset
import data.fintype.basic
import data.fintype.card
I've set up my group G and subgroup K with these lines:
variables {G : Type} [group G] [fintype G]
variables [K : subgroup G] [fintype K]
Buzzard's setup is as follows (Lean likes this and knows how to handle it):
def R (a b : ℤ) : Prop :=
∃ z : ℤ, a - b = 37 * z
lemma R_def (a b : ℤ) : R a b ↔ ∃ z : ℤ, a - b = 37 * z :=
begin
refl,
end
I've modified to be:
def R (g h : G) : Prop :=
∃ (k : K), g = k * h
lemma R_def (g h : G) : R g h ↔ ∃ (k : K), g = k * h :=
begin
refl,
end
But now get the following error:
failed to synthesize type class instance for
G : Type,
_inst_1 : group G,
_inst_2 : fintype G,
K : subgroup G,
_inst_3 : fintype ↥K,
g h : G
⊢ subgroup G
g : G
Running #check R yields R : ?M_1 → ?M_1 → Prop, so it seems like Lean can't recognize my group G for whatever reason? Running #check G gives G: Type and doing #check ℤ also gives ℤ : Type, so I don't see why Buzzard's example for ℤ doesn't work for my group G. Any help would be much appreciated!
variables [K : subgroup G] is no good, because subgroup is not a class.
The way classes work is that if C x y z is a class, there is only ever supposed to be one term of type C x y z. The square bracket system (the "typeclass inference system") works under this assumption. For example you don't particularly want two proofs that a type is finite, and you usually don't want two multiplicative group structures on a type, so group G and fintype X are classes. However there are definitely lots of cases where you want to have more than one subgroup of a group, so subgroup G is a structure but not a class. This means that it's not the typeclass inference system's job to keep track of subgroups of a group, so you want to do variable (K : subgroup G) and then R will be a function of K (makes sense, right? There is one equivalence relation per subgroup).
This works:
import tactic
import group_theory.subgroup.basic
variables {G : Type} [group G]
variables (K : subgroup G)
def R (g h : G) : Prop :=
∃ (k : K), g = k * h
lemma R_def (g h : G) : R K g h ↔ ∃ (k : K), g = k * h :=
begin
refl,
end
Note that I'm writing R K not R. Note also that I've removed the finiteness assumptions: idiomatic Lean code is to only put in the assumptions where you need them, so maybe you'll need them later on depending on what you're going to do, but you definitely don't need them for defining the equivalence relation so they shouldn't be there yet.