Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
10b2efba51
This PR Introduces new foundations for reasoning about monadic Lean
code. Eventually we will port `mvcgen` on top of these new foundations,
to make the framework more general and robust.
Key issues, new metatheory is supposed to solve are
- It gives more flexibility over what an assertion language for
pre-/post-conditions of monadic Hoare triples can be. In particular, any
`CompleteLattice` might become a pre-/post-condtions language, not only
`SPred`. It potentially gives an opportunity to reason about
probabilistic monads, where assertion language are distributions. This
also simplifies the metatheory of monadic Hoare triples, as it does not
require defining the notion of `SPred`, and allows users to work in a
fairly common interface of `CompleteLattice`
- It splits the post-conditions of Hoare triples/ WPs into two: (1)
`post` for post-conditions on terminating paths and (2) `epost` for
post-conditions on abrupt paths. Current foundations always bundle them
into a pair, which inevitably leads to constructing and eliminating such
pairs everywhere in the code.
- It relaxes some conditions that the current foundations require for
instantiating `WPMonad` type class. In particular we do not require `wp`
to distribute over `bind` any more. Instead, we require just `wp x (fun
x => wp (f x) post epost) epost ⊑ wp (x >>= f) post epost`, i.e. the
distributed `wp` must only imply the non-distributed one (and not
necessarily vice versa). With this we can define `WPMonad` for
Separation Logic, where `wp` only distributes over `bind` on
local-footprint computations.
- It solves some universe polymorphism issues. As now universe levels of
assertion languages are independent of universe levels in the monad, one
can define `WPMonad Id.{u} Prop EPost⟨⟩`, which means that for arbitrary
level `Id` the language for pre-/post-conditions is going to be just
`Prop` and the language for post-conditions on abrupt exits is idle.
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
|
||
|---|---|---|
| .claude | ||
| .github | ||
| .vscode | ||
| doc | ||
| images | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .gitpod.Dockerfile | ||
| .gitpod.yml | ||
| .ignore | ||
| AGENTS.md | ||
| CMakeLists.txt | ||
| CMakePresets.json | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| flake.lock | ||
| flake.nix | ||
| lean-toolchain | ||
| LICENSE | ||
| LICENSES | ||
| README.md | ||
| RELEASES.md | ||
This is the repository for Lean 4.
About
- Quickstart
- Homepage
- Theorem Proving Tutorial
- Functional Programming in Lean
- Documentation Overview
- Language Reference
- Release notes starting at v4.0.0-m3
- Examples
- External Contribution Guidelines
Installation
See Install Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean.