Tail of reduced word is reduced

Stream: Is there code for X?

[Christian K]

import Mathlib.GroupTheory.FreeGroup.Basic


lemma tail_reduced_eq_reduced {α : Type} [DecidableEq α] (x : List (α × Bool)) (hx : x =  FreeGroup.reduce x) :
    x.tail =  FreeGroup.reduce x.tail := by
    induction x with
    | nil =>
        simp
        exact hx
    | cons head tail ih =>
        simp
        sorry

"A codeblock says more than a thousand words"...
I have a List wich represents a word in a FreeGroup. according to hx, this word is fully reduced. I thought it would be simple to prove that the tail of this word is also reduced, but I'm stuck. What am I missing?

[Mitchell Lee]

I think there are essentially three steps to this proof.

1. Show (using FreeGroup.reduce.cons and induction) that (FreeGroup.reduce L).length ≤ L.length for all lists L, and that equality holds if and only if FreeGroup.reduce L = L.
2. Show that (FreeGroup.reduce (x :: L)).length ≤ 1 + (FreeGroup.reduce L).length for all x and L. This can be done using FreeGroup.reduce.cons directly and should not require induction.
3. Assuming that FreeGroup.reduce (x :: L) = x :: L, you can take the length of both sides and combine the above results to show that FreeGroup.reduce L = L.

That is how I would approach it, but maybe someone can suggest an easier way.

[Mitchell Lee]

I do not think that it makes much sense to use induction directly on the theorem tail_reduced_eq_reduced you are trying to prove. In order to actually use the inductive hypothesis ih, you will need to show that tail = FreeGroup.reduce tail. And if you can do that, the proof is already done anyway.

[Christian K]

I don't think the first point works like that, because if
List.length (FreeGroup.reduce L) < List.length Lthen Lis not reduced.
And I don't see how i could use 2. then.

[Matt Diamond]

I came up with a proof, though I wouldn't be surprised if there's an easier / more elegant way:

import Mathlib.GroupTheory.FreeGroup.Basic

variable {α : Type} [DecidableEq α] {x : List (α × Bool)}

lemma reduce_ne_inv_pair : FreeGroup.reduce x ≠ (a, b) :: (a, !b) :: L :=
by
  have : (a, b) :: (a, !b) :: L = [] ++ (a, b) :: (a, !b) :: L := by rw [List.nil_append]
  rw [this]
  exact FreeGroup.reduce.not

lemma tail_reduced_eq_reduced (hx : x = FreeGroup.reduce x)
  : x.tail = FreeGroup.reduce x.tail :=
by
  cases x with
  | nil => exact hx
  | cons head tail =>
    rw [FreeGroup.reduce.cons] at hx
    by_cases h1 : FreeGroup.reduce tail = []
    · simp [h1] at hx
      simp [hx, FreeGroup.reduce]
    · obtain ⟨b, L, h2⟩ := List.exists_cons_of_ne_nil h1
      simp only [h2] at hx
      split_ifs at hx with h3
      · cases b; cases head
        simp only at h3
        cases' h3 with h4 h5
        rw [← hx, h4, h5] at h2
        exact (reduce_ne_inv_pair h2).elim
      · rw [List.cons_inj] at hx
        rw [List.tail_cons, h2]
        exact hx

[Christian K]

Ok thank you very much.