show variant string function is terminating

Stream: general

[Kayla Thomas]

I'm wondering how I would go about setting this up to show that the recursion terminates, since eventually s will be longer than any of the elements of l?

def variant
  (s : String)
  (c : Char)
  (l : Finset String) : String :=
  if s ∈ l
  then variant (s.append c.toString) c l
  else s

[Kayla Thomas]

Maybe part of the issue is that it is an if, then, else and not a match, so I'm not sure what the syntax is to deal with it to start.

[Mario Carneiro]

you need to use if h : s ∈ l

[Kayla Thomas]

Do I somehow introduce by to show the proof?

[Kayla Thomas]

I guess it is termination_by.

[Kayla Thomas]

(deleted)

[Kayla Thomas]

Is this the right setup?

def variant
  (s : String)
  (c : Char)
  (l : Finset String) : String :=
  if h : s ∈ l
  then variant (s.append c.toString) c l
  else s
  termination_by variant s _ l => (l.sup String.length) - s.length

[Kayla Thomas]

What kind of expression is termination_by looking for?

[Kayla Thomas]

Is it supposed to be some kind of function?

[Kevin Buzzard]

Look for examples in core lean or mathlib -- right now this seems to be the most efficient way to understand this stuff

[Kayla Thomas]

There might be a simpler way to do it, but I kept hacking at it and got this to work.

import Mathlib.Data.String.Lemmas


def List.str_max_len :
  List String → ℕ
| [] => 0
| hd :: tl => max hd.length (List.str_max_len tl)

lemma list_str_max_len_mem
  (s : String)
  (l : List String)
  (h1 : s ∈ l) :
  s.length <= List.str_max_len l :=
  by
  induction l
  case nil =>
    simp at h1
  case cons hd tl ih =>
    simp at h1
    unfold List.str_max_len
    cases h1
    case inl c1 =>
      simp only [c1]
      simp
    case inr c1 =>
      specialize ih c1
      trans List.str_max_len tl
      · exact ih
      · simp

def variant
  (s : String)
  (c : Char)
  (l : List String) :=
  if h : s ∈ l
  then
  have : List.str_max_len l + 1 - (String.length s + String.length (Char.toString c)) < List.str_max_len l + 1 - String.length s :=
    by
    have s1 : (Char.toString c).length = 1
    simp only [String.length]
    unfold Char.toString
    simp
    simp only [s1]
    simp
    obtain s2 := list_str_max_len_mem s l h
    refine Iff.mpr (tsub_lt_tsub_iff_right s2) ?_
    simp
  variant (s ++ c.toString) c l
  else s
  termination_by variant s _ l => List.str_max_len l + 1 - s.length

[Kayla Thomas]

Would anyone happen to know how to go about proving things about this definition? Is there some way to do induction on it? For example, I'm struggling with this:

example
  (s : String)
  (c : Char)
  (l : List String) :
  variant s c l ∉ l :=

[Kayla Thomas]

Unfolding the definition doesn't help, because it just keeps on going.

[Kayla Thomas]

And I'm not certain what to do induction on.

[Kayla Thomas]

I thought maybe s.data, but induction s.data doesn't seem to change the goal.

[Kevin Buzzard]

Unfold variant and use split?

[Kayla Thomas]

example
  (s : String)
  (c : Char)
  (l : List String) :
  variant s c l ∉ l :=
  by
  unfold variant
  simp
  split_ifs
  case inl c1 =>
    sorry

s: String
c: Char
l: List String
c1: s ∈ l
⊢ ¬variant (s ++ Char.toString c) c l ∈ l

[Kayla Thomas]

I'm not sure where to go from there.

[Kayla Thomas]

The most I have been able to prove is that

example
  (s : String)
  (c : Char)
  (l : List String)
  (h1 : s ∉ l) :
  variant s c l = s :=

[Alex J. Best]

You can use a similar recursion for the proof

lemma variant_spec
  (s : String)
  (c : Char)
  (l : List String) : ¬ variant s c l ∈ l :=
  if h : s ∈ l
  then
  have : List.str_max_len l + 1 - (String.length s + String.length (Char.toString c)) < List.str_max_len l + 1 - String.length s :=
    by
    have s1 : (Char.toString c).length = 1
    simp only [String.length]
    unfold Char.toString
    simp
    simp only [s1]
    simp
    obtain s2 := list_str_max_len_mem s l h
    refine Iff.mpr (tsub_lt_tsub_iff_right s2) ?_
    simp
  by
    rw [variant]
    simp only [h, dite_eq_ite, ite_true]

    apply variant_spec _ _ _
  else by
    rw [variant]
    simp [h]
  termination_by variant_spec s _ l => List.str_max_len l + 1 - s.length

[Kayla Thomas]

@Alex J. Best Thank you! I'm not familiar with how this form of proof works. Is it equivalent in some way to one of the usual forms of induction? Is there exposition on it somewhere?

[Alex J. Best]

Well whats happening here is that lemmas and defs are basically the same thing. Constructing some sort of resursive function that terminates and produces some value is not just analogous to writing down some recursive function that terminates and produces a proof, its really the same thing. So seeing as you already worked out precisely what induction you needed to state the function it makes sense to use the analogous structure to prove things about the function.
Under the hood both are being turned into something defined in terms of docs#WellFounded.fix, we can just use this nice recursive syntax to write this down in a natual way.
The only difference is that when I want to prove something I can freely drop into tactic mode to finish things off rather than having to write a proof term by hand, this is much more conventient so I use it in 2 places in the above proof.

[Kayla Thomas]

Thank you.