Two induction principles

Stream: Is there code for X?

[Stuart Presnell]

Do we have the following induction principles? First,

def pincer_induction {P : ℕ → ℕ → Sort*} (Ha0 : ∀ a : ℕ, P a 0) (H0b : ∀ b : ℕ, P 0 b)
  (H : ∀ x y : ℕ, P x y.succ → P x.succ y → P x.succ y.succ) : Π (n m : ℕ), P n m := sorry

or (from @Chris Birkbeck's #14828)

def strong_sub_induction {P : ℕ → ℕ → Sort*}
  (H : ∀ n m, (∀ x y, x < n → y < m → P x y) → P n m) : Π (n m : ℕ), P n m := sorry

If not, are they worth PRing?

[Chris Birkbeck]

Yes good question. I couldn't find the one I wrote and Ive been meaning to ask if it's worth PRIng.

[Violeta Hernández]

I'm weakly opposed to having these in the library, since they're both just special cases of induction on prod.lex (<) (<).

[Violeta Hernández]

In fact, I believe the equation compiler should be able to do these sorts of inductions automatically

[Violeta Hernández]

Oh actually this isn't quite the case for pincer_induction but it is the case for strong_sub_induction

[Violeta Hernández]

def strong_sub_induction {P : ℕ → ℕ → Sort*}
  (H : ∀ n m, (∀ x y, x < n → y < m → P x y) → P n m) : Π (n m : ℕ), P n m
| n m := H n m (λ x y hx hy, strong_sub_induction x y)

[Stuart Presnell]

Oh, very nice, thanks!

[Violeta Hernández]

I guess we could still have the second theorem, since using the equation compiler in the middle of a proof isn't really something you can do

[Stuart Presnell]

#15061
Very open to suggestions for better names and/or docstrings!