feat: functional induction #3432

nomeata · 2024-02-21T11:04:24Z

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.

leanprover-community-mathlib4-bot · 2024-02-21T11:21:02Z

Mathlib CI status (docs):

❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c9aea32d3e1da1287d099d41dcec831dc5151610 --onto 8b8e001794e6a8b481d37f24fa77bb07797682a1. (2024-02-21 11:21:01)
❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 88fbe2e5313bb418abdb035c48cae2680ea9bcea --onto 5b15e1a9f3c0d1283df7f2e2f3f1b1dc59f92cf6. (2024-02-25 22:49:29)
❗ Std CI can not be attempted yet, as the nightly-testing-2024-02-26 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-02-26 11:15:17)
💥 Mathlib branch lean-pr-testing-3432 build failed against this PR. (2024-02-27 20:17:00) View Log
💥 Mathlib branch lean-pr-testing-3432 build failed against this PR. (2024-02-27 21:41:56) View Log
💥 Mathlib branch lean-pr-testing-3432 build failed against this PR. (2024-02-28 09:56:31) View Log
💥 Mathlib branch lean-pr-testing-3432 build failed against this PR. (2024-02-28 11:03:30) View Log
💥 Mathlib branch lean-pr-testing-3432 build failed against this PR. (2024-02-28 14:11:55) View Log
💥 Mathlib branch lean-pr-testing-3432 build failed against this PR. (2024-02-28 18:20:20) View Log
💥 Mathlib branch lean-pr-testing-3432 build failed against this PR. (2024-02-29 11:43:08) View Log
❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b9f9ce874dcbc31acbaf3a09ae547c5546d087f5 --onto 5a330917326cfc6e8afd37c0b78a72ccb9d1f09d. (2024-02-29 14:21:39)

PR #3432 will introduce more operations on `MatcherApp`, including somet that have more dependencies. This change prepares by introducing `Lean.Meta.Match.MatcherApp.Basic` for the basic definition, and `Lean.Meta.MatcherApp.Transform` for the transformations, currently `addArg` and `refineThrough`, but more to come.

david-christiansen · 2024-02-26T08:45:44Z

src/Lean/Meta/Basic.lean

+Removes `fvarId` from the local context, and replaces occurrences of it with `e`.
+It is the responsibility of the caller to ensure that `e` is well-typed in the context
+of any occurrence of `fvarId`.


This operation sounds like "substitution" to me, but you're not using that terminology. Why not?

No deep reason, just out of consistency with existing function names and doc strings: https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.Expr.replaceFVar

src/Lean/Meta/Match/MatchEqs.lean

src/Lean/Meta/Match/MatcherApp/Transform.lean

david-christiansen · 2024-02-26T08:51:32Z

src/Lean/Meta/Match/MatcherApp/Transform.lean

+/--
+Performs a possibly type-changing transformation to a `MatcherApp`.
+
+* `onParams` is run on each parameter and discrimitant


I don't know the term "discrimitant", and my dictionary doesn't either. Is this specialized technical vocabulary, or should it be "scrutinee"?

Scrurtinee seems to be mostly GHC lingo, and discrs is used in the lean code base. 🤷‍♂️

Suggested change

* `onParams` is run on each parameter and discrimitant

* `onParams` is run on each parameter and discriminant

Consistency is good here!

"Scrutinee" is also what we called it in Idris 1, but there were plenty of GHC-isms in that code as well, like "zonk".

Though "-ant" is "a person or thing performing or causing the stated action". But the thing we're talking about here is not that which is causing discrimination to occur, it's that which is being subject to discrimination. "Discriminee" isn't in any English dictionaries that I could find, but it follows the regular pattern of "-ee" pointing at the object of a verb.

Indeed googling shows up Coq docs that (occasionally? rarely?) use of discriminee, but never discriminant.

But yet:

~/build/lean/lean4 $ git grep discriminant|wc -l 84 ~/build/lean/lean4 $ git grep discriminee|wc -l 0

I don’t mind changing that, but if we do, then everywhere separate of this PR.

Do we need a little “glossary and nomenclature” document somewhere where we can keep track of such decisions?

"scrutinee" is also used in the Rust reference: https://doc.rust-lang.org/reference/expressions/match-expr.html#match-expressions

src/Lean/Meta/Match/MatcherApp/Transform.lean

src/Lean/Meta/Tactic/FunInd.lean

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 <[email protected]> Co-authored-by: Leonardo de Moura <[email protected]>

github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 21, 2024 11:17 Inactive

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 21, 2024

nomeata mentioned this pull request Feb 21, 2024

refactor: module MatcherApp.Transform #3439

Merged

github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 21, 2024 13:29 Inactive

leodemoura force-pushed the code_action branch 2 times, most recently from 98452f1 to 9daaadb Compare February 25, 2024 19:02

nomeata force-pushed the joachim/funind branch from fec130b to 4c65206 Compare February 25, 2024 22:32

nomeata changed the base branch from code_action to master February 25, 2024 22:32

nomeata marked this pull request as ready for review February 25, 2024 22:33

nomeata requested review from Kha and leodemoura as code owners February 25, 2024 22:33

github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 25, 2024 22:45 Inactive