feat(Data/Nat/Fib/Basic): some API for `Nat.fib` #26962

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Open

themathqueen wants to merge 2 commits into leanprover-community:master from themathqueen:fib_api

+24 −0

Contributor

themathqueen commented Jul 10, 2025

Added some helpful lemmas for Nat.fib.


          some api for Nat.fib

11a2d1f

github-actions bot added new-contributor t-data labels

github-actions bot commented Jul 10, 2025 •

edited

Loading

PR summary 1ec99bd9a0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ fib_add_ne_zero
+ fib_add_sub_one
+ fib_sub_one
+ fib_succ_sub_fib_pred

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

vihdzp reviewed

View reviewed changes

Collaborator

vihdzp left a comment

These results all seem kind of fishy to me; natural number subtraction is usually something to be avoided. Nevertheless, some comments.

Mathlib/Data/Nat/Fib/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Data/Nat/Fib/Basic.lean

    
                · exact le_refl _

                · exact le_trans hd fib_le_fib_succ

              lemma fib_succ_sub_fib_pred {n : ℕ} (hn : n ≠ 0) :

Collaborator

vihdzp Jul 10, 2025

I think using sub_eq_iff_eq_add' (if imports permit) might give you a slightly shorter proof, since you avoid the add_comm.

Are you sure you need these theorems, though? Natural number subtraction is very different from subtraction on the integers; it's likely not what you want.

Mathlib/Data/Nat/Fib/Basic.lean Outdated

    
                nth_rw 3 [fib_sub_one hn]

                simp [Nat.mul_sub]

                rw [← Nat.sub_add_eq, tsub_add_tsub_comm

                  (Nat.mul_le_mul (le_refl _) (fib_le_fib_of_le (by omega)))

Collaborator

vihdzp Jul 10, 2025

I think you can golf this proof slightly by using mul_left_mono.

Mathlib/Data/Nat/Fib/Basic.lean

    
            @@ -150,6 +164,21 @@ theorem fib_add (m n : ℕ) : fib (m + n + 1) = fib m * fib n + fib (m + 1) * fi
          
                  simp only [fib_add_two, ih]

                  ring

              lemma fib_add_ne_zero {m n : ℕ} (hn : n ≠ 0) :

Collaborator

vihdzp Jul 10, 2025

I don't know if I see the point of having this alongside fib_add.

Contributor Author

themathqueen Jul 10, 2025

I feel it's convenient to have this alongside fib_add


          replace with mono

5f08ce0

Ruben-VandeVelde reviewed

View reviewed changes

Mathlib/Data/Nat/Fib/Basic.lean

    
            @@ -150,6 +159,21 @@ theorem fib_add (m n : ℕ) : fib (m + n + 1) = fib m * fib n + fib (m + 1) * fi
          
                  simp only [fib_add_two, ih]

                  ring

              lemma fib_add_ne_zero {m n : ℕ} (hn : n ≠ 0) :

Collaborator

Ruben-VandeVelde Jul 11, 2025

If this is kept, it should be:

Suggested change

      
            lemma fib_add_ne_zero {m n : ℕ} (hn : n ≠ 0) :
          
            lemma fib_add_of_ne_zero {m n : ℕ} (hn : n ≠ 0) :

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

new-contributor t-data