Combining Nat-indexed binary relations

Stream: general

[Peter Nelson]

Is there a way to do the following with the equation compiler? If not, is there a natural definition where using induction to prove transitivity etc isn't painful?

import Mathlib.Tactic

def ranked_le {α : ℕ → Type} (r : (i : ℕ) → α i → α (i+1) → Prop) (a b : (i : ℕ) × (α i)) : Prop :=
  sorry
-- `ranked_le ⟨i,a⟩ ⟨j,b⟩` means that `either `i = j` and `a = b`, or that `i < j` and
-- there is some `b' : α (j-1)` with `ranked_le ⟨i,a⟩ ⟨j-1,b'⟩` and `r (j-1) b' b`.
-- eg `ranked_le ⟨2,a⟩ ⟨5,b⟩` holds if `r 2 a x`, `r 3 x y` and `r 4 y b` for some `x` and `y`.

[Kyle Miller]

Maybe this is a reasonable place to use a Prop-valued inductive type?

[Kyle Miller]

inductive RankedLE {α : ℕ → Type} (r : (i : ℕ) → α i → α (i+1) → Prop) :
    (i : ℕ) × (α i) → (i' : ℕ) × (α i') → Prop where
  | base (i : ℕ) (a : α i) : RankedLE r ⟨i, a⟩ ⟨i, a⟩
  | step (i j : ℕ) (h : i < j) (a : α i) (b' : α j) (b : α (j + 1)):
    r j b' b → RankedLE r ⟨i,a⟩ ⟨j,b'⟩ → RankedLE r ⟨i,a⟩ ⟨j+1,b⟩

[Kyle Miller]

It'd be easier to work with, so that you can do cases/induction, if you changed this so that it didn't use Sigma.mk constructors in the indices.

[Kyle Miller]

Maybe this?

inductive RankedLE {α : ℕ → Type} (r : (i : ℕ) → α i → α (i+1) → Prop) :
    (i : ℕ) × (α i) → (i' : ℕ) × (α i') → Prop where
  | base (a : (i : ℕ) × α i) : RankedLE r a a
  | step (a b' b : (i : ℕ) × α i) (h1 : a.1 < b.1) (hi : b.1 = b'.1 + 1) :
    r b'.1 b'.2 (hi ▸ b.2) → RankedLE r a b' → RankedLE r a b

[Peter Nelson]

Thank you!