Word metric on group

Stream: new members

[Rémi Bottinelli]

Hey!
In the code below, I'm trying to figure out how to define the word metric on a group given an indexed set of generators.
I'm stuck at showing that the word metric is always realized by a geodesic.
My problem is that the way I define the length of a group element is as a shortest word: geod_for in the code, and I can't see how to "inspect" the function's body to be able to say that "if there is some word representing this group element, then there is a geodesic one, and the length is realized" (that's the length_realized function).
I have two versions of geod_for, one of which is a composite of "first deciding emptiness of the set of words", and "then finding a geod in case it is non-empty". I thought this would help, but it doesn't seem to.
What am I doing wrong? Thanks!

import group_theory.free_group
import group_theory.quotient_group
import data.real.ennreal
import data.nat.enat

open option
open set function list
open well_founded
open classical
open_locale classical



noncomputable theory

namespace word_metric

variables {G : Type*} [group G] {ι : Type*} (letters : ι → G)


def val : (free_group ι) → G := λ w, free_group.lift letters w
def len : (free_group ι) → ℕ := λ w, (free_group.to_word w).length

def words_for (g : G) : set (free_group ι) :=
{ w : free_group ι | val letters w = g }
def geods_for  (g : G) : set (free_group ι) :=
{ w ∈  words_for letters g | ∀ u ∈ words_for letters g, (len u) ≥ (len w) }

lemma geods_have_same_length
  (g : G) (w₁ w₂ : geods_for letters g) : len (w₁ : free_group ι) = len (w₂ : free_group ι) :=
let
  ⟨f₁,word₁,geod₁⟩ := w₁
, ⟨f₂,word₂,geod₂⟩ := w₂
in
  ge_antisymm (geod₂ f₁ word₁) (geod₁ f₂ word₂)



def geod_for (g : G)  : option (geods_for letters g) :=
let
  wg := words_for letters g
in
  if h : wg.nonempty then
    let
      w := argmin_on len nat.lt_wf wg h
    , w_word_for_g := argmin_on_mem len nat.lt_wf wg h
    , w_shortest   := λ (w' : free_group ι) (w'_in : w' ∈ wg), argmin_on_le len nat.lt_wf wg w'_in h
    in
      option.some ( ⟨w,w_word_for_g,w_shortest⟩ )
  else
    none

def geod_for_helper (g : G)
  (emp : psum (words_for letters g).nonempty ¬(words_for letters g).nonempty ) :
  option (geods_for letters g) :=
let
  wg := words_for letters g
in
  psum.rec
    ( λ h,  let
        w := argmin_on len nat.lt_wf wg h
      , w_word_for_g := argmin_on_mem len nat.lt_wf wg h
      , w_shortest   := λ (w' : free_group ι) (w'_in : w' ∈ wg), argmin_on_le len nat.lt_wf wg w'_in h
      in
        option.some ( ⟨w,w_word_for_g,w_shortest⟩ : geods_for letters g ))
    ( λ h, none)
    emp

def get_emp (g : G) :
  psum (words_for letters g).nonempty ¬(words_for letters g).nonempty :=
dite (words_for letters g).nonempty (λ h, psum.inl h) (λ h, psum.inr h)

def geod_for' (g : G) := geod_for_helper letters g (get_emp letters g)

def word_length  (g : G) : enat :=
option.elim (geod_for' letters g) ⊤ (λ w, len (w : free_group ι))

lemma word_length_realized (g : G) (w : free_group ι) (win : w ∈ words_for letters g):
  ∃ u ∈ geods_for letters g, word_length letters g = len u :=
begin
  rcases get_emp letters g with (nonempty|empty),
  {-- Confusion here
  sorry},
  { exfalso,
    -- seems overly convoluted
    exact (eq_empty_iff_forall_not_mem.mp $ not_nonempty_iff_eq_empty.mp empty) w win,}

end

lemma word_length_le_word (g : G) (w : free_group ι) (win : w ∈ words_for letters g) :
  word_length letters g ≤ len (w : free_group ι) :=
begin
  rcases word_length_realized letters g w win with ⟨f,⟨word,geod⟩,exact⟩,
  calc word_length letters g = len f : exact
                         ... ≤ len (w : free_group ι) : enat.coe_le_coe.mpr $ ge.le $ geod w win,
end


lemma word_length_top_iff_no_words (g : G) :
  word_length letters g = ⊤ ↔ words_for letters g = ∅ :=
sorry
lemma word_length_fin_iff_words (g : G) :
  word_length letters g < ⊤ ↔ words_for letters g ≠ ∅ :=
sorry




end word_metric