Theorems · Definition · logic and foundations

Relation.CutExpand

{α : Type u_1} → (α → α → Prop) → Multiset α → Multiset α → Prop

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.

Defined in

Mathlib.Logic.Hydra

Cited by

19 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound