prettyprinter and parameters

Stream: general

[Kevin Buzzard]

"Let $G$ be a group, let $H$ be a subgroup. Define an equivalence relation $\sim$ on $G$ by $a\sim b\iff ab^{-1}\in H$. Now let's prove some trivial things".

I am trying to set this up in Lean, ideally using ~ for the equivalence relation because it's what mathematicians are used to. The problem is that the notation depends on H, which can't be inferred, so I need to use H : subgroup G as a parameter, which seems to force me to have G as a parameter as well. Here are two attempts, the first makes notation leak and the second is hilarious :-)

Is there any way I can use notation which depends on a variable or parameter, and get Lean to behave itself?

Aah -- making H implicit as well seems to solve the problem. My instinct is that this might cause me problems later but at least it's a workaround.

/-
Let G be a group and let H be a subgroup. Define an equivalence relation ~ by a ~ b ↔ ab⁻¹ ∈ H. This equivalence relation is reflexive.
-/

structure subgroup (G : Type) [group G] :=
(carrier : set G)
/-
axioms omitted
-/

instance (G : Type) [group G] : has_mem G (subgroup G) := ⟨λ m H, m ∈ H.carrier⟩

section rel1

parameters (G : Type) [group G] (H : subgroup G) -- note (G)

def rel1 : ∀ (a b : G), Prop := λ a b, a * b⁻¹ ∈ H

local notation a ` ~ ` b := rel1 a b -- needs to be local because it depends on H

example : ∀ (a : G), a ~ a :=
begin
  -- ⊢ ∀ (a : G), rel1 a a -- notation was not kept
  sorry
end

end rel1

section rel2

parameters {G : Type} [group G] (H : subgroup G) -- implicit {G}

def rel2 : ∀ (a b : G), Prop := λ a b, a * b⁻¹ ∈ H

local notation a ` ~~ ` b := rel2 a b

example : ∀ (a : G), a ~~ a :=
begin
  -- ⊢ ∀ (a : G), (H ~~ a) a -- wtf??
  sorry
end

end rel2