Repository navigation
Conversation
dominic-mulligan-aws
left a comment
dominic-mulligan-aws
left a comment
There was a problem hiding this comment.
Thanks for your contribution! Could you rebase and push again? I've just got some minor comments...
| text\<open>First, we define the mathematical Fibonacci function recursively. | ||
| Solution taken from: https://isabelle.in.tum.de/library/HOL/HOL-Number_Theory/Fib.html \<close> | ||
|
|
||
| fun fib :: "nat \<Rightarrow> nat" where |
There was a problem hiding this comment.
nit: can you use cartouches instead of quotation marks, and match our prevailing style?
|
|
||
| text\<open>Some basic properties of the mathematical definition\<close> | ||
|
|
||
| lemma fib_plus_2: "fib (n + 2) = fib (n + 1) + fib n" |
There was a problem hiding this comment.
nit: can you phrase lemmas using assumes and shows and match our prevailing style?
7edac3f to
d18d99a
Compare
d18d99a to
767c83f
Compare
9653020 to
fc49322
Compare
hanno-becker
left a comment
hanno-becker
left a comment
There was a problem hiding this comment.
Apologies for the late reply, @nagyors. The change looks good. I took the liberty to squash your two commits into one, but could you please add a DCO signoff? Please also consider if you want to add your name to the Copyright header in the newly added file.
Add a Micro Rust function that computes Fibonacci numbers with two mutable `nat` accumulators. Its contract returns `fib (unat n)`, and the loop invariant relates the accumulators to consecutive Fibonacci values. Import the theory from `Micro_Rust_Examples`. Signed-off-by: Örs Nagy <nagyors456@gmail.com>
Add the standard copyright and SPDX header to the new iterative Fibonacci theory. Remove the three trailing spaces reported by `git diff --check`. The definitions and proof are unchanged. Signed-off-by: Hanno Becker <beckphan@amazon.com>
fc49322 to
5c56179
Compare
|
@hanno-becker I signed off my commit, but didn't feel the need to add my name to the copyright header. Thank you for letting me contribute! |
This branch has not been deployed
3 participants
Issue #6 : Implements one of the examples suggested (iterative Fibonacci correctness proof).
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.