This PR adds support for inductive and coinductive predicates defined
using lattice theoretic structures on `Prop`. These are syntactically
defined using `greatest_fixpoint` or `least_fixpoint` termination
clauses for recursive `Prop`-valued functions. The functionality relies
on `partial_fixpoint` machinery and requires function definitions to be
monotone. For non-mutually recursive predicates, an appropriate
(co)induction proof principle (given by Park induction) is generated.
Summary of changes:
- `Interal.Order.Basic` now contains `CompleteLattice` class, as well as
version of Knaster-Tarski fixpoint theorem (with an associated Park
induction principle) for the internal use for defining (co)inductive
predicates. `Prop` is shown to have two complete lattice structures (one
given by implication order for defining inductive predicates, and one
given by reverse implication for defining coinductive predicates).
Additionally, proofs that lattices are closed under products and
function spaces are included.
- Partial fixpoint's `EqnInfo` now additionally carries an information
whether something is defined as a lattice-theoretic fixpoint or via
CCPOs.
- When constructing a (co)inductive predicate,`PartialFixpoint/Main`
builds an appropriate lattice structure on the type of the predicate
using product lattice, function space lattice and an appropriate lattice
instance on `Prop`.
- `PartialFixpoint/Eqns` is modified to be able to perform rewrite under
lattice-theoretic fixpoint construction
- `PartialFixpoint/Induction`contains a case split for handling of the
(co)inductive predicates. In the case of lattice-theoretic fixpoints, it
appropriately desugars the Park induction principle.
This implements the `termination_by structural` syntax proposed in
#3909.
I went with `termination_by structural` over, say,
`termination_by (config := {method := .structural})` mainly because it
was
easier to get going (otherwise I’d have to look into how to define
recursive
parsers, as `Parser.config` depends on `term` and `termination_by` is
part of
term. But also because I find it more ergonomic and aesthetic as a user.
But syntax can still change.
The `termination_by?` syntax will no longer force well-founded
recursion,
and instead the inferred `termination_by structurally` annotation will
be shown
if structural termination is possible.
While I was it, this fixes#4546 the easy way (log errors about but
otherwise
ignore incomplete `termination_by` sets for mutual recursion). Maybe we
get
multiple replacements (#4551), but even then this this good behavior.
Involves a bit of shuffling around `TerimationHints` (now validated for
a
clique already by `PreDefinition.main`) and `TerminationArguments` (now
lifted
out of the `WF` namespace, and a bit simplified).
Fixes#3909
---------
Co-authored-by: Richard Kiss <him@richardkiss.com>
This change
* moves `termination_by` and `decreasing_by` next to the function they
apply to
* simplify the syntax of `termination_by`
* apply the `decreasing_by` goal to all goals at once, for better
interactive use.
See the section in `RELEASES.md` for more details and migration advise.
This is a hard breaking change, requiring developers to touch every
`termination_by` in their code base. We decided to still do it as a
hard-breaking change, because supporting both old and new syntax at the
same time would be non-trivial, and not save that much. Moreover, this
requires changes to some metaprograms that developers might have
written, and supporting both syntaxes at the same time would make
_their_ migration harder.
until around 7fe6881 the way to define well-founded recursions was to
specify a `WellFoundedRelation` on the argument explicitly. This was
rather low-level, for example one had to predict the packing of multiple
arguments into `PProd`s, the packing of mutual functions into `PSum`s,
and the cliques that were calculated.
Then the current `termination_by` syntax was introduced, where you
specify the termination argument at a higher level (one clause per
functions, unpacked arguments), and the `WellFoundedRelation` is found
using type class resolution.
The old syntax was kept around as `termination_by'`. This is not used
anywhere in the lean, std, mathlib or the theorem-proving-in-lean
repositories,
and three occurrences I found in the wild can do without
In particular, it should be possible to express anything that the old
syntax
supported also with the new one, possibly requiring a helper type with a
suitable instance, or the following generic wrapper that now lives in
std
```
def wrap {α : Sort u} {r : α → α → Prop} (h : WellFounded r) (x : α) : {x : α // Acc r x}
```
Since the old syntax is unused, has an unhelpful name and relies on
internals, this removes the support. Now is a good time before the
refactoring that's planned in #2921.
The test suite was updated without particular surprises.
The parametric `terminationHint` parser is gone, which means we can
match on syntax more easily now, in `expandDecreasingBy?`.
