Using rw at QuotientGroup

Stream: new members

[张守信(Shouxin Zhang)]

In the example

open Subgroup in
example {G : Type*} [Group G] [IsCyclic G] (g : G):
  letI := IsCyclic.commGroup (α := G)
  letI : Normal (zpowers (g ^ 0)) := by
    exact normal_of_comm _
  G ⧸ (zpowers (g ^ 0)) ≃* G ⧸ (⊥ : Subgroup G) := by
  rw [pow_zero, zpowers_one_eq_bot]

Tactic rw works well, but in the following case

instance {G : Type*} [Group G] [IsCyclic G] (g : G) :
  Subgroup.Normal (Subgroup.zpowers (g ^ 0)) := by
    letI := IsCyclic.commGroup (α := G)
    exact Subgroup.normal_of_comm _

open Subgroup in
example {G : Type*} [Group G] [IsCyclic G] (g : G):
  G ⧸ (zpowers (g ^ 0)) ≃* G ⧸ (⊥ : Subgroup G) := by
  rw [pow_zero, zpowers_one_eq_bot]

Lean will return error : "tactic 'rewrite' failed, motive is not type correct: instNormalZpowersHPowOfNat_exercise g
has type
(zpowers (g ^ 0)).Normal : Prop
but is expected to have type
(zpowers _a).Normal : Prop"

How can I deal with this strange question?

[Robin Arnez]

In new versions, it gives a detailed explanation:

tactic 'rewrite' failed, motive is not type correct:
  fun _a => G ⧸ zpowers _a ≃* G ⧸ ⊥
Error: application type mismatch
  @QuotientGroup.Quotient.group G inst✝¹ (zpowers _a) ⋯
argument
  «instNormalZpowersHPowOfNat_mathlib-demo» g
has type
  (zpowers (g ^ 0)).Normal : Prop
but is expected to have type
  (zpowers _a).Normal : Prop

Explanation: The rewrite tactic rewrites an expression 'e' using an equality 'a = b' by the following process. First, it looks for all 'a' in 'e'. Second, it tries to abstract these occurrences of 'a' to create a function 'm := fun _a => ...', called the *motive*, with the property that 'm a' is definitionally equal to 'e'. Third, we observe that 'congrArg' implies that 'm a = m b', which can be used with lemmas such as 'Eq.mpr' to change the goal. However, if 'e' depends on specific properties of 'a', then the motive 'm' might not typecheck.

Possible solutions: use rewrite's 'occs' configuration option to limit which occurrences are rewritten, or use 'simp' or 'conv' mode, which have strategies for certain kinds of dependencies (these tactics can handle proofs and 'Decidable' instances whose types depend on the rewritten term, and 'simp' can apply user-defined '@[congr]' theorems as well).

tl;dr: rw just does a naive substitution and doesn't for example touch the instance you defined above, because it doesn't take g ^ 0 as a parameter. So it still uses the same instance but now with type zpowers 1, giving a type error. In the version above, it was parameterized because normal_of_comm can take anything, so rw will also substitute that. Whether that works or not very much depends on the situation but if you want to avoid this, usually simp and conv are options; in this case you're probably better off using special functions:

import Mathlib.GroupTheory.SpecificGroups.Cyclic

instance {G : Type*} [Group G] [IsCyclic G] (g : G) :
  Subgroup.Normal (Subgroup.zpowers (g ^ 0)) := by
    letI := IsCyclic.commGroup (α := G)
    exact Subgroup.normal_of_comm _

open Subgroup in
example {G : Type*} [Group G] [IsCyclic G] (g : G):
    G ⧸ (zpowers (g ^ 0)) ≃* G ⧸ (⊥ : Subgroup G) := by
  apply QuotientGroup.quotientMulEquivOfEq
  rw [pow_zero, zpowers_one_eq_bot]

[张守信(Shouxin Zhang)]

Robin Arnez said:

In new versions, it gives a detailed explanation:

tactic 'rewrite' failed, motive is not type correct:
  fun _a => G ⧸ zpowers _a ≃* G ⧸ ⊥
Error: application type mismatch
  @QuotientGroup.Quotient.group G inst✝¹ (zpowers _a) ⋯
argument
  «instNormalZpowersHPowOfNat_mathlib-demo» g
has type
  (zpowers (g ^ 0)).Normal : Prop
but is expected to have type
  (zpowers _a).Normal : Prop

Explanation: The rewrite tactic rewrites an expression 'e' using an equality 'a = b' by the following process. First, it looks for all 'a' in 'e'. Second, it tries to abstract these occurrences of 'a' to create a function 'm := fun _a => ...', called the *motive*, with the property that 'm a' is definitionally equal to 'e'. Third, we observe that 'congrArg' implies that 'm a = m b', which can be used with lemmas such as 'Eq.mpr' to change the goal. However, if 'e' depends on specific properties of 'a', then the motive 'm' might not typecheck.

Possible solutions: use rewrite's 'occs' configuration option to limit which occurrences are rewritten, or use 'simp' or 'conv' mode, which have strategies for certain kinds of dependencies (these tactics can handle proofs and 'Decidable' instances whose types depend on the rewritten term, and 'simp' can apply user-defined '@[congr]' theorems as well).

tl;dr: rw just does a naive substitution and doesn't for example touch the instance you defined above, because it doesn't take g ^ 0 as a parameter. So it still uses the same instance but now with type zpowers 1, giving a type error. In the version above, it was parameterized because normal_of_comm can take anything, so rw will also substitute that. Whether that works or not very much depends on the situation but if you want to avoid this, usually simp and conv are options; in this case you're probably better off using special functions:

import Mathlib.GroupTheory.SpecificGroups.Cyclic

instance {G : Type*} [Group G] [IsCyclic G] (g : G) :
  Subgroup.Normal (Subgroup.zpowers (g ^ 0)) := by
    letI := IsCyclic.commGroup (α := G)
    exact Subgroup.normal_of_comm _

open Subgroup in
example {G : Type*} [Group G] [IsCyclic G] (g : G):
    G ⧸ (zpowers (g ^ 0)) ≃* G ⧸ (⊥ : Subgroup G) := by
  apply QuotientGroup.quotientMulEquivOfEq
  rw [pow_zero, zpowers_one_eq_bot]

I know this answer, but this answer really seems strange, because we must using a theorem to congr , instead of rw directly. simp and conv also failed.

Is there really no simple way to fix this? Or is there something wrong with the way I write instance that prevents Lean from automatically finding motive?

[Robin Arnez]

you probably aren't supposed to use rw, simp or conv here, a MulEquiv is in principle data and rw and stuff is discouraged there because it removes defeq and blocks reduction. That's probably also the reason why QuotientGroup.quotientMulEquivOfEq exists in the first place.