Termination of a hydra game.

cut_expand_wf.lean

import data.multiset.basic

section relation
variables {α β : Type*} (rα : α → α → Prop) (r r' : β → β → Prop) (f : α → β)

lemma acc.of_fibration (fib : ∀ {a b}, r b (f a) → ∃ a', rα a' a ∧ f a' = b)
  (a : α) (ha : acc rα a) : acc r (f a) :=
begin
  induction ha with a ha ih,
  refine acc.intro (f a) (λ b hr, _),
  obtain ⟨a', hr', rfl⟩ := fib hr,
  exact ih a' hr',
end

end relation

section game_add
variables {α β : Type*} (rα rα' : α → α → Prop) (rβ rβ' : β → β → Prop)

inductive game_add : α × β → α × β → Prop
| fst {a a' b} : rα a a' → game_add (a,b) (a',b)
| snd {a b b'} : rβ b b' → game_add (a,b) (a,b')

variables {rα rβ}
lemma acc.game_add {a : α} {b : β} (ha : acc rα a) (hb : acc rβ b) :
  acc (game_add rα rβ) (a, b) :=
begin
  induction ha with a ha iha generalizing b,
  induction hb with b hb ihb,
  refine acc.intro _ (λ h, _),
  rintro (⟨_,_,_,ra⟩|⟨_,_,_,rb⟩),
  exacts [iha _ ra (acc.intro b hb), ihb _ rb],
end
/- notice that this isn't true for `prod.lex`, so it requires a separate proof. -/

/- also PR downward closed, definition of fibration, well_founded game_add,
   acc trans_gen, acc cut_expand singleton -/

end game_add

section hydra_wf
open game_add multiset

variables {α : Type*} [decidable_eq α] (r : α → α → Prop)

/-- Cut one head `a` of a hydra `s`, and it grows back an arbitrary finite number of
  heads at "lower levels" than the head cut. -/
def cut_expand (s' s : multiset α) : Prop :=
∃ (t : multiset α) (a ∈ s), (∀ a' ∈ t, r a' a) ∧ s' = s.erase a + t

namespace cut_expand
/-! We follow the proof by Peter LeFanu Lumsdaine at https://mathoverflow.net/a/229084/3332 to
  show that `cut_expand r` is well-founded when `r` is. -/

lemma game_add_fibration ⦃ss : _ × _⦄ ⦃s : multiset α⦄
  (hc : cut_expand r s (ss.1 + ss.2)) :
  ∃ ss', game_add (cut_expand r) (cut_expand r) ss' ss ∧ ss'.1 + ss'.2 = s :=
begin
  obtain ⟨s₁, s₂⟩ := ss,
  obtain ⟨t, a, ha, hr, rfl⟩ := hc,
  obtain (h|h) := mem_add.1 ha,
  use [(s₁.erase a + t, s₂), fst ⟨t, a, h, hr, rfl⟩,
    by rw [s₂.erase_add_left_pos h, add_right_comm]],
  use [(s₁, s₂.erase a + t), snd ⟨t, a, h, hr, rfl⟩,
    by rw [s₁.erase_add_right_pos h, add_assoc]],
end

lemma acc_of_singleton (s : multiset α) :
  (∀ a ∈ s, acc (cut_expand r) {a}) → acc (cut_expand r) s :=
begin
  refine multiset.induction _ _ s,
  { exact λ _, acc.intro 0 (λ s, by rintro ⟨_, _, ⟨⟩, _⟩) },
  { intros a s ih hacc, rw ← s.singleton_add a,
    apply acc.of_fibration _ _ _ (game_add_fibration r) ({a}, s)
      ((hacc a $ s.mem_cons_self a).game_add $ ih $ λ a ha, hacc a $ mem_cons_of_mem ha) },
end

theorem _root_.well_founded.cut_expand (hr : well_founded r) : well_founded (cut_expand r) :=
begin
  suffices : ∀ a, acc (cut_expand r) {a},
  { exact ⟨λ s, acc_of_singleton r s $ λ a _, this a⟩ },
  refine λ a, hr.induction a (λ a ih, _),
  refine acc.intro _ (λ s, _),
  rintro ⟨t, a, ha, hr, rfl⟩,
  cases mem_singleton.1 ha,
  refine acc_of_singleton r _ (λ a', _),
  rw [erase_singleton, zero_add],
  exact ih a' ∘ hr a',
end

end cut_expand
end hydra_wf