6 kyu
Program Verification #1: The sum of an arithmetic progression
25 of 210monadius
Description:
The goal of this kata is to prove that two functions which compute the sum 0 + 1 + 2 + ... + n
are equivalent.
The following code is preloaded:
module Preloaded
%access public export
%default total
arithSum : Nat -> Nat
arithSum Z = Z
arithSum (S n) = S n + arithSum n
-- We define our own function for dividing a natural
-- number by 2.
-- The existing Idris function divNatNZ
-- is not a good choice because it is impossible (correct
-- me if I my wrong) to prove many useful properties of
-- divNatNZ.
half : Nat -> Nat
half (S (S n)) = S (half n)
half _ = Z
arithFormula : Nat -> Nat
arithFormula n = half $ n * (n + 1)
Your task is to implement the following function:
arithEq : (n : Nat) -> arithFormula n = arithSum n
arithEq n = ?write_a_proof
Similar Problems
Please check out the following collections for similar problems:
Theorem Proving
Fundamentals
Similar Kata:
Stats:
Created | Mar 15, 2019 |
Published | Mar 15, 2019 |
Warriors Trained | 743 |
Total Skips | 62 |
Total Code Submissions | 375 |
Total Times Completed | 210 |
Idris Completions | 25 |
Agda Completions | 60 |
Coq Completions | 93 |
Lean Completions | 43 |
Total Stars | 10 |
% of votes with a positive feedback rating | 98% of 44 |
Total "Very Satisfied" Votes | 42 |
Total "Somewhat Satisfied" Votes | 2 |
Total "Not Satisfied" Votes | 0 |
Total Rank Assessments | 3 |
Average Assessed Rank | 5 kyu |
Highest Assessed Rank | 5 kyu |
Lowest Assessed Rank | 7 kyu |