A round of clean-up for the context of the functional induction
principle cases.
* Already previously, with `match e with | p => …`, functional induction
would ensure that `h : e = p` is in scope, but it wouldn’t work in
dependent cases. Now it introduces heterogeneous equality where needed
(fixes#4146)
* These equalities are now added always (previously we omitted them when
the discriminant was a variable that occurred in the goal, on the
grounds that the goal gets refined through the match, but it’s more
consistent to introduce the equality in any case)
* We no longer use `MVarId.cleanup` to clean up the goal; it was
sometimes too aggressive (fixes#5347)
* Instead, we clean up more carefully and with a custom strategy:
* First, we substitute all variables without a user-accessible name, if
we can.
* Then, we substitute all variable, if we can, outside in.
* As we do that, we look for `HEq`s that we can turn into `Eq`s to
substitute some more
* We substitute unused `let`s.
**Breaking change**: In some cases leads to a different functional
induction principle (different names and order of assumptions, for
example).
Previously, the tactic state shown at `decreasing_by` would leak lots of
details about the translation, and mention `invImage`, `PSigma` etc.
This is not nice.
So this introduces `clean_wf`, which is like `simp_wf` but using
`simp`'s `only` mode, and runs this unconditionally. This should clean
up the goal to a reasonable extent.
Previously `simp_wf` was an unrestricted `simp […]` call, but we
probably don’t want arbitrary simplification to happen at this point, so
this now became `simp only` call. For backwards compatibility,
`decreasing_with` begins with `try simp`. The `simp_wf` tactic
is still available to not break too much existing code; it’s docstring
suggests to no longer use it.
With `set_option cleanDecreasingByGoal false` one can disable the use of
`clean_wf`. I hope this is only needed for debugging and understanding.
Migration advise: If your `decreasing_by` proof begins with `simp_wf`,
either remove that (if the proof still goes through), or replace with
`simp`.
I am a bit anxious about running even `simp only` unconditionally here,
as it may do more than some user might want, e.g. because of options
like `zetaDelta := true`. We'll see if we need to reign in this tactic
some more.
I wonder if in corner cases the `simp_wf` tactic might be able to close
the goal, and if that is a problem. If so, we may have to promote simp’s
internal `mayCloseGoal` parameter to a simp configuration option and use
that here.
fixes#4928
This refactoring PR changes the structure of the `FunInd` module, with
the main purpose to make it easier to support mutual structural
recursion.
In particular the recursive calls are now longer recognized by their
terms (simple for well-founded recursion, `.app oldIH [arg, proof]`, but
tedious for structural recursion and even more so for mutual structural
recursion), but the type after replacing `oldIH` with `newIH`, where the
type will be simply and plainly `mkAppN motive args`).
We also no longer try to guess whether we deal with well-founded or
structural recursion but instead rely on the `EqnInfo` environment
extensions. The previous code tried to handle both variants, but they
differ too much, so having separate top-level functions is easier.
This also fuses the `foldCalls` and `collectIHs` traversals and
introduces a suitable monad for collecting the inductive hypotheses.
no need to enter `derive_functional_induction` anymore.
(Will remove the support for `derive_functional_induction` after the
next stage0 update, since we are already using it in Init.)
This extends `derive_functional_induction` to work with structural
recursion as well.
It produces the less general, more concrete induction rule where the
induction hypothesis is
specialized for every argument of the recursive call, not just the the
one that the function
is recursing on.
Care is taken so that the induction principle and it's motive take the
arguments in the same
order as the original function.
While I was it, also makes sure that the order of the cases in the
induction principle matches
the order of recursive calls in the function better.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
Sets the default value to `pp.fieldNotation.generalized` to `true`.
Updates tests, and fixes some minor flaws in the implementation of the
generalized field notation pretty printer.
Now generalized field notation won't be used for any function that has a
`motive` argument. This is intended to prevent recursors from pretty
printing using it as (1) recursors are more like control flow structures
than actual functions and (2) generalized field notation tends to cause
elaboration problems for recursors.
Note: be sure functions that have an `@[app_unexpander]` use
`@[pp_nodot]` if applicable. For example, `List.toArray` needs
`@[pp_nodot]` to ensure the unexpander prints it using `#[...]`
notation.
This attribute, which was implemented in #3640, is applied to the
following structures: `Sigma`, `PSigma`, `PProd`, `And`, `Subtype`, and
`Fin`. These were given this attribute in Lean 3.
using the `substVars` tactic on the goal can remove too much
information, as it does not take into account that the `motive` may
depend on the fixed parameters.
This is fixed by etracting `substVar` from `subst` which expects the
`x`, not the `h : x = rhs`, and then using this tactic on the local
declarations _after_ the `motive` exclusively.
This introduces the `ArgsPacker` module and abstraction, to replace the
exising `PackDomain`/`PackMutual` code. The motivation was that we now
have more uses besides `Fix.lean` (`GuessLex` and `FunInd`), and the
code was spread in various places.
The goals are
* consistent function naming withing the the `PSigma` handling, the
`PSum` handling, and the combined interface
* avoid taking a type apart just based on the `PSigma`/`PSum` nesting,
to be robust in case the user happens to be using `PSigma`/`PSum`
somewhere. Therefore, always pass an `arity` or `numFuncs` or `varNames`
around.
* keep all the `PSigma`/`PSum` encoding logic contained within one
module (`ArgsPacker`), and keep that module independent of its users (so
no `EqnInfos` visible here).
* pick good variable names when matching on a packed argument
* the unary function now is either called `fun1._unary` or
`fun1._mutual`, never `fun1._unary._mutual`.
This file has less heavy dependencies than `PackMutual` had, so build
parallelism is improved as well.
The `delabConstWithSignature` delaborator is responsible for pretty
printing constants with a declaration-like signature, with binders, a
colon, and a type. This is used by the `#check` command when it is given
just an identifier.
It used to accumulate binders from pi types indiscriminately, but this
led to unfriendly behavior. For example, `#check String.append` would
give
```
String.append (a✝ : String) (a✝¹ : String) : String
```
with inaccessible names. These appear because `String.append` is defined
using patterns, so it never names these parameters.
Now the delaborator stops accumulating binders once it reaches an
inaccessible name, and for example `#check String.append` now gives
```
String.append : String → String → String
```
We do not synthesize names for the sake of enabling binder syntax
because the binder names are part of the API of a function — one can use
`(arg := ...)` syntax to pass arguments by name. The delaborator also
now stops accumulating binders once it reaches a parameter with a name
already seen before — we then rely on the main delaborator to provide
that parameter with a fresh name when pretty printing the pi type.
As a special case, instance parameters with inaccessible names are
included as binders, pretty printing like `[LT α]`, rather than
relegating them (and all the remaining parameters) to after the colon.
It would be more accurate to pretty print this as `[inst✝ : LT α]`, but
we make the simplifying assumption that such instance parameters are
generally used via typeclass inference. Likely `inst✝` would not
directly appear in pretty printer output, and even if it appears in a
hover, users can likely figure out what is going on. (We may consider
making such `inst✝` variables pretty print as `‹LT α›` or
`infer_instance` in the future, to make this more consistent.)
Something we note here is that we do not do anything to make sure
parameters that can be used as named arguments actually appear named
after the colon (nor do we assure that the names are the correct names).
For example, one sees `foo : String → String → String` rather than `foo
: String → (baz : String) → String`. We can investigate this later if it
is wanted.
We also give `delabConstWithSignature` a `universes` flag to enable
turning off pretty printing universe levels parameters.
Closes#2846
this makes the ugly `fst`/`snd` variable names in the functional
induction principles go away.
Ironically I thought in order to fix these name, I should touch the
mutual/n-ary argument packing code used for well-founded recursion, and
embarked on a big refactor/rewrite of that code, only to find that at
least this particular instance of the issue was somewhere else. Hence
breaking this into its own PR; the refactoring will follow (and will
also improve some other variable names.)
This adds the concept of **functional induction** to lean.
Derived from the definition of a (possibly mutually) recursive function,
a **functional
induction principle** is tailored to proofs about that function. For
example from:
```
def ackermann : Nat → Nat → Nat
| 0, m => m + 1
| n+1, 0 => ackermann n 1
| n+1, m+1 => ackermann n (ackermann (n + 1) m)
derive_functional_induction ackermann
```
we get
```
ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
(case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
(case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m))
(x x : Nat) : motive x x
```
At the moment, the user has to ask for the functional induction
principle explicitly using
```
derive_functional_induction ackermann
```
The module docstring of `Lean/Meta/Tactic/FunInd.lean` contains more
details on the
design and implementation of this command.
More convenience around this (e.g. a `functional induction` tactic) will
follow eventually.
This PR includes a bunch of `PSum`/`PSigma` related functions in the
`Lean.Tactic.FunInd`
namespace. I plan to move these to `PackArgs`/`PackMutual` afterwards,
and do some cleaning
up as I do that.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
