## Induction principles from well-founded function definitions

In this repository I am prototyping a tool that takes a (well-founded) recursive function definition in Lean4, and derive a custom tailored induction principle that follows that function's execution paths.

Examples:

```
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)
```

produces

```
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
```

and

```
inductive Tree
| node : List Tree → Tree
def Tree.rev : Tree → Tree
| node ts => .node (ts.attach.map (fun ⟨t, _ht⟩ => t.rev) |>.reverse)
```

produces

```
Tree.rev.induct (motive : Tree → Prop)
(case1 : ∀ (ts : List Tree),
(∀ (t : Tree), t ∈ ts → motive t) →
motive (Tree.node ts))
(x : Tree) : motive x
```

This is work in progress, so do not use this in production yet.

I am interested in interesting and small test cases. Just talk to me (Joachim Breitner) on zulip.

### Implementation

The idea of the implemenation is to take the final function definition (in terms of `WellFounded.fix`

), which has all the decreasing proofs in it, and rewrite that definition into one that proves the desired induction principle. The steps are

- Unfold the definition to expose the
`WellFounded.fixF`

function. - Construct a suitable
`motive`

. - Replace its argument (with the
`oldIH`

argument) as follows: - For every recursive call (i.e. call to
`oldIH`

) we replace it with a call to the original function. - Also, for every call to
`oldIH`

, we pass its argument o`newIH`

to construct the induction hypothesis for this recursive call. - For top-level matches
- check if it is refining the
`oldIH`

; if it is, replace that with`newIH`

. - use the splitter, if present, to get extra assumptions for overlapping matches
- keep the match application

- check if it is refining the
- In the branches of the top-level matches
- Create a hole with the (refined)
`motive`

. - Pass all induction hypothese to that hole

- Create a hole with the (refined)
- Finally, abstract over all these holes.
- Profit.