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)
{-# OPTIONS --safe #-}
module Preloaded where

open import Data.Nat

arith-sum : ℕ
arith-sum zero = zero
arith-sum (suc n) = suc n + arith-sum n

arith-formula : ℕ
arith-formula n = ⌊ n * (n + 1) /2⌋
Require Import Arith.

Fixpoint arith_sum (n : nat) : nat :=
  match n with
  | 0 => 0
  | S m => n + arith_sum m
  end.

Definition arith_formula (n : nat) : nat := Nat.div2 (n * (n + 1)).
def arith_sum :| 0 := 0
| (nat.succ n) := nat.succ n + arith_sum n

def arith_formula (n : ℕ) : ℕ := n * (n + 1) / 2

Your task is to implement the following function:

arithEq : (n : Nat) -> arithFormula n = arithSum n
arithEq n = ?write_a_proof
arith-eq : (n : ℕ) -> arith-formula n ≡ arith-sum n
arith-eq n = ?

Similar Problems

Please check out the following collections for similar problems:

Theorem Proving
Fundamentals

Stats:

CreatedMar 15, 2019
PublishedMar 15, 2019
Warriors Trained743
Total Skips62
Total Code Submissions375
Total Times Completed210
Idris Completions25
Agda Completions60
Coq Completions93
Lean Completions43
Total Stars10
% of votes with a positive feedback rating98% of 44
Total "Very Satisfied" Votes42
Total "Somewhat Satisfied" Votes2
Total "Not Satisfied" Votes0
Total Rank Assessments3
Average Assessed Rank
5 kyu
Highest Assessed Rank
5 kyu
Lowest Assessed Rank
7 kyu
Ad
Contributors
  • monadius Avatar
  • donaldsebleung Avatar
  • kazk Avatar
  • eric-wieser Avatar
Ad