Code

feat: functional induction#3432

Code

Merged

nomeata merged 51 commits intomasterleanprover/lean4:masterfrom joachim/funindleanprover/lean4:joachim/funindCopy head branch name to clipboardMar 5, 2024

+2,347-4

Commits

Commits on Feb 29, 2024

• stash shuffling MatcherApp modules

  nomeata

  committed
  6b0997f

  Copy full SHA for 6b0997f

• Add funind implementation

  nomeata

  committed
  95878ab

  Copy full SHA for 95878ab

• Make it a built-in command

  nomeata

  committed
  64bdcfc

  Copy full SHA for 64bdcfc

• More module shuffling

  nomeata

  committed
  0fa88b5

  Copy full SHA for 0fa88b5

• Apply suggestions from code review

  Show description for 5a708b2
  

  nomeata

  and

  david-christiansen

  committed
  5a708b2

  Copy full SHA for 5a708b2

• Apply suggestions from code review

  Show description for 5429b40
  

  nomeata

  and

  david-christiansen

  committed
  5429b40

  Copy full SHA for 5429b40

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

  nomeata

  committed
  1ea4317

  Copy full SHA for 1ea4317

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

  nomeata

  committed
  b429ba9

  Copy full SHA for b429ba9

• Update src/Lean/Meta/Tactic/FunInd.lean

  nomeata

  committed
  3fd16ee

  Copy full SHA for 3fd16ee

• Update src/Lean/Meta/Tactic/FunInd.lean

  nomeata

  committed
  1c9fa02

  Copy full SHA for 1c9fa02

• Update src/Lean/Meta/Tactic/FunInd.lean

  nomeata

  committed
  0f55eba

  Copy full SHA for 0f55eba

• Update src/Lean/Meta/Tactic/FunInd.lean

  nomeata

  committed
  569edcb

  Copy full SHA for 569edcb

• Refine docstring

  nomeata

  committed
  cd0b017

  Copy full SHA for cd0b017

• s/derive_induction/derive_functional_induction/

  nomeata

  committed
  d86a30d

  Copy full SHA for d86a30d

• Rewrote

  nomeata

  committed
  b5c7451

  Copy full SHA for b5c7451

• Rephrease intro

  nomeata

  committed
  2e29751

  Copy full SHA for 2e29751

• Less fun

  nomeata

  committed
  c8529d4

  Copy full SHA for c8529d4

• Update src/Lean/Meta/Tactic/FunInd.lean

  nomeata

  committed
  f7e285a

  Copy full SHA for f7e285a

• "k"

  nomeata

  committed
  351ce5e

  Copy full SHA for 351ce5e

• test: add new test with dependent types + mutual recursion

  

  leodemoura

  authored and

  nomeata

  committed
  417371f

  Copy full SHA for 417371f

• test: use generated functional induction principle in a simple proof

  

  leodemoura

  authored and

  nomeata

  committed
  f98dbaf

  Copy full SHA for f98dbaf

• test: another derive_functional_induction with dependent types

  

  leodemoura

  authored and

  nomeata

  committed
  56f5722

  Copy full SHA for 56f5722

• Extend Leo’s examples with uses of induction

  nomeata

  committed
  fecd23f

  Copy full SHA for fecd23f

• Avoid inferType in MatcherApp.transform

  nomeata

  committed
  7f0e41a

  Copy full SHA for 7f0e41a

• Also split tail-recursive non-refining matches

  nomeata

  committed
  435ab9a

  Copy full SHA for 435ab9a

• More careful unfolding and better error messages

  nomeata

  committed
  e5f9b91

  Copy full SHA for e5f9b91

• Revert "Also split tail-recursive non-refining matches"

  Show description for 93e5dd4
  nomeata

  committed
  93e5dd4

  Copy full SHA for 93e5dd4

• Use ih, not IH

  nomeata

  committed
  2d63347

  Copy full SHA for 2d63347

• Rename tests to all start with funind_

  nomeata

  committed
  6ad86ad

  Copy full SHA for 6ad86ad

• document why we don’t split all match applications yet

  nomeata

  committed
  ce16d1a

  Copy full SHA for ce16d1a

• More example of functions that we probably want to case-split

  nomeata

  committed
  08bb472

  Copy full SHA for 08bb472

• More tests

  nomeata

  committed
  4c7f198

  Copy full SHA for 4c7f198

• Also split tail-recursive non-refining matches

  nomeata

  committed
  534695a

  Copy full SHA for 534695a

• Abstract goal

  nomeata

  committed
  f837dec

  Copy full SHA for f837dec

• Use substVars

  nomeata

  committed
  35850c2

  Copy full SHA for 35850c2

• Revert "Use substVars", causes unresolved mvars

  Show description for 4138a89
  nomeata

  committed
  4138a89

  Copy full SHA for 4138a89

• Refactor out mkLambdaFVarsMasked

  nomeata

  committed
  8f15e23

  Copy full SHA for 8f15e23

• Add equalities to transformed match

  nomeata

  committed
  f13d9a6

  Copy full SHA for f13d9a6

• Do not duplicate equalities when they are already there

  nomeata

  committed
  2a65a0c

  Copy full SHA for 2a65a0c

• Update docs

  nomeata

  committed
  ad61827

  Copy full SHA for ad61827

• Use substVars to simplify induction

  nomeata

  committed
  1380721

  Copy full SHA for 1380721

• Reverting later improves order of cases? oh wey

  nomeata

  committed
  d9f9e2c

  Copy full SHA for d9f9e2c

Commits on Mar 4, 2024

• Avoid mkAppN with fixed length arrays

  nomeata

  committed
  11d5ba1

  Copy full SHA for 11d5ba1

• Merge branch 'master' of github.com:leanprover/lean4 into joachim/funind

  nomeata

  committed
  0d5edef

  Copy full SHA for 0d5edef

• Some cleanupAnnotation

  nomeata

  committed
  ba96cfc

  Copy full SHA for ba96cfc

• More cleanupAnnotations

  nomeata

  committed
  3acb55d

  Copy full SHA for 3acb55d

Commits on Mar 5, 2024

• Revert experiments done to work around #3595

  nomeata

  committed
  df6183a

  Copy full SHA for df6183a

• Merge branch 'master' of github.com:leanprover/lean4 into joachim/funind

  nomeata

  committed
  6fa0b3d

  Copy full SHA for 6fa0b3d

• Update test again

  nomeata

  committed
  9755115

  Copy full SHA for 9755115

• Add RELEASES entry

  nomeata

  committed
  6ea3389

  Copy full SHA for 6ea3389

• Disable liasolver on windows

  nomeata

  committed
  29ec55b

  Copy full SHA for 29ec55b