lean4

lean4 copied to clipboard

### Description If a nested inductive goes through a type that has an optional parameter, there is an "application type mismatch" failure from the `inductive` command. ### Steps to Reproduce...

kmill

fix: IndPred: track function's motive in a let binding, use withoutProofIrrelevance, no chaining

1

This is a variant of #4827, mostly to improve my understanding. When replacing recursive calls by the corresponding induction hypothesis, it replaces the use of `IndPredBelow.backwardsChaining` with a non-recursive search...

nomeata

fix: improve proof search in IndPredBelow

2

`MVarId.apply` is clever in the order it returns mvars, by putting those arising from non-dependent arguments first. If we lean on that behavior, this fixes #1672. H'T to @DanielFabian, this...

nomeata

refactor: IndPredBelow: use `apply_assumption`

1

when transforming the `match` statements in `IndPredBelow`, given a local variable `x : T`, we need to search for `hx : T.below x`. Previously this was done using the custom...

nomeata

fix: make cdot anonymous function notation handle ambiguous notation

1

Fixes an issue where each alternative in choice nodes would get their own arguments. Now cdot function expansion is aware of choice nodes. Also modifies the variable naming so that...

kmill

feat: let `unfold` do zeta-delta reduction of local definitions

2

This is "upstreaming" mathlib's `unfold_let` tactic by incorporating its functionality into `unfold`. Now `unfold` can, in addition to unfolding global definitions, unfold local definitions. An improvement to `unfold_let` is that...

kmill

cdot function notation fails to macro expand properly when there is ambiguous syntax

2

### Description If ambiguous notation appears inside a cdot function, then the function can end up with more arguments than expected since `expandCDot?` collects cdots from each alternative in choice...

kmill

refactor: deriving DecidableEq to use `termination_by structural`

4

now that we support structural mutual recursion, I expect that every `DecidableEq` instance be implemented using structural recursion, so let's be explicit about it.

nomeata

fix: IndPred: track function's motive in a let binding, use withoutProofIrrelevance

7

this improves support for structural recursion over inductive *predicates* when there are reflexive arguments. Consider ```lean inductive F: Prop where | base | step (fn: Nat → F) -- set_option...

nomeata

structural recursion over inductive predicates struggle with reflexive inductives

7

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Test your...

mik-jozef