Zulip Chat Archive

Stream: new members

Topic: dependent rewrite


Joachim Breitner (Jan 21 2022 at 18:23):

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 (Jan 21 2022 at 18:26):

Can you give a #mwe ?

Yakov Pechersky (Jan 21 2022 at 18:28):

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 (Jan 21 2022 at 18:29):

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

Yakov Pechersky (Jan 21 2022 at 18:29):

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

Adam Topaz (Jan 21 2022 at 18:32):

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 (Jan 21 2022 at 18:32):

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

Adam Topaz (Jan 21 2022 at 18:33):

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

Yakov Pechersky (Jan 21 2022 at 18:33):

Ah

Yakov Pechersky (Jan 21 2022 at 18:34):

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 (Jan 21 2022 at 18:37):

It feels a bit hacky to me :)

Joachim Breitner (Jan 21 2022 at 18:39):

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

Kevin Buzzard (Jan 21 2022 at 18:40):

yeah, that error is common in these situations.

Adam Topaz (Jan 21 2022 at 18:40):

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 (Jan 21 2022 at 18:40):

(With a better name, of course ;))

Yakov Pechersky (Jan 21 2022 at 18:42):

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

Kevin Buzzard (Jan 21 2022 at 18:43):

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 (Jan 21 2022 at 18:43):

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

Joachim Breitner (Jan 21 2022 at 18:44):

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 (Jan 21 2022 at 18:45):

@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 (Jan 21 2022 at 18:46):

I see

Adam Topaz (Jan 21 2022 at 18:52):

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 (Jan 21 2022 at 19:03):

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

Joachim Breitner (Jan 21 2022 at 19:05):

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 (Jan 21 2022 at 19:07):

So indeed,

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

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

Joachim Breitner (Jan 21 2022 at 19:10):

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 (Jan 21 2022 at 19:35):

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


Last updated: Dec 20 2023 at 11:08 UTC