feat(SetTheory/Game/PGame): dicotic pregames

[LeoDog896]

Adds the definition of dicotic pregames and that star is a dicotic pregame. A second pull request may introduce the lawnmower theorem for long and short games.

---

[github-actions]

PR summary a2264a14b3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ dicotic
+ star_dicotic

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[alreadydone]

This doesn't seem right; it's not even recursive, and you shouldn't use type equality since there are many types of the same cardinality. I think the following is correct:

/-- A game is dicotic if both players can move from every nonempty subposition of G. -/
def IsDicotic (x : PGame) : Prop :=
  (IsEmpty x.LeftMoves ∧ IsEmpty x.RightMoves) ∨
  (Nonempty x.LeftMoves ∧ Nonempty x.RightMoves ∧
    (∀ l : x.LeftMoves, IsDicotic (x.moveLeft l)) ∧
    ∀ r : x.RightMoves, IsDicotic (x.moveRight r))
termination_by x

and I think for a PR on dicotic games to be accepted it (or another PR depending on it) must prove this. This helps verify the definition is as intended.

[LeoDog896]

Indeed! I noticed the lack of a recursive definition, but stopped on dicotic games to prove that the equivalence class of games is formed in context of a lack of reversible and dominated options. Thanks for the syntax for a recursive definition, though!

That goal to prove the class dicotic games were equivalent to the class of small games was my goal for this PR.

I also missed using Nonempty there. Comparing for PEmpty was a mistake.