Zulip Chat Archive

Stream: general

Topic: prettyprinter and parameters


Kevin Buzzard (Apr 28 2020 at 11:58):

"Let GG be a group, let HH be a subgroup. Define an equivalence relation \sim on GG by ab    ab1Ha\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

Last updated: Dec 20 2023 at 11:08 UTC