Cycles of permutation appear to be missing glue lemmas

Stream: Is there code for X?

[metakuntyyy]

Hey guys,

I think I can't find important API for ConcreteCycle. Those lemmas appear to be missing. I tried to prove them for several hours today, but failed as I couldn't find simple API. The API for cyclic permutation seems to be incomplete and it's unfortunate to have to deal with IsCycle, IsCycleOn, Cycle and the underlying list.

Can anyone help me with this? I think those lemmas should be in mathlib.

import Mathlib

variable {α : Type*} [Fintype α] [DecidableEq α]


theorem next_isCyclePerm {x:α }(π: Equiv.Perm α)  (hs: π.IsCycle) (hel: x ∈ (Equiv.Perm.toCycle π hs) ):
    (Equiv.Perm.toCycle π hs).next (Equiv.Perm.nodup_toCycle π hs) x hel = π x :=by
  sorry


theorem eq_isCyclePerm {x:α }(π: Equiv.Perm α)  (hs: π.IsCycle) :
    x ∈ (Equiv.Perm.toCycle π hs)  ↔ π x ≠  x :=by
  sorry

[Jakub Nowak]

Do you need to use Cycle? It might help if you share more context.

[metakuntyyy]

Yes, I do need to use cycle. I am proving something about all permutations with https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Perm/Cycle/Factors.html#Equiv.Perm.cycle_induction_on. In the induction step I need to prove a property with the hypothesis that my permutation is a cycle. I obtain a cycle by https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Perm/Cycle/Concrete.html#Equiv.Perm.toCycle. I already have proof steps where I do induction by the cycle with https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/List/Cycle.html#Cycle.induction_on. Everything works well up until this point
image.png
Here I need both lemmas above. The proof itself is done modulo one sorry that is going analogously. But I really need those lemmas above.

[metakuntyyy]

There are nearly no lemmas for https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Perm/Cycle/Concrete.html#Equiv.Perm.toCycle I would be happy to fill above theorems and PR them to mathlib.

I don't know any proof ideas for the above two theorems. I spent around two hours trying to prove them and failed. I spent over 30 hours already filling in the sorries in my proof. Every definition I had worked after a lot of tinkering and the induction proofs are working well so far.

[metakuntyyy]

This is the best attempt I have so far

import Mathlib

variable {α : Type*} [Fintype α] [DecidableEq α]

theorem next_isCyclePerm {x:α }(π: Equiv.Perm α)  (hs: π.IsCycle) (hel: x ∈ (Equiv.Perm.toCycle π hs) ):
    (Equiv.Perm.toCycle π hs).next (Equiv.Perm.nodup_toCycle π hs) x hel = π x :=by
  unfold Equiv.Perm.toCycle at ⊢ hel
  simp at hel ⊢
  sorry

theorem eq_isCyclePerm {x:α }(π: Equiv.Perm α)  (hs: π.IsCycle) :
    x ∈ (Equiv.Perm.toCycle π hs)  ↔ π x ≠  x :=by
  constructor
  · intro h
    unfold Equiv.Perm.toCycle at h
    simp at h
    by_contra! hc
    sorry
  · intro h
    unfold Equiv.Perm.toCycle
    simp
    sorry

I don't know how to deal with the recursors.

[metakuntyyy]

Well, now there are some lemmas. I'll PR them once I clean them up. Does someone have good names for those three theorems?

import Mathlib

variable {α : Type*} [Fintype α] [DecidableEq α]

open Equiv Equiv.Perm List in
theorem dnontrivial_toCycle (f : Perm α) (hf : IsCycle f) : ∃ x, toCycle f hf = toList f x := by
  obtain ⟨x, hx, hy⟩ := id hf
  rw [Perm.toCycle_eq_toList f hf x hx]
  use x


open Equiv Equiv.Perm List in
theorem next_isCyclePerm {x:α }(f: Equiv.Perm α)  (hf: f.IsCycle) (hel: x ∈ (Equiv.Perm.toCycle f hf) ):
    (Equiv.Perm.toCycle f hf).next (Equiv.Perm.nodup_toCycle f hf) x hel = f x := by
  have ⟨ l, hl ⟩ := dnontrivial_toCycle f hf
  simp[hl] at ⊢
  have hele := hel
  simp [hl] at hele
  have aya := Equiv.Perm.nodup_toCycle f hf
  have ayb := Equiv.Perm.nontrivial_toCycle f hf
  rw[hl] at aya ayb
  simp at aya
  have eee : (Cycle.ofList (f.toList l)).next (hl ▸ nodup_toCycle f hf) x (hl ▸ (Eq.refl x)▸  hel) =
    (f.toList l).next x hele := by rfl
  rw[eee]
  exact Equiv.Perm.next_toList_eq_apply f l x hele


theorem eq_isCyclePerm {x:α }(f: Equiv.Perm α)  (hf: f.IsCycle) :
    x ∈ (Equiv.Perm.toCycle f hf)  ↔ f x ≠  x :=by
  constructor
  · intro h
    by_contra! hcon
    have ⟨ l, hl ⟩ := dnontrivial_toCycle f hf
    rw[hl] at h
    simp only [Cycle.mem_coe_iff] at h
    have lnm := List.next_mem (f.toList l) x h
    have len : 2 ≤ (f.toList l).length := by
      have ddll := (Cycle.length_nontrivial (Equiv.Perm.nontrivial_toCycle f hf))
      simp only [hl, Cycle.length_coe] at ddll
      exact ddll
    have dada := List.idxOf_lt_length_of_mem h
    set i := List.idxOf x (f.toList l)
    set li := (f.toList l)
    have dde : li.Nodup := by
      have eed := Equiv.Perm.nodup_toCycle f hf
      simp only [hl, Cycle.nodup_coe_iff] at eed
      exact eed
    have lnel := List.next_getElem li dde i dada
    have tete : li[i] = x := by exact List.getElem_idxOf dada
    simp [tete] at lnel
    rw[Equiv.Perm.next_toList_eq_apply] at lnel
    rw[lnel, ← tete] at hcon
    have twot : li[i]? = li[(i + 1) % li.length]? := by
      grind
    have lgei := List.getElem?_inj dada dde twot
    by_cases hcc : i = li.length - 1
    · have ip1 : i+1 = li.length := by grind
      rw[ip1] at lgei
      simp at lgei
      have ii : 1 < i := by grind
      grind
    · have hdd : i ≤ li.length -1 := by grind
      have hde : i +1 < li.length  := by grind
      have hdf : (i+1) % li.length = (i+1) :=  Nat.mod_eq_of_lt hde
      grind
  · intro h
    have eee := Equiv.Perm.toCycle_eq_toList f hf x h
    rw[eee]
    simp only [Cycle.mem_coe_iff]
    unfold Equiv.Perm.toList
    simp only [List.mem_iterate, Equiv.Perm.iterate_eq_pow]
    use 0
    constructor
    · simp only [Finset.card_pos, Equiv.Perm.support_cycleOf_nonempty, ne_eq]
      exact h
    · simp

[metakuntyyy]

https://github.com/leanprover-community/mathlib4/pull/31665 open for the first two theorems. I golfed them as hard as I could.

[Antoine Chambert-Loir]

Using rw [← Cycle.formPerm_apply_mem_eq_next], you need to prove that (π.toCycle hs).formPerm (π.nodup_toCycle hs) = π, something that seems to be hidden in the equivalence docs#Equiv.Perm.isoCycle. (Your cycle will be nontrivial because it contains x.)

[metakuntyyy]

Thanks, but I've proven the lemmas I wanted to prove. I guess topics in this channel can't be resolved. https://github.com/leanprover-community/mathlib4/pull/31665 opens the PR for the first lemma, I still need to clean up the second lemma.

[Jakub Nowak]

@metakuntyyy But docs#Cycle and docs#Equiv.Perm.IsCycle/docs#Equiv.Perm.IsCycleOn are two quite different things. docs#Equiv.Perm.cycle_induction_on doesn't use docs#Cycle. I suspect, if you want to prove something about cycles in permutations you should be using docs#Equiv.Perm.IsCycle/docs#Equiv.Perm.IsCycleOn, not docs#Cycle.

[metakuntyyy]

@Jakub Nowak Yes you are correct, they are different things, isCycle is a Prop while Cycle is data. I was first looking at the API how to do it with IsCycle. IsCycle is a prop and the statement that I want to prove in the induction step is easiest by using data. Using https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Perm/Cycle/Concrete.html#Equiv.Perm.toCycle gives me data with which I can proceed.

I tried looking for good API with IsCycle, and the best that sticked was getting a cycle. The only thing that bugged me was that API was missing for cycle, which I am in the process of PRing the missing statements to mathlib.

[Jakub Nowak]

I feel like having two different APIs for cycles will make things worse. Maybe it would be better to add missing induction lemmas to IsCycle?

[metakuntyyy]

Sure thing. Do you have any suitable replacement for https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/List/Cycle.html#Cycle.induction_on? Because this is the theorem I'm relying on.

[Jakub Nowak]

Do you mind sharing how do you use docs#Cycle.induction_on in your proof? Maybe you could use docs#Equiv.Perm.support instead of docs#Equiv.Perm.toCycle and do induction on the support Finset? That would only work if you don't need an order for a proof.

[metakuntyyy]

Here you go. I stubbed the proof out.

import Mathlib

variable {α : Type*} [Fintype α] [DecidableEq α]

def cycleCountFinset  (c: Cycle α)(p: α → Prop)[DecidablePred p] (hs: c.Nodup): Finset α  :=
  Finset.univ.filter (fun x => if h: x ∈ c then ((p x) ∧ ¬ (p (Cycle.next c hs x h))) else False)

def cycleCountSwitch (c: Cycle α)(p: α → Prop)[DecidablePred p] (hs: c.Nodup):ℕ :=
  (cycleCountFinset c p hs).card


theorem outher (c: Cycle α)(p: α → Prop)[DecidablePred p] (hs: c.Nodup):
    (cycleCountSwitch c (fun x => p x) hs) = (cycleCountSwitch c (fun x => ¬ p x) hs) := by
  have ay :=  Cycle.induction_on c (motive := (fun a =>
    if hey : a.Nodup then (cycleCountSwitch a (fun x => p x) hey) = (cycleCountSwitch a (fun x => ¬ p x) hey)
    else True
  )) ?_ ?_
  · simp only [hs, ↓reduceDIte] at ay
    exact ay
  · simp only [Cycle.nodup_nil, ↓reduceDIte]
    unfold cycleCountSwitch cycleCountFinset
    simp only [Cycle.notMem_nil, ↓reduceDIte, Finset.filter_false, Finset.card_empty]
  sorry

[metakuntyyy]

Again, it's well possible that it is easier to do with IsCycle. The first thing that I found that worked well is Cycle, as that one had an induction principle that I needed.

[Jakub Nowak]

No need to use Cycle.induction_on, it's easier to use induction tactic:

import Mathlib

variable {α : Type*} [Fintype α] [DecidableEq α]

def cycleCountFinset (c : Cycle α) (p : α → Prop) [DecidablePred p] (hs : c.Nodup) : Finset α :=
  Finset.univ.filter (fun x => if h : x ∈ c then ((p x) ∧ ¬ (p (Cycle.next c hs x h))) else False)

def cycleCountSwitch (c : Cycle α) (p : α → Prop) [DecidablePred p] (hs : c.Nodup) : ℕ :=
  (cycleCountFinset c p hs).card

theorem outher (c : Cycle α) (p : α → Prop) [DecidablePred p] (hs : c.Nodup) :
    (cycleCountSwitch c (p ·) hs) = (cycleCountSwitch c (¬ p ·) hs) := by
  induction c with
  | nil => simp [cycleCountSwitch, cycleCountFinset]
  | cons x xs ih =>
    sorry

After all, I think that induction on Cycle is the best approach to prove this. It makes more sense and is easier to prove this for Cycle and then transfer the result to Perm. And I agree, that the two lemmas you mentioned at the beginning are needed to do that.

[metakuntyyy]

Thanks, I'll use the improvements.

[Jakub Nowak]

docs#Equiv.Perm.mem_support is already marked with @[simp] so I think π x ≠ x should be preferred form. I think that API might work better:

theorem Equiv.Perm.support_mem_toCycle (π : Equiv.Perm α) (hs : π.IsCycle) {x : α} (h : π x ≠ x) :
    x ∈ π.toCycle hs := by sorry

theorem Equiv.Perm.toCycle_next_eq {x : α} (π : Equiv.Perm α) (hs : π.IsCycle) (h : π x ≠ x) :
    (π.toCycle hs).next (π.nodup_toCycle hs) x (π.support_mem_toCycle hs h) = π x := by sorry

@[simp]
theorem Equiv.Perm.mem_toCycle_iff_support {x : α} (π : Equiv.Perm α) (hs : π.IsCycle) :
    x ∈ π.toCycle hs ↔ π x ≠ x := by sorry

[metakuntyyy]

@Jakub Nowak Thanks for the help. I managed to prove the theorem in 10 lines, the previous proof was 50 lines. Your docs#Equiv.Perm.mem_support was indeed very helpful. https://github.com/leanprover-community/mathlib4/pull/31665

[Jakub Nowak]

@metakuntyyy No problem! Could you link to this discussion in a PR? Relevant discussion might be helpful for the reviewer, and for anyone looking for information in the future.