8038604d3e
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> |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||