custom induction for inductive predicate

Stream: general

[Asei Inoue]

Motivation

I read the example about palindromes on the official Lean website.
There, in order to prove propositions about an inductive predicate called Palindrome, they constructed an induction principle specifically for Palindrome.

In code, it looks like this:

variable {α : Type}

@[grind]
inductive Palindrome : List α → Prop
  | nil : Palindrome []
  | single (a : α) : Palindrome [a]
  | sandwich {a : α} {as : List α} (ih : Palindrome as) : Palindrome ([a] ++ as ++ [a])

variable {a : α} {as : List α}

theorem List.palindrome_ind {motive : List α → Prop}
    (nil : motive [])
    (single : (a : α) → motive [a])
    (sandwich : (a b : α) → (as : List α) → motive as → motive ([a] ++ as ++ [b]))
    (as : List α)
    : motive as :=
  match as with
  | [] => nil
  | [a] => single a
  | a₁ :: a₂ :: as' =>
    have ih := palindrome_ind nil single sandwich (a₂ :: as').dropLast
    let xs := (a₂ :: as').dropLast
    let x := (a₂ :: as').getLast (by simp)
    have : [a₁] ++ xs ++ [x] = a₁ :: a₂ :: as' := by
      grind [List.dropLast_concat_getLast]
    this ▸ sandwich _ _ _ ih
termination_by as.length

example (h : as.reverse = as) : Palindrome as := by
  induction as using List.palindrome_ind with grind

This is quite cumbersome.
I thought it would be convenient if we could automatically generate induction principles for inductive predicates as well.

Question

Lean has functional induction, and for recursive functions it can automatically generate induction principles.
So I thought that, when an inductive predicate can be written as a recursive function, we could rewrite it as such and obtain an induction principle that way. I tried this approach, and it worked.

For Palindrome, it looks like this:

open scoped Classical in

def PalindromeRec (as : List α) : Prop :=
  match as with
  | [] => true
  | [a] => true
  | a₁ :: a₂ :: as =>
    let xs := (a₂ :: as).dropLast
    let x := (a₂ :: as).getLast (by simp)

    have : [a₁] ++ xs ++ [x] = a₁ :: a₂ :: as := by
      grind [List.dropLast_concat_getLast]

    if a₁ = x then
      PalindromeRec xs
    else
      false
termination_by as.length

example (h : as.reverse = as) : Palindrome as := by
  induction as using PalindromeRec.induct with grind

I think this is a good approach, but it only applies to inductive predicates that can be rewritten as recursive functions.
If an inductive predicate cannot be rewritten as a recursive function, is the only option to write the induction principle by hand?

[Asei Inoue]

Addendum

I recently realized that functional induction is actually useful not only for recursive functions, but also for inductive predicates that can be rewritten as recursive functions.
Thank you for introducing functional induction. It turned out to be far more useful than I initially thought.

[Aaron Liu]

What about the Palindrome.rec?

[Aaron Liu]

oh I guess you can only use it when you know it's a palindrome?

[Aaron Liu]

Then I don't see how this works in general

[Jakub Nowak]

Isn't it the case that every inductive predicate can be rewritten as recursive function? Although, proving termination in case of a function might be cumbersome (and might require passing some additional objects around).

[Kyle Miller]

I see — you did say this right at the beginning, but I skipped to the code and missed it — this is an induction principle especially for proving that something is a Palindrome. Usually induction principles go the other way.

I would say that you're right, List.palindrome_ind could naturally be defined via a function that checks whether something is a palindrome. Joachim (who implemented functional induction) has said before that a convenient way to build an induction principle is to define a recursive function that has the shape you want.

[Kyle Miller]

If it were possible to use the pattern

def isPalindrome : List α → Prop
  | [] => True
  | [_] => True
  | [a] ++ as ++ [b] => a = b ∧ isPalindrome as

then you'd get the exact induction principle you want through functional induction. However, the third one isn't a valid pattern in Lean.

[Jakub Nowak]

Hm, but unlike PalindromeRec, List.palindrome_ind doesn't check a₁ = x. So there is some difference here.

[Kyle Miller]

Right, it's setting up the induction for proving palindromes, that's the difference I was re-emphasizing

[Kyle Miller]

That doesn't mean that it proves lists are palindromes itself.

[Kyle Miller]

@Asei Inoue Another equivalent approach to List.palindrome_ind is to define the inductive predicate with List.palindrome_ind as its recursor, then prove it's always true, like so:

variable {α : Type}

@[grind]
inductive Palindrome : List α → Prop
  | nil : Palindrome []
  | single (a : α) : Palindrome [a]
  | sandwich {a : α} {as : List α} (ih : Palindrome as) : Palindrome ([a] ++ as ++ [a])

variable {a : α} {as : List α}

@[grind]
inductive IsPalindromeAux : List α → Prop
  | nil : IsPalindromeAux []
  | single (a : α) : IsPalindromeAux [a]
  | sandwich (a b : α) (as : List α) (ih : IsPalindromeAux as) : IsPalindromeAux ([a] ++ as ++ [b])

theorem IsPalindromeAux.trivial (as : List α) : IsPalindromeAux as :=
  match as with
  | [] => nil
  | [a] => single a
  | a :: a' :: as' =>
    have ih := trivial (a' :: as').dropLast
    let b := (a' :: as').getLast (by simp)
    have : [a] ++ (a' :: as').dropLast ++ [b] = a :: a' :: as' := by
      grind [List.dropLast_concat_getLast]
    this ▸ sandwich a b _ ih
termination_by as.length

example (h : as.reverse = as) : Palindrome as := by
  induction IsPalindromeAux.trivial as with grind

[Kyle Miller]

Just to check that indeed it has the expected recursor:

set_option pp.proofs true
#check IsPalindromeAux.rec
/-
IsPalindromeAux.rec {α : Type} {motive : (a : List α) → IsPalindromeAux a → Prop}
  (nil : motive [] IsPalindromeAux.nil)
  (single : ∀ (a : α), motive [a] (IsPalindromeAux.single a))
  (sandwich :
    ∀ (a b : α) (as : List α) (ih : IsPalindromeAux as),
      motive as ih → motive ([a] ++ as ++ [b]) (IsPalindromeAux.sandwich a b as ih))
  {a✝ : List α} (t : IsPalindromeAux a✝) : motive a✝ t
-/

(There's a small complexity where the IsPalindromeAux proof itself is passed along as an additional argument, but that doesn't change anything.)

[Jakub Nowak]

Hmm, so I guess we can view functional induction as something that takes a recursive induction, creates an equivalent inductive predicate for it, and does structural induction on it.