Complicated induction

Stream: new members

[Antoine Chambert-Loir]

When one needs to do an induction on an object that depends on many things, how to have the induction hypothesis be made variable ?

The context is the following :

variables (M X : Type*) [group M] [mul_action M X]

and I want to prove a proposition for all s : finset X by induction on s or on its cardinality. However, the inductive step, if s = a :: t, needs to replace M and X (by stabilizer M a and X by X \ {a}, about which I have the required mul_action).

The problem is that applying finset.induction_on furnishes an induction hypothesis that has not modified M and X, so is useless.

I can of course introduce an auxiliary integer n, with hypothesis s.card = n, and doing induction on n, but then, in the induction step, I need to rewrite myself s as a :: t, etc.

[Reid Barton]

It sounds like the real proof is either (1) induction on n = s.card, with induction hypothesis quantifying over all groups and actions, as you suggest, or (2) induction on s : finset X, but then quantifying over all subgroups M' of M and subsets X' of X with M' acting on X', and s contained in X', etc

[Henrik Böving]

If you are mostly concerned with the manual labor you have to do in the proof to get here you can also define your own induction principle that sets this environment up and tell the induction tactic to use that instead.

[Eric Wieser]

What's the statement that includes s?

[Kevin Buzzard]

Did you try induction...generalizing M X?

[Eric Wieser]

I doubt that's going to work when the type of s depends on X

[Mark Dickinson]

I found myself needing something similar earlier today: I wanted to prove something about all objects of a given type by complete induction on the "height" of those objects (with the height being an element of ℕ). I ended up abstracting out what I needed to the following:

lemma height_induction_gen {α : Type*} (ht : α -> ℕ) {P : α -> Prop} (J : α) :
    (∀ K : α, (∀ L : α, ht L < ht K -> P L) -> P K) -> P J :=
begin
  intro h,
  induction hn : ht J using nat.strong_induction_on with n ind_hyp generalizing J,
  exact h J (λ K ht_lt_ht, ind_hyp (ht K) (eq.rec ht_lt_ht hn) K rfl)
end

and then using a specialisation height_induction of that in an induction J using height_induction statement in my main proof. I dare say there's a better way, though. (I'm very much still learning Lean.)

[Antoine Chambert-Loir]

The kind of statement I wanted to prove is

theorem index_of_fixing_subgroup_of_multiply_pretransitive {M α:Type*} [group M] [mul_action M α] [fintype α]
     (s : finset α) :  (fixing_subgroup M (s : set X)).index * (fintype.card α - s.card).factorial = (fintype.card α).factorial :=
sorry

(possibly replacing the finset s by a set).

[Kevin Buzzard]

But your inductive step involved alphas of smaller size, right? So you should be able to generalise X and M using tricks like the one Mark is demonstrating. Their alpha is your triple X,M,alpha

[Antoine Chambert-Loir]

Right, but there are also the instances that M is a group and X a mul_action, and I don't know how to write it up.
I started with

 lemma induction_on_finset_mul_action
  (P : Π (G : Type*) (X : Type*)(group G) (mul_action G X) (s : finset X), Prop) :
  (∀ (G X : Type*) [group G] [mul_action G X], P (∅ : finset X)) →
  (∀ (G X : Type*) [group G] [mul_action G X] (a : X) (s : finset (sub_mul_action_of_stabilizer G X a)),
    P (stabilizer G a) (sub_mul_action_of_stabilizer G X a) s → P G X (insert a s)) →
  ∀ (G X : Type*) [group G] [mul_action G X] (s : finset X), P G X s := sorry
  ```
but some type inference does not work.

[Eric Wieser]

You need the by exactI trick for ∀ [group G] [mul_action G X], to work

[Eric Wieser]

That is, ∀ [group G], by exactI ∀ [mul_action G X],

[Kevin Buzzard]

Typeclasses after the colon don't get put into the typeclass system so you have to put them there manually, typically with an I tactic.

[Antoine Chambert-Loir]

It seems that I now need to add an exactI whenever I use something that refers to an instance…

[Eric Rodriguez]

thankfully all this will be gone(tm) in lean4

[Antoine Chambert-Loir]

And even this is a nightmare : I can't do rw anymore, I get strange error messages that rw or refineare unknown…

[Antoine Chambert-Loir]

Just in case a good soul passes nearby, and although this is not a MWE at all, here is the kind of stuff I wrote.
The rw [by exactI… does not work.

theorem jordan0 {n : ℕ} :
  ∀ {α : Type*} [decidable_eq α] [fintype α],
  ∀ {G : Type*} [group G] [hGα : by exactI mul_action G α],
  ∀ (hG : by exactI is_preprimitive G α)
    {s : set α} (hsn : by exactI fintype.card s = n.succ)
    (hsn' : by exactI 1 + n.succ < fintype.card α)
    (hs_trans : by exactI is_pretransitive (fixing_subgroup G s) (sub_mul_action_of_fixing_subgroup G s)),
  by exactI is_multiply_pretransitive (subgroup.normal_closure (fixing_subgroup G s).carrier) α 2 :=
begin
  induction n with n hrec,
  -- Initialization : n = 0
  { -- s = {a}
    intros α _ _ G _ _ _ s hsn hsn' hs_trans,

    let hG_eq := by exactI hG.to_is_pretransitive.exists_smul_eq,

    obtain ⟨a, hsa⟩ := by exactI card_eq_one_iff_is_singleton s hsn,
    rw hsa at *,

    have hG' : by exactI is_multiply_pretransitive G α 2,

-- up to here Lean stays silent, although I cannot be sure he's doing what I expect,
-- but on that point, it definitely complains.
      rw [by exactI stabilizer.is_multiply_pretransitive G α hG.to_is_pretransitive],

      rw ← is_pretransitive_iff_is_one_pretransitive,
      -- is_pretransitive (stabilizer G a) (sub_mul_action_of_stabilizer G α a),
      refine is_pretransitive_of_bihom
        (sub_mul_action_of_fixing_subgroup_of_singleton_bihom G a)
        (function.bijective.surjective
          (sub_mul_action_of_fixing_subgroup_of_singleton_bihom_bijective G a))
        hs_trans,


    let this : fixing_subgroup G ({a} : set α) = stabilizer G a :=
    { -- stabilizer G a = fixing_subgroup G ({a} : set α),
      by exactI ext g,  split,
      intro hg, exact (mem_fixing_subgroup_iff G).mp hg a (set.mem_singleton a) ,
      intro hg, rw mem_fixing_subgroup_iff, intros x hx,
        rw (set.mem_singleton_iff.mp hx), exact hg },

    rw this,

    by exactI refine jordan0_init G hG _ _,
    apply lt_of_eq_of_lt _ hsn', norm_num,
    rw is_pretransitive_iff_is_one_pretransitive,
    exact (stabilizer.is_multiply_pretransitive G α hG.to_is_pretransitive).mp hG',
    },

{
  -- Induction step



    sorry
},
end

[Adam Topaz]

Does the tactic#resetI tactic help at all?

[Adam Topaz]

When you're in a tactic block, using resetI tells lean to consider all the things that you have in context that could be considered as instances, to actually be considered as instances.

[Kyle Miller]

You can also use tactic#introsI when you're introducing an instance

[Kyle Miller]

That does resetI for you under the hood.

[Kyle Miller]

You don't need it here, but unfreezingI { induction n with n hrec } is something that is useful if somehow there were instances whose types depend on n. It also effectively does resetI while also unfreezing the local instances -- for efficiency local instances are "frozen" in Lean 3.

[Kevin Buzzard]

Antoine Chambert-Loir said:

And even this is a nightmare : I can't do rw anymore, I get strange error messages that rw or refineare unknown…

Probably you've made a syntax error.

[Kevin Buzzard]

Why the heck are you putting all those typeclasses after the colon? Why not put them all before the colon? I can't get anything to work, I don't know what is_preprimitive is.

[Eric Wieser]

My guess is they're before the colon because Antoine wasn't aware of unfreezingI {induction n generalizing G ... }

[Antoine Chambert-Loir]

Well, I managed to do the induction by hand, but this may deserve a general lemma.
I had to put some exactI in the statement, but after that, introsI did the job! Phew! (See branch#acl-Wielandt)

[Eric Wieser]

Can you link to a specific line in that branch?

[Kevin Buzzard]

lol 9000 lines :-) Antoine it will start rotting if you're not careful. They change the definition of groups occasionally, remember?

[Antoine Chambert-Loir]

For example : https://github.com/leanprover-community/mathlib/blob/3804896f0d9de686a81005b5928371da5ec598d3/acl-sandbox/group_theory/multiple_trans_specific.lean#L1120

[Antoine Chambert-Loir]

Now that the proof works, I need to tidy everything up and push PRs.
This will require : uniform naming of lemmas, cleaner APIs, but in the next days, I have some works to grade…

[Martin C. Martin]

.

[Bart Michels]

I have a situation that looks like this, where I want to do induction on dimension:

import linear_algebra.free_module.finite.basic
variables {K V : Type u} [division_ring K] [add_comm_group V] [module K V]

example [finite_dimensional K V] {S : Type*} (f : S → V) : true := by sorry

After lots of searching and trial and error I figured out I can do:

unfreezingI { induction h_dim : (module.rank K V).to_nat using nat.rec_on
  with n ih generalizing V },

Is this the correct way? I can't find this induction h : something type of thing in the tactics docs.

[Bart Michels]

Also, is it true that Lean will always figure out it needs to generalize everything that depends on V as well (here, f) ? Edit: ok surely.

[Ruben Van de Velde]

tactic#induction mentioned "induction h : t will introduce an equality of the form h : t = C x y, asserting that the input term is equal to the current constructor case, to the context." but not so much why that would be useful