Induction principle for well-founded recursion definition

Stream: maths

[Heather Macbeth]

When you make a definition by well-founded recursion, is there a way to auto-generate an induction principle for it?

For example, the following definition is made by well-founded recursion (it moves strictly forward according to the default SizeOf instance on Nat × Nat, namely SizeOf.sizeOf (a, b) = 1 + a + b):

def Pascal : Nat × Nat → Nat
  | (0, _) => 1
  | (_, 0) => 1
  | (a + 1, b + 1) => Pascal (a + 1, b) + Pascal (a, b + 1)

Is there a way to generate the following induction principle for free: if P : Nat × Nat → Nat → Prop is some family of predicates, true in the right base cases, and also if we have we have the right inductive hypothesis (it's complicated but approximately

if we have assigned Nat values to everything less than (a.succ, b.succ) as specified by a function A : ∀ y : Nat × Nat, sizeOf y < sizeOf (a.succ, b.succ) → Nat, and they all satisfy P for the right inputs, then the assignation of a Nat value according to the induction rule for (a.succ, b.succ) will also satisfy P for the right inputs

) then the statement is true for P (a, b) (Pascal (a, b)) for all (a, b)?

open SizeOf

theorem lt_left {a b : Nat} : sizeOf (a, b) < sizeOf (a.succ, b) :=
  Nat.add_lt_add_right (Nat.add_lt_add_left a.lt_succ_self _) _

theorem lt_right {a b : Nat} : sizeOf (a, b) < sizeOf (a, b.succ) :=
  Nat.add_lt_add_left b.lt_succ_self _

theorem Pascal.rec {P : Nat × Nat → Nat → Prop} (hP1 : ∀ j, P (0, j) 1) (hP2 : ∀ i, P (i, 0) 1)
    (hP : ∀ a b,
    ∀ (A : ∀ y : Nat × Nat, sizeOf y < sizeOf (a.succ, b.succ) → Nat),
    (∀ (y : Nat × Nat) (hy : sizeOf y < sizeOf (a.succ, b.succ)), P y (A y hy))
    → P (a.succ, b.succ) ((A (a.succ, b) lt_right) + (A (a, b.succ) lt_left)))
    (x : Nat × Nat) :
    P x (Pascal x) :=
  sorry

[Anne Baanen]

My first idea is to turn the inductive definition of Pascal into an inductive relation:

inductive PascalRel : Nat → Nat → Nat → Prop
  | zero_left {b} : PascalRel 0 b 1
  | zero_right {a} : PascalRel a 0 1
  | succ_succ {a b m n} : PascalRel (a + 1) b m → PascalRel a (b + 1) n → PascalRel (a + 1) (b + 1) (m + n)

Wouldn't the induction principle for PascalRel be exactly what you are looking for?

[Anne Baanen]

Looking at #print PascalRel.rec we'd need to do some rewriting (namely by using PascalRel a b n ↔ n = Pascal a b), but I think it's close to what you're looking for.

recursor PascalRel.rec : ∀ {motive : (a a_1 a_2 : Nat) → PascalRel a a_1 a_2 → Prop},
  (∀ {b : Nat}, motive 0 b 1 (_ : PascalRel 0 b 1)) →
    (∀ {a : Nat}, motive a 0 1 (_ : PascalRel a 0 1)) →
      (∀ {a b m n : Nat} (a_1 : PascalRel (a + 1) b m) (a_2 : PascalRel a (b + 1) n),
          motive (a + 1) b m a_1 →
            motive a (b + 1) n a_2 → motive (a + 1) (b + 1) (m + n) (_ : PascalRel (a + 1) (b + 1) (m + n))) →
        ∀ {a a_1 a_2 : Nat} (t : PascalRel a a_1 a_2), motive a a_1 a_2 t