Tactic for game inequalities

This file defines the game_cmp tactic, capable of proving inequalities between games. See its docstring for more info.

Tests for the tactic are found in the CombinatorialGames.Test file.

def tacticGame_cmp : Lean.ParserDescr

Proves simple inequalities on concrete games.

This tactic works by repeatedly unfolding the definition of ≤ and applying simp lemmas tagged with game_cmp until the goal is solved. It is effective on any game whose moves can be "enumerated" by simp, in the sense that a quantifier over its moves can be written in a quantifier-less way. For instance, ∀ y ∈ leftMoves {{0, 1} | {2, 3}}ᴵ, P y can be simplified into P 0 ∧ P 1.

Which lemmas to tag

Lemmas which are safe to tag with game_cmp are the following:

• Lemmas of the form (∀ y ∈ leftMoves (f x), P y) ↔ _ and analogous, as long as any quantifiers in the simplified form are over left or right moves of simpler games.
• Lemmas of the form leftMoves (f x) = _ and analogous, as long as the simplified set is of the form {x₁, x₂, …}, listing out all elements explicitly.
• Lemmas which directly replace games by other simpler games.

Tagging any other lemmas might lead to simp failing to eliminate all quantifiers, and getting stuck in a goal that it can't solve.

Equations

• tacticGame_cmp = Lean.ParserDescr.node `tacticGame_cmp 1024 (Lean.ParserDescr.nonReservedSymbol "game_cmp" false)

Extra tagged lemmas

theorem Set.exists_mem_empty {α : Type u_1} {P : α → Prop} : (∃ x ∈ ∅, P x) ↔ False

theorem Set.forall_singleton {α : Type u_1} {P : α → Prop} {x : α} : (∀ y ∈ {x}, P y) ↔ P x

theorem Set.exists_singleton {α : Type u_1} {P : α → Prop} {x : α} : (∃ y ∈ {x}, P y) ↔ P x

theorem Set.forall_insert {α : Type u_1} {P : α → Prop} {x : α} {y : Set α} : (∀ z ∈ insert x y, P z) ↔ P x ∧ ∀ z ∈ y, P z

theorem Set.exists_insert {α : Type u_1} {P : α → Prop} {x : α} {y : Set α} : (∃ z ∈ insert x y, P z) ↔ P x ∨ ∃ z ∈ y, P z

theorem forall_lt_zero {P : ℕ → Prop} : (∀ n < 0, P n) ↔ True

theorem exists_lt_zero {P : ℕ → Prop} : (∃ n < 0, P n) ↔ False

theorem forall_lt_one {P : ℕ → Prop} : (∀ n < 1, P n) ↔ P 0

theorem exists_lt_one {P : ℕ → Prop} : (∃ n < 1, P n) ↔ P 0