Induction where the base case is 1 not 0

Stream: new members

[Ryan Smith]

I am writing a proof by induction on the order of a finite group G. My base case is the trivial group which has order 1, not order 0. How do you structure an argument like this? I could technically have a case for order 0 which is a contradiction, a case for order 1 which I prove something, and an inductive case for n > 1 ? The order is a Nat so perhaps two base cases make sense?

[Weiyi Wang]

Does this help? Nat.le_induction

[Ryan Smith]

That seems like what I was looking for, I can't find any examples of anyone actually using this?

[Marcus Rossel]

Here's a simple example:

import Mathlib.Data.Nat.Init

example (h : 0 < n) : 0 < n * n := by
  induction n, h using Nat.le_induction with
  | base => grind
  | succ => grind

[Ryan Smith]

Thanks for the example! I hadn't heard of grind before, and I don't see it in mathematics in lean. Is there a more comprehensive and up to date reference? Also one question about the example, we don't have a name for the inductive hypothesis in the succ case do we?

[Niels Voss]

Well there's the reference manual https://lean-lang.org/doc/reference/latest/The--grind--tactic/#grind-tactic, but probably the reason you've never heard of grind is because it's only been available for a month or two

[Ryan Smith]

Why is this failing then?

import Mathlib

variable {G: Type*} [Group G] [Finite G]

example (h : 0 < Nat.card G) : True := by
  induction Nat.card G, h using Nat.le_induction with
  | base => sorry
  | succ => sorry

The induction step has a type issue,

target
  h
has type
  0 < Nat.card G : Prop
but is expected to have type
  ?m.89 ≤ x✝ : Prop

Didn't we give it what it wanted here? A statement that the thing we are inducting on is greater than zero?

[Aaron Liu]

this is probably a bug in induction

[Aaron Liu]

I'm guessing it's the same one as #18690

[Ryan Smith]

From the bug description, would you expect

import Mathlib

variable {G: Type*} [Group G] [Finite G]

example (h : 0 < Nat.card G) : True := by
  let cardG := Nat.card G
  induction cardG, h using Nat.le_induction with
  | base => sorry
  | succ => sorry

To work then? Since that's the same, although it seems to match the work around suggested in the bug

[Weiyi Wang]

import Mathlib

variable {G: Type*} [Group G] [Finite G]

example (h : 0 < Nat.card G) : True := by
  induction Nat.card G, Nat.one_le_of_lt h using Nat.le_induction with
  | base => sorry
  | succ => sorry

This does build, but I doubt the induction is doing the right thing... I am also curious what proof uses induction on the order of the group

[Weiyi Wang]

If this is not strictly a property of group, but a property of natural numbers, you can generalize n = Nat.card G first

[Ryan Smith]

Could you explain what you mean about generalize n = Nat.card G ? I'm still trying to express stuff to lean so possibly going about this in the wrong way.

As for why, pretty simple. I was curious to see if I could formalize Burnside's theorem which says groups of order p^a q^b are solvable and one step is a simplifying assumption that Z(G)=1 since if were nontrivial we could induct on the order of G to get that Z(G) and G/Z(G) are solvable by hypothesis therefore G is solvable. I guess it could still be a little bit messy since an arbitrary n might not be of the form p^a q^b

[Aaron Liu]

you need some sort of strong induction

[Aaron Liu]

docs#Nat.strongRec

[Weiyi Wang]

My first reaction to this is I might write it as a recursive proof

[Aaron Liu]

termination_by Nat.card G

[Damiano Testa]

Is it maybe something like this that you are trying to do?

example (h : 0 < Nat.card G) : True := by
  generalize hn : Nat.card G = n
  revert G
  induction n using Nat.strong_induction_on with
  | h n ih =>
    sorry

[Damiano Testa]

(I am going more by what I expect an induction on the size of a group to look like, than by actually using Nat.le_induction.)

[Weiyi Wang]

This looks about right

[Aaron Liu]

import Mathlib

example {G : Type*} (h : 0 < Nat.card G) : True := by
  generalize hn : Nat.card G = n
  induction n using Nat.strongRec generalizing G with subst hn
  | ind n ih =>
    sorry

golfed

[Aaron Liu]

I needed to do something similar recently

[Aaron Liu]

the solution was to find a better induction theorem

[Ryan Smith]

That is some amazing black magic. I'm still trying to parse in my brain what exactly is going on here. How do I have no base case any longer?

[Aaron Liu]

Ryan Smith said:

That is some amazing black magic. I'm still trying to parse in my brain what exactly is going on here. How do I have no base case any longer?

you don't need a base case for this kind of induction

[Weiyi Wang]

For strong induction, the base case is implied, because when n = 0 (or 1 for your particular theorem), ih becomes "useless", as its condition can never be fulfilled

[Ryan Smith]

Ok right, so we implicitly handle it when the quantifier is quantifying over nothing

More generally, what does generalize actually do? I thought I understood from a tutorial but now I think I do not.

[Ryan Smith]

Sort of progress?

import Mathlib

open Group

variable (p q : ℕ) (G : Type*) [Group G] [Finite G]

theorem temp (p q a b : ℕ) [Fact p.Prime] [Fact q.Prime]
    (hord : Nat.card G = p ^ a * q ^ b) : IsSolvable G := by
  generalize hn : Nat.card G = n
  induction n using Nat.strongRec generalizing G with subst hn
  | ind n ih =>
    sorry

The issue is that the type of ih is

ih : ∀ m < Nat.card G,
  ∀ (G : Type u_1) [inst : Group G] [Finite G], Nat.card G = p ^ a * q ^ b → Nat.card G = m → IsSolvable G

How do I go about unpacking that into something I can use? My understanding from tutorials is that rcases or obtain would make sense, but my attempts at both fail since ih is not an inductive type?

[Damiano Testa]

I suspect that you should also revert the p q a b variables for the induction to be useful.

[Damiano Testa]

As to how to use ih, you'll probably start your proof, produce a subgroup/quotient of G and then you'll have hyp := ih ..., where the G in the application is the subgroup/quotient you identified.