induction while keeping track of a hypothesis

Stream: general

[Mantas Baksys]

Hey, I've run into the following problem. I can't seem to be able to find out how to induct over permutations satisfying a specific hypothesis. Here's an MWE :

import tactic group_theory.perm.support group_theory.perm.sign

open finset equiv
open_locale classical big_operators

theorem induction {ι : Type*} [fintype ι] (s : finset ι) (σ : perm ι) (hσ : σ.support ⊆ s) :
  false :=
begin
  cases (perm.trunc_swap_factors σ).out with l hl,
  induction l with g l generalizing σ hσ,
  sorry,
  sorry,
end

The problem is that hσ as a hypothesis is true only for the current σ and I'd like to have it as a hypothesis also for the previous one. Initially, I wanted to use swap_induction_on but that turned out to be set up in a way, where this hypothesis tracking is not supported. Thanks!

[Riccardo Brasca]

This was nonsense, sorry

[Alex J. Best]

I don't think this is mathematically possible for an arbitrary hypothesis right? Like if the hypothesis is sigma.support = s there's no way to get there with only transpositions. So you are really doing something special to the situation that I don't think there are tools for. You'd have to write an induction principle saying that every perm with restricted support is attainable via compositing transpositions with that support, likely the existing proof already does this under the hood?
In your case seeing as your condition is that the perm lies in a subgroup it might be more effective to pass to that subgroup (perm s) and use induction on that subgroup.

[Mantas Baksys]

Alex J. Best said:

I don't think this is mathematically possible for an arbitrary hypothesis right? Like if the hypothesis is sigma.support = s there's no way to get there with only transpositions. So you are really doing something special to the situation that I don't think there are tools for. You'd have to write an induction principle saying that every perm with restricted support is attainable via compositing transpositions with that support, likely the existing proof already does this under the hood?
In your case seeing as your condition is that the perm lies in a subgroup it might be more effective to pass to that subgroup (perm s) and use induction on that subgroup.

You're right, I'll need to write something specific in that case.

[Yakov Pechersky]

Does cases h : (perm.trunc_swap_factors σ).out with l hl, help, at least conceptually, with what you wanted?