Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
4135674021
This PR introduces a new `grind` option, `funCC` (enabled by default),
which extends congruence closure to *function-valued* equalities. When
`funCC` is enabled, `grind` tracks equalities of **partially applied
functions**, allowing reasoning steps such as:
```lean
a : Nat → Nat
f : (Nat → Nat) → (Nat → Nat)
h : f a = a
⊢ (f a) m = a m
g : Nat → Nat
f : Nat → Nat → Nat
h : f a = g
⊢ f a b = g b
```
Given an application `f a₁ a₂ … aₙ`, when `funCC := true` and function
equality is enabled for `f`, `grind` generates and tracks equalities for
all partial applications:
* `f a₁`
* `f a₁ a₂`
* …
* `f a₁ a₂ … aₙ`
This allows equalities such as `f a₁ = g` to propagate through further
applications.
**When is function equality enabled for a symbol?**
Function equality is enabled for `f` in the following cases:
1. `f` is **not a constant** (e.g., a lambda, a local function, or a
function parameter).
2. `f` is a **structure field projection**, provided the structure is
**not a `class`**.
3. `f` is a constant marked with `@[grind funCC]`
Users can also enable function equality for specific constants in a
single call using:
```lean
grind [funCC f, funCC g]
```
**Examples:**
```lean
example (m : Nat) (a : Nat → Nat) (f : (Nat → Nat) → (Nat → Nat)) (h : f a = a) :
f a m = a m := by
grind
example (m : Nat) (a : Nat → Nat) (f : (Nat → Nat) → (Nat → Nat)) (h : f a = a) :
f a m = a m := by
fail_if_success grind -funCC -- fails if `funCC` is disabled
grind
```
```lean
example (a b : Nat) (g : Nat → Nat) (f : Nat → Nat → Nat) (h : f a = g) :
f a b = g b := by
grind
example (a b : Nat) (g : Nat → Nat) (f : Nat → Nat → Nat) (h : f a = g) :
f a b = g b := by
fail_if_success grind -funCC
grind
```
**Enabling per-symbol with parameters or attributes**
```lean
opaque f : Nat → Nat → Nat
opaque g : Nat → Nat
example (a b c : Nat) : f a = g → b = c → f a b = g c := by
grind [funCC f, funCC g]
attribute [grind funCC] f g
example (a b c : Nat) : f a = g → b = c → f a b = g c := by
grind
```
This feature substantially improves `grind`’s support for higher-order
and partially-applied function equalities, while preserving
compatibility with first-order SMT behavior when `funCC` is disabled.
Closes #11309
|
||
|---|---|---|
| .claude | ||
| .github | ||
| doc | ||
| images | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .gitpod.Dockerfile | ||
| .gitpod.yml | ||
| .ignore | ||
| CMakeLists.txt | ||
| CMakePresets.json | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| flake.lock | ||
| flake.nix | ||
| lean-toolchain | ||
| lean.code-workspace | ||
| 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.