dependent rewrite

Stream: new members

[Joachim Breitner]

I found that I had to write a helper lemma

lemma comap_center_subst {H₁ H₂ : subgroup G} [normal H₁] [normal H₂] (h : H₁ = H₂) :
  comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₂) (center (G ⧸ H₂)) :=
  by { unfreezingI { subst h, } }

because simply rw h in my main proof (where my h is an equality that’s non-trivial on both sides) did not work – presumably because rw replaces just the first occurrence, and then the term becomes ill-typed. Is there a way to do rewrite that can change stuff that appears dependently in the goal?

[Adam Topaz]

Can you give a #mwe ?

[Yakov Pechersky]

In what context do you hope to use this lemma? What about "simp_rw [h]"? The issue is the normal instance isn't simply a target of the rewrite.

[Adam Topaz]

I assume that comap is subgroup.comap and mk' is quotient_group.mk'?

[Yakov Pechersky]

docs#subgroup.comap, docs#subgroup.normal, docs#subgroup.center, docs#quotient_group.mk'

[Adam Topaz]

Cant you use subgroup.ext and some lemma that tells you when something is inside of comap, then rewrite h on the resulting condition?

[Yakov Pechersky]

So this is true regardless of the [normal] instances, right?

[Adam Topaz]

you need normality for $G/H$ to be a group, and hence for mk' to be a homomorphism along which you can comap.

[Yakov Pechersky]

Ah

[Yakov Pechersky]

I don't see what's wrong about unfreezingI in this case, you can go through extensionality in the carrier, of just force the rewrite against the cached typeclass instance.

[Adam Topaz]

It feels a bit hacky to me :)

[Joachim Breitner]

Unfreezing doesn’t help, I still get rewrite tactic failed, motive is not type correct. I’ll try to construct a MWE.

[Kevin Buzzard]

yeah, that error is common in these situations.

[Adam Topaz]

Maybe we could add the following lemma?

@[simp]
lemma mem_comap_center_quotient {H : subgroup G} [normal H] (x : G) :
  x ∈ comap (mk' H) (center (G ⧸ H)) ↔ ∀ g : G, x * g * x⁻¹ * g⁻¹ ∈ H := sorry

[Adam Topaz]

(With a better name, of course ;))

[Yakov Pechersky]

Sorry, I meant subst, not rw. Subst makes sure to do it everywhere

[Kevin Buzzard]

Note that we already have docs#quotient_group.equiv_quotient_of_eq which IIRC was added to get around motive is not type correct errors

[Yakov Pechersky]

If you have a hypothesis of equality, you might as well simplify everything (substitute everywhere) to simplify your goal state

[Joachim Breitner]

MWE:

import group_theory.quotient_group

open subgroup
open quotient_group
example
  {G : Type*}
  [group G]
  {H₁ H₂ : unit -> subgroup G}
  [normal (H₁ ())] [normal (H₂ ())]
  (h : H₁ () = H₂ ())
  : comap (mk' (H₁ ())) ⊤ = comap (mk' (H₂ ())) ⊤ :=
begin rw h,
end

[Joachim Breitner]

@Yakov Pechersky subst only works if it is an equality with a variable on one side? That’s what I can do inside the helper lemma, but not where I actually want to do the rewriting.

[Yakov Pechersky]

I see

[Adam Topaz]

I think we should at some point develop some commutator calculus in groups, so it might be worthwhile to have a lemma expressing the condition in terms of commutators.

[Yakov Pechersky]

Just for those examples, what goal does the congr tactic leave you?

[Joachim Breitner]

11 goals
G: Type ?
_inst_1: group G
H₁H₂: unit → subgroup G
_inst_2: (H₁ ()).normal
_inst_3: (H₂ ()).normal
h: H₁ () = H₂ ()
⊢ H₁ () = H₂ ()
G: Type ?
_inst_1: group G
H₁H₂: unit → subgroup G
_inst_2: (H₁ ()).normal
_inst_3: (H₂ ()).normal
h: H₁ () = H₂ ()
⊢ H₁ () = H₂ ()
G: Type ?
_inst_1: group G
H₁H₂: unit → subgroup G
_inst_2: (H₁ ()).normal
_inst_3: (H₂ ()).normal
h: H₁ () = H₂ ()
⊢ _inst_2 == _inst_3
G: Type ?
_inst_1: group G
H₁H₂: unit → subgroup G
_inst_2: (H₁ ()).normal
_inst_3: (H₂ ()).normal
h: H₁ () = H₂ ()
⊢ H₁ () = H₂ ()
G: Type ?
_inst_1: group G
H₁H₂: unit → subgroup G
_inst_2: (H₁ ()).normal
_inst_3: (H₂ ()).normal
h: H₁ () = H₂ ()
⊢ _inst_2 == _inst_3
G: Type ?
_inst_1: group G
H₁H₂: unit → subgroup G
_inst_2: (H₁ ()).normal
_inst_3: (H₂ ()).normal
h: H₁ () = H₂ ()
⊢ H₁ () = H₂ ()
G: Type ?
_inst_1: group G
H₁H₂: unit → subgroup G
_inst_2: (H₁ ()).normal
_inst_3: (H₂ ()).normal
h: H₁ () = H₂ ()
⊢ H₁ () = H₂ ()
G: Type ?
_inst_1: group G
H₁H₂: unit → subgroup G
_inst_2: (H₁ ()).normal
_inst_3: (H₂ ()).normal
h: H₁ () = H₂ ()
⊢ _inst_2 == _inst_3
G: Type ?
_inst_1: group G
H₁H₂: unit → subgroup G
_inst_2: (H₁ ()).normal
_inst_3: (H₂ ()).normal
h: H₁ () = H₂ ()
⊢ H₁ () = H₂ ()
G: Type ?
_inst_1: group G
H₁H₂: unit → subgroup G
_inst_2: (H₁ ()).normal
_inst_3: (H₂ ()).normal
h: H₁ () = H₂ ()
⊢ H₁ () = H₂ ()
G: Type ?
_inst_1: group G
H₁H₂: unit → subgroup G
_inst_2: (H₁ ()).normal
_inst_3: (H₂ ()).normal
h: H₁ () = H₂ ()
⊢ _inst_2 == _inst_3

[Joachim Breitner]

So indeed,

  congr; try { refl, }; try { exact h }

works in the MWE.
But not in my real example.

[Joachim Breitner]

There, I get remaining goals of type _ == _, and suggest says I should use

exact cast_heq (congr_arg normal (eq.symm ih)) (upper_central_series.subgroup.normal G (nat.succ n)),

which actually works. But is hardly better than the helper lemma :-)

[Yakov Pechersky]

Likely, some less unraveling congr' 2 or something will not go as deep. But Adam's suggestion of proving via extensionality is also always possible to avoid dependent type hell. Or use mathematical statements about isomorphisms using Kevin's definition