simp fails to handle recursors

JasonGross commented 5 years ago

Prerequisites

[X] Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
  - Specifically, check out the wishlist, open RFCs, or feature requests.
- Reduced the issue to a self-contained, reproducible test case.

Description

@[simp]
def fact (n : ℕ) : ℕ :=
  nat.rec
    1
    (λ n' fact_n', (nat.succ n') * fact_n')
    n

example : fact 5 = 5 :=
begin
  simp [fact,has_mul.mul,nat.mul],
  simp [nat.rec]
-- 11:3: invalid simplification lemma 'nat.rec' (use command 'set_option trace.simp_lemmas true' for more details)
-- state:
-- ⊢ nat.rec 1 (λ (n' : ℕ), nat.mul (nat.succ n')) 5 = 5
end

If I remove [nat.rec], then instead I get the error:

11:3: simplify tactic failed to simplify
state:
⊢ nat.rec 1 (λ (n' : ℕ), nat.mul (nat.succ n')) 5 = 5

How am I supposed to simplify recursion?

Expected behavior: simp reduces things like nat.rec, int.rec, list.rec, etc

Actual behavior: simp does not reduce these things

Reproduces how often: [What percentage of the time does it reproduce?] 100%

Versions

$ lean --version
Lean (version 3.4.2, commit cbd2b6686ddb, Release)
$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 16.04.6 LTS
Release:        16.04
Codename:       xenial
$ uname -a
Linux jgross-Leopard-WS 4.4.0-161-generic #189-Ubuntu SMP Tue Aug 27 08:10:16 UTC 2019 x86_64 x86_64 x86_64 GNU/Linux

fpvandoorn commented 5 years ago

Hmm... There are a couple things going on here. I'm also replying to #2005

First of all, this is very un-idiomatic Lean. Much better would be to do
```
def fact : ℕ → ℕ
| 0     := 1
| (n+1) := (n+1) * fact n 
```

example : fact 5 = 5 := begin rw [fact], simp [fact], end

What's happening here is that when you define a definition using the equation compiler, Lean will automatically generate the corresponding rewrite rules for each case, and use those when you call `rw`/`simp`. 
If you don't use the equation compiler, you are encouraged to write those lemmas yourself for your definition of `fact`, and not rely on unfolding your definition.
* If this solution is not satisfactory to you, it is a bit hard to guess what you actually want. If you want to reduce this actual definition, without generating extra lemmas something like this works, but it is discouraged:
```lean
def fact (n : ℕ) : ℕ :=
  nat.rec
    1
    (λ n' fact_n', (nat.succ n') * fact_n')
    n

example : fact 5 = 5 :=
begin
  dsimp only [nat.has_one, bit0, bit1, nat.has_add, nat.add, nat.has_zero, fact],
end

Numerals in Lean can be pretty complex, internally. To see the actual expression a numeral is, use set_option pp.numerals false.
The best place to ask questions like this is the Zulip chat: https://leanprover.zulipchat.com/ We're happy to help there!

cipher1024 commented 5 years ago

Also, I'd like to add that development on Lean 3 have moved to https://github.com/leanprover-community/lean. This is where we put bug fixes and new features.

leanprover / lean3