help proving well-foundedness

Stream: general

[Scott Morrison]

I am terrible at proving well-foundedness, apparently (or maybe just bad at telling when something is well-founded in the first place). Can anyone provide the proof of well-foundedness here:

universe u

inductive pgame : Type (u+1)
| mk : ∀ α β : Type u, (α → pgame) → (β → pgame) → pgame

namespace pgame

def left_moves : pgame → Type u
| (mk l _ _ _) := l
def right_moves : pgame → Type u
| (mk _ r _ _) := r

def move_left : Π (g : pgame), left_moves g → pgame
| (mk l _ L _) i := L i
def move_right : Π (g : pgame), right_moves g → pgame
| (mk _ r _ R) j := R j

inductive r : pgame → pgame → Prop
| left : Π (x : pgame) (i : x.left_moves), r (x.move_left i) x
| right : Π (x : pgame) (j : x.right_moves), r (x.move_right j) x
| trans : Π (x y z : pgame), r x y → r y z → r x z

theorem wf_r : well_founded r :=
begin
  sorry
end

end pgame

[Mario Carneiro]

theorem wf_r : well_founded r :=
⟨λ x, begin
  induction x with l r L R IHl IHr,
  refine ⟨_, λ y h, _⟩,
  generalize_hyp e : mk l r L R = x at h,
  induction h with _ i _ j a b _ h1 h2 IH1 IH2; subst e,
  { apply IHl },
  { apply IHr },
  { exact acc.inv (IH2 rfl) h1 }
end⟩

[Scott Morrison]

Wow! Not trivial. I feel less bad failing to do that. :-)

[Mario Carneiro]

the transitivity part is tricky. Usually I would have used the lemma that says the transitive closure of a wf relation is wf