Termination proof

Stream: Is there code for X?

[Ka Wing Li]

I am trying to get the following done. But it seems lean losses dependent information when proving termination through pattern matching

def n_leading_spaces (s : String) : Nat :=
  match s.toList with
  | [] => 0
  | ' ' :: t => 1 + n_leading_spaces (String.ofList t)
  | _ => 0
  termination_by s.length
  decreasing_by
    all_goals simp_wf
    sorry

Or is there a nice way to pattern match on string?

[Kim Morrison]

I would use something like s.chars.takeWhile (· == ' ') |>.size. (Not sure if those function names are right: but use the iterators.)

[Jakub Nowak]

Yes, if you match on property or output of function then termination checker won't work.

[Jakub Nowak]

You can do this:

def n_leading_spaces (s : String) : Nat := go s.toList
  where
  go (s : List Char) : Nat :=
    match s with
    | [] => 0
    | ' ' :: t => 1 + go t
    | _ => 0

But using API as Kim hinted should also work, and it might be less hassle.

[Ka Wing Li]

Thanks! I am wondering why hypotheses are not generated from pattern matching.

[Aaron Liu]

I think it's because it would clutter the infoview with matching hypotheses you usually don't need

[Jakub Nowak]

You can instruct match to generate hypothesis by modifying the match in the body of the function. Though, it's a bit weird that you have you modify the body of the function for the termination proof. I agree with you that termination checker should introduce match hypotheses by default. Just like e.g. split tactic does.

def n_leading_spaces (s : String) : Nat :=
  match h : s.toList with
  | [] => 0
  | ' ' :: t => 1 + n_leading_spaces (String.ofList t)
  | _ => 0
  termination_by s.length
  decreasing_by
    all_goals simp_wf
    guard_hyp h : s.toList = ' ' :: t