feat: port Logic.Hydra (#2290)

Co-authored-by: Jason Yuen <[email protected]>
Co-authored-by: int-y1 <[email protected]>
Co-authored-by: Scott Morrison <[email protected]>
Co-authored-by: ChrisHughes24 <[email protected]>

Mathlib.lean

@@ -1232,6 +1232,7 @@ import Mathlib.Logic.Equiv.Set
 import Mathlib.Logic.Function.Basic
 import Mathlib.Logic.Function.Conjugate
 import Mathlib.Logic.Function.Iterate
+import Mathlib.Logic.Hydra
 import Mathlib.Logic.IsEmpty
 import Mathlib.Logic.Lemmas
 import Mathlib.Logic.Nonempty

Mathlib/Data/Multiset/Basic.lean

@@ -158,9 +158,9 @@ protected theorem induction {p : Multiset α → Prop} (empty : p 0)
 #align multiset.induction Multiset.induction
 
 @[elab_as_elim]
-protected theorem induction_on {p : Multiset α → Prop} (s : Multiset α) (h₁ : p 0)
-    (h₂ : ∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)) : p s :=
-  Multiset.induction h₁ h₂ s
+protected theorem induction_on {p : Multiset α → Prop} (s : Multiset α) (empty : p 0)
+    (cons : ∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)) : p s :=
+  Multiset.induction empty cons s
 #align multiset.induction_on Multiset.induction_on
 
 theorem cons_swap (a b : α) (s : Multiset α) : a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s :=

Mathlib/Data/Multiset/Sections.lean

@@ -62,8 +62,8 @@ theorem sections_add (s t : Multiset (Multiset α)) :
 theorem mem_sections {s : Multiset (Multiset α)} :
     ∀ {a}, a ∈ Sections s ↔ s.Rel (fun s a => a ∈ s) a := by
   induction s using Multiset.induction_on
-  case h₁ => simp
-  case h₂ a a' ih => simp [ih, rel_cons_left, eq_comm]
+  case empty => simp
+  case cons a a' ih => simp [ih, rel_cons_left, eq_comm]
 
 #align multiset.mem_sections Multiset.mem_sections
 

Mathlib/Logic/Hydra.lean

@@ -0,0 +1,160 @@
+/-
+Copyright (c) 2022 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+
+! This file was ported from Lean 3 source module logic.hydra
+! leanprover-community/mathlib commit 48085f140e684306f9e7da907cd5932056d1aded
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Data.Finsupp.Lex
+import Mathlib.Data.Finsupp.Multiset
+import Mathlib.Order.GameAdd
+
+/-!
+# Termination of a hydra game
+
+This file deals with the following version of the hydra game: each head of the hydra is
+labelled by an element in a type `α`, and when you cut off one head with label `a`, it
+grows back an arbitrary but finite number of heads, all labelled by elements smaller than
+`a` with respect to a well-founded relation `r` on `α`. We show that no matter how (in
+what order) you choose cut off the heads, the game always terminates, i.e. all heads will
+eventually be cut off (but of course it can last arbitrarily long, i.e. takes an
+arbitrary finite number of steps).
+
+This result is stated as the well-foundedness of the `CutExpand` relation defined in
+this file: we model the heads of the hydra as a multiset of elements of `α`, and the
+valid "moves" of the game are modelled by the relation `CutExpand r` on `Multiset α`:
+`CutExpand r s' s` is true iff `s'` is obtained by removing one head `a ∈ s` and
+adding back an arbitrary multiset `t` of heads such that all `a' ∈ t` satisfy `r a' a`.
+
+We follow the proof by Peter LeFanu Lumsdaine at https://mathoverflow.net/a/229084/3332.
+
+TODO: formalize the relations corresponding to more powerful (e.g. Kirby–Paris and Buchholz)
+hydras, and prove their well-foundedness.
+-/
+
+
+namespace Relation
+
+open Multiset Prod
+
+variable {α : Type _}
+
+/-- The relation that specifies valid moves in our hydra game. `CutExpand r s' s`
+  means that `s'` is obtained by removing one head `a ∈ s` and adding back an arbitrary
+  multiset `t` of heads such that all `a' ∈ t` satisfy `r a' a`.
+
+  This is most directly translated into `s' = s.erase a + t`, but `Multiset.erase` requires
+  `DecidableEq α`, so we use the equivalent condition `s' + {a} = s + t` instead, which
+  is also easier to verify for explicit multisets `s'`, `s` and `t`.
+
+  We also don't include the condition `a ∈ s` because `s' + {a} = s + t` already
+  guarantees `a ∈ s + t`, and if `r` is irreflexive then `a ∉ t`, which is the
+  case when `r` is well-founded, the case we are primarily interested in.
+
+  The lemma `Relation.cutExpand_iff` below converts between this convenient definition
+  and the direct translation when `r` is irreflexive. -/
+def CutExpand (r : α → α → Prop) (s' s : Multiset α) : Prop :=
+  ∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ s' + {a} = s + t
+#align relation.cut_expand Relation.CutExpand
+
+variable {r : α → α → Prop}
+
+theorem cutExpand_le_invImage_lex [IsIrrefl α r] :
+    CutExpand r ≤ InvImage (Finsupp.Lex (rᶜ ⊓ (· ≠ ·)) (· < ·)) toFinsupp := by
+  rintro s t ⟨u, a, hr, he⟩
+  replace hr := fun a' ↦ mt (hr a')
+  classical
+  refine ⟨a, fun b h ↦ ?_, ?_⟩ <;> simp_rw [toFinsupp_apply]
+  · apply_fun count b  at he
+    simpa only [count_add, count_singleton, if_neg h.2, add_zero, count_eq_zero.2 (hr b h.1)]
+      using he
+  · apply_fun count a  at he
+    simp only [count_add, count_singleton_self, count_eq_zero.2 (hr _ (irrefl_of r a)),
+      add_zero] at he
+    exact he ▸ Nat.lt_succ_self _
+#align relation.cut_expand_le_inv_image_lex Relation.cutExpand_le_invImage_lex
+
+theorem cutExpand_singleton {s x} (h : ∀ x' ∈ s, r x' x) : CutExpand r s {x} :=
+  ⟨s, x, h, add_comm s _⟩
+#align relation.cut_expand_singleton Relation.cutExpand_singleton
+
+theorem cutExpand_singleton_singleton {x' x} (h : r x' x) : CutExpand r {x'} {x} :=
+  cutExpand_singleton fun a h ↦ by rwa [mem_singleton.1 h]
+#align relation.cut_expand_singleton_singleton Relation.cutExpand_singleton_singleton
+
+theorem cutExpand_add_left {t u} (s) : CutExpand r (s + t) (s + u) ↔ CutExpand r t u :=
+  exists₂_congr fun _ _ ↦ and_congr Iff.rfl <| by rw [add_assoc, add_assoc, add_left_cancel_iff]
+#align relation.cut_expand_add_left Relation.cutExpand_add_left
+
+theorem cutExpand_iff [DecidableEq α] [IsIrrefl α r] {s' s : Multiset α} :
+    CutExpand r s' s ↔
+      ∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t := by
+  simp_rw [CutExpand, add_singleton_eq_iff]
+  refine' exists₂_congr fun t a ↦ ⟨_, _⟩
+  · rintro ⟨ht, ha, rfl⟩
+    obtain h | h := mem_add.1 ha
+    exacts [⟨ht, h, erase_add_left_pos t h⟩, (@irrefl α r _ a (ht a h)).elim]
+  · rintro ⟨ht, h, rfl⟩
+    exact ⟨ht, mem_add.2 (Or.inl h), (erase_add_left_pos t h).symm⟩
+#align relation.cut_expand_iff Relation.cutExpand_iff
+
+theorem not_cutExpand_zero [IsIrrefl α r] (s) : ¬CutExpand r s 0 := by
+  classical
+  rw [cutExpand_iff]
+  rintro ⟨_, _, _, ⟨⟩, _⟩
+#align relation.not_cut_expand_zero Relation.not_cutExpand_zero
+
+/-- For any relation `r` on `α`, multiset addition `Multiset α × Multiset α → Multiset α` is a
+  fibration between the game sum of `CutExpand r` with itself and `CutExpand r` itself. -/
+theorem cutExpand_fibration (r : α → α → Prop) :
+    Fibration (GameAdd (CutExpand r) (CutExpand r)) (CutExpand r) fun s ↦ s.1 + s.2 := by
+  rintro ⟨s₁, s₂⟩ s ⟨t, a, hr, he⟩; dsimp at he ⊢
+  classical
+  -- Porting note: Originally `obtain ⟨ha, rfl⟩`
+  -- This is https://github.com/leanprover/std4/issues/62
+  obtain ⟨ha, hb⟩ := add_singleton_eq_iff.1 he
+  rw [hb]
+  rw [add_assoc, mem_add] at ha
+  obtain h | h := ha
+  · refine' ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, _⟩, _⟩
+    · rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
+    · rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]
+  · refine' ⟨(s₁, (s₂ + t).erase a), GameAdd.snd ⟨t, a, hr, _⟩, _⟩
+    · rw [add_comm, singleton_add, cons_erase h]
+    · rw [add_assoc, erase_add_right_pos _ h]
+#align relation.cut_expand_fibration Relation.cutExpand_fibration
+
+/-- A multiset is accessible under `CutExpand` if all its singleton subsets are,
+  assuming `r` is irreflexive. -/
+theorem acc_of_singleton [IsIrrefl α r] {s : Multiset α} (hs : ∀ a ∈ s, Acc (CutExpand r) {a}) :
+    Acc (CutExpand r) s := by
+  induction s using Multiset.induction
+  case empty => exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim
+  case cons a s ihs =>
+    rw [← s.singleton_add a]
+    rw [forall_mem_cons] at hs
+    exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)
+#align relation.acc_of_singleton Relation.acc_of_singleton
+
+/-- A singleton `{a}` is accessible under `CutExpand r` if `a` is accessible under `r`,
+  assuming `r` is irreflexive. -/
+theorem _root_.Acc.cutExpand [IsIrrefl α r] {a : α} (hacc : Acc r a) : Acc (CutExpand r) {a} := by
+  induction' hacc with a h ih
+  refine' Acc.intro _ fun s ↦ _
+  classical
+  simp only [cutExpand_iff, mem_singleton]
+  rintro ⟨t, a, hr, rfl, rfl⟩
+  refine' acc_of_singleton fun a' ↦ _
+  rw [erase_singleton, zero_add]
+  exact ih a' ∘ hr a'
+#align acc.cut_expand Acc.cutExpand
+
+/-- `CutExpand r` is well-founded when `r` is. -/
+theorem _root_.WellFounded.cutExpand (hr : WellFounded r) : WellFounded (CutExpand r) :=
+  ⟨have := hr.isIrrefl; fun _ ↦ acc_of_singleton fun a _ ↦ (hr.apply a).cutExpand⟩
+#align well_founded.cut_expand WellFounded.cutExpand
+
+end Relation