refactor: 1. split Plfl/Init to 3 files, 2. update version to v4.31.0

[srghma]

the only interesting thing is that when PDecidable is written as class - need to use @[reducible] on functions that return PDecidable

[rami3l]

For this I think it'd be reasonable to wait for the mathlib people on leanprover-community/mathlib4#39751.

• Maybe it's useful and we can just use the mathlib type once included?
• Or this is not useful enough and the introduction of this type makes little sense?
• Or Decidable' was my bad hack and the proof can be done otherwise? I didn't have time to check...

[srghma]

I will make pr, but dont I think they will merge it

[Copilot]

⚠️ Human review recommended

It includes a toolchain/dependency bump plus a cross-cutting refactor of foundational modules/types, which warrants a human-verified full build and downstream impact check.

Pull request overview

This PR refactors the project’s foundational “Init” layer by splitting it into separate modules, introduces PDecidable as a replacement for the former Decidable', and updates downstream modules accordingly; it also bumps the Lean/mathlib toolchain versions and adjusts a handful of proofs/definitions to remain compatible.

Changes:

• Replace Decidable' with PDecidable (as an inductive class) and update inference code to use .isTrue/.isFalse.
• Split Plfl.Init into Plfl.Init.Tactics, Plfl.Init.Lemmas, and Plfl.Init.PDecidable, updating imports across the codebase (and removing Plfl/Init.lean).
• Bump Lean + mathlib versions (and update Lake config/manifest), with small proof tweaks and converting some non-typeclass instance declarations to def.

File summaries

File	Description
Plfl/Untyped/Substitution.lean	Proof adjustment to work with the refactor (simp/convert changes).
Plfl/Untyped/Denotational/Soundness.lean	Proof tweaks to preserve soundness lemmas after refactor.
Plfl/Untyped/Denotational/ContextualEquivalence.lean	Drop Plfl.Init import; rely on updated import graph.
Plfl/Untyped/Denotational/Compositional.lean	Drop Plfl.Init import; rely on updated import graph.
Plfl/Untyped/Denotational/Adequacy.lean	Drop Plfl.Init import; rely on updated import graph.
Plfl/Untyped/Denotational.lean	Drop Plfl.Init import; rely on updated import graph.
Plfl/Untyped/Confluence.lean	Convert non-typeclass instance equivalence to def and tweak pattern-matching proof style.
Plfl/Untyped/BigStep.lean	Drop Plfl.Init import; rely on updated import graph.
Plfl/Untyped.lean	Convert non-typeclass instance equivalences to def and drop Plfl.Init import.
Plfl/More/Inference.lean	Switch from Decidable' to PDecidable throughout bidirectional inference and examples.
Plfl/More/DoubleSubst.lean	Update imports to pull in the split Init pieces explicitly.
Plfl/More/Bisimulation.lean	Drop Plfl.Init import; rely on updated import graph.
Plfl/More.lean	Adjust Init import strategy as part of the split.
Plfl/Lambda/Properties.lean	Update Init import usage and convert non-typeclass instance equivalences to def.
Plfl/Lambda.lean	Drop Plfl.Init import and convert a non-typeclass instance embedding to def.
Plfl/Init/Tactics.lean	New module extracted from former Plfl.Init (defines is_empty tactic).
Plfl/Init/PDecidable.lean	New PDecidable definition plus helpers (toDecidable, get) and Repr.
Plfl/Init/Lemmas.lean	New module extracted from former Plfl.Init (e.g., congr_arg₃).
Plfl/Init.lean	Removed; its contents are now split across Plfl/Init/*.
Plfl/DeBruijn.lean	Update Init import to the new split module(s).
Plfl.lean	Stop re-exporting Plfl.Init (consistent with its removal).
lean-toolchain	Bump Lean toolchain to v4.31.0.
lakefile.toml	Bump mathlib to v4.31.0 and adjust aesop requirement configuration.
lake-manifest.json	Update pinned dependency revisions to match the new toolchain/deps.

Copilot's findings

• Files reviewed: 24/24 changed files
• Comments generated: 4

Note

Your feedback helps us improve the quality of this feature.
Please use 👍 or 👎 to tell us whether this assessment is correct.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[srghma]

@rami3l done