Induction over a generalised type · Beginner Questions

I am posting this here in addition to my mailing list email from yesterday. In short, I am working on a proof, which
inducts over all abelian groups and passes to the quotient group in one of the cases during the induction step. This creates a type issue even if
generalizing the group itself since the types of elements of the quotient group and the original group are different. I have come up with a short minimal working example to illustrate the proof with a short sketch:

theory Scratch
  imports Complex_Main
  "Jacobson_Basic_Algebra.Ring_Theory"

begin

context abelian_group

begin

(* below are just examples, otherwise can't use P and Q for the factor group *)
definition P :: "'b set ⇒ nat ⇒ bool" where
  "P A n = True"

definition Q :: "'b set ⇒ 'b set ⇒ bool" where "Q A B = undefined"

lemma induction_sketch:
  fixes n :: nat
  shows "∀ A. Q A G ⟶ P A n"
proof-
  have "abelian_group G (⋅) 𝟭 ⟹ (∀ A. Q A G ⟶ P A n)"
  proof(induction n arbitrary: G "(⋅)" "𝟭" rule: nat_less_induct)
    fix n
    fix G :: "'a set"
    fix add (infixl "⊕" 65)
    fix unit :: "'a"
    assume hind: "∀m<n. ∀x xa xb. abelian_group x xa xb ⟶ (∀A. Q A x ⟶ P A m)"
      and hgroupG: "abelian_group G add unit"
    interpret G: abelian_group G add unit by (simp add: hgroupG)
    obtain K :: "'a set" where hK: "subgroup_of_abelian_group K G (⊕) unit" sorry
    interpret K : subgroup_of_abelian_group K G "(⊕)" unit by (simp add: hK)
    (* below trivial *)
    have hgroupGK: "abelian_group (G.Factor_Group G K) K.quotient_composition (K.Class unit)" sorry
    obtain C :: "('a set) set" and m :: "nat" where hmn: "m < n" and
      hQC: "Q C (G.Factor_Group G K)" sorry
    show "(∀A. Q A G ⟶ P A n)"
    proof(auto)
      fix A assume "Q A G"
      (* claim I can prove *)
      moreover have "Q A G ⟹ P C m ⟹ P A n" sorry
      (* this should be a combination of hind, hgroupGK, hQC and hmn but fails *)
      moreover have "P C m" using hind hgroupGK hQC hmn sorry
      ultimately show "P A n" by simp
    qed
  qed
  then show ?thesis by (simp add: abelian_group_axioms)
qed

end

end

(* this should be a combination of hind, hgroupGK, hQC and hmn but fails *)
      moreover have "P C m" using hind hgroupGK hQC hmn sorry

Here, I fail to be able to specialize the induction hypothesis to the quotient group because the induction hypothesis is over a group, whose carrier is in ' b set and the carrier of the quotient group is in 'a set set. Thanks in advance for your help on making this work!

Manuel Eberl (Aug 23 2022 at 17:30):

Yeah I'm afraid that doesn't work. That's just a restriction of HOL's type system: you cannot do quantification over type variables.

The only solution I can think of is to simply always work on groups with elements of type nat. I assume everything is countable in your case (otherwise you wouldn't be able to do induction), so you can simply obtain some arbitrary bijection between your group elements and some set of natural numbers and then push everything along the isomorphism. It's not great, but it works.

Mantas Baksys (Aug 23 2022 at 18:34):

Thanks for the idea! I think the induction argument should work over all groups, not just countable ones. In the actual statement of Kneser’s theorem, we just pick nonempty finite subsets A, B of the group G, which we do not a-priori assume to be countable, so the group itself may not biject with a set of naturals. If I’m getting this right, your idea is to find a fixed type, in which we could embed all (abelian) groups?

Manuel Eberl (Aug 23 2022 at 19:13):

Manuel Eberl (Aug 23 2022 at 19:15):

If I understood you correctly, your induction step is to go from the group to some quotient group of that group?

Manuel Eberl (Aug 23 2022 at 19:16):

In that case, what you could do is to fix an arbitrary canonical representative for each of the equivalence classes and then just work with those representatives instead of the classes. This way, your 'a group is still an 'a group after the quotienting.

Manuel Eberl (Aug 23 2022 at 19:17):

Manuel Eberl (Aug 23 2022 at 19:20):

Just as a side note, I'm not an expert on this topic, but I think that even in systems that do support type-level quantification like Coq and Lean you might run into trouble here and have to employ a similar trick. But I might be wrong.

Mantas Baksys (Aug 24 2022 at 07:54):

Thanks, this indeed looks like a possible solution, I will try to implement it soon

Stream: Beginner Questions

Topic: Induction over a generalised type

Mantas Baksys (Aug 19 2022 at 17:55):