Insufficient number of targets

Stream: batteries

[Robin Green]

I tried to do

induction data using String.utf8InductionOn

but I got insufficient number of targets for 'String.utf8InductionOn'. I don't know what this error message means. Is this supported at all?

[Kevin Buzzard]

#mwe ?

[Robin Green]

import Std.Data.String.Lemmas

def count (s : Substring) (p : Char -> Bool) : Nat :=
  s.foldr (fun ch c => if p ch then c + 1 else c) 0

theorem missing_char_count_zero (v : Substring.Valid word) : word.contains ch = false -> count word (· == ch) = 0 := by
  cases word
  . case mk str startPos stopPos =>
      cases str
      . case mk data =>
          induction data using String.utf8InductionOn

[Mario Carneiro]

I don't think String.utf8InductionOn is compatible with the induction tactic

[Mario Carneiro]

you have to just call it directly

[Mario Carneiro]

which looks like this:

          apply String.utf8InductionOn
            (motive := fun data startPos =>
              Substring.contains ⟨⟨data⟩, startPos, stopPos⟩ ch = false →
              (count ⟨⟨data⟩, startPos, stopPos⟩ fun x ↦ x == ch) = 0)
            data startPos stopPos

[Mario Carneiro]

cc: @Joachim Breitner , it would be nice to get the induction using parser to support more theorems in std/mathlib with inductionOn in the name - the lean 4 rules are more restrictive than lean 3 and mostly don't work at all when the motive has multiple targets

[Eric Rodriguez]

docs#String.utf8InductionOn

[Eric Rodriguez]

Oh, because the motive takes two parameters?

[Joachim Breitner]

On the phone right now. But does induction data, startPos using String.utf8InductionOn (p := stopPos) not work?

[Robin Green]

No - now I get:

tactic 'introN' failed, insufficient number of binders
case p
ch : Char
startPos stopPos : String.Pos
data : List Char
⊢ String.PosLean 4

Though I'm having fun with the full power of using apply directly :grinning_face_with_smiling_eyes:

[Joachim Breitner]

That's probably https://github.com/leanprover/lean4/issues/3212. So it's not much missing

[Joachim Breitner]

But yes, at some point it's easier to use apply or refine rather than fighting the induction tactic :-)

[Joachim Breitner]

Oh, and you can work around #3212 by revert’ing yourself:

import Std.Data.String.Lemmas

def count (s : Substring) (p : Char -> Bool) : Nat :=
  s.foldr (fun ch c => if p ch then c + 1 else c) 0

theorem missing_char_count_zero (v : Substring.Valid word) : word.contains ch = false -> count word (· == ch) = 0 := by
  cases word
  . case mk str startPos stopPos =>
      cases str
      . case mk data =>
          revert v
          induction data, startPos using String.utf8InductionOn (p := stopPos)

[Robin Green]

It considers the (p := stopPos) a syntax error now, but it does appear to generate some subgoals if I remove that part

[Joachim Breitner]

You are probably on 4.5.0; it works already on live.lean-lang.org; this is a new feature I added recently.

[Joachim Breitner]

But yes, you can omit it, and then use exact p as the first “case” instead