Relating a proof to a Haskell program

Question

I am trying to relate the following integer square root theorem

$\forall x: \mathbb{N}, \exists y : \mathbb{N}((y^2 \leq x) \land (x < (y+1)^2))$

and its proof to its role as a specification of the Integer Square Root isqrt ($\lfloor \sqrt{x} \rfloor$) function in a Haskell program.

Below is a inductive proof of the theorem and the related Haskell program. The proof was done using natural deduction in the Fitch system, hence there are notational differences between code and proof e.g. no $\leq$ in Fitch.

For my question the details of the proof are not important. I wish to focus on the base case, and the two cases involving $\exists$-Elimination and $\lor$-Elimination.

I used Quickcheck as a reasonable check that the theorem holds in the code.

I can see that cases 1 and 2 in the proof correspond to the guard conditions in the Haskell definition of isqrt function. I did not specify, prove, and implement the function isqrt in any structured way. I just used any examples I could find. I believe that there must some more formal transformation from proof to code that I am missing. So despite having written both the proof and code the precise correspondence between both eludes my comprehension.

Is there a technical name for this form of proof to program relation? I would be grateful for an explanation or pointer to the literature.

module Peano where
import Test.QuickCheck

data Nat = Z | S Nat deriving Show
-- addition
(+@) :: Nat -> Nat -> Nat
Z +@ y = y
(S x) +@ y = S (x +@ y)
-- multiplication
(*@) :: Nat -> Nat -> Nat
x *@ Z = Z 
x *@ S y = (x *@ y) +@ x 
-- square
sqr x = x *@ x 
-- equality
(=@) :: Nat -> Nat -> Bool
Z =@ Z  = True
(S m) =@  (S n) = m =@ n 
_=@ _  = False 

-- lesst than
(<@) :: Nat -> Nat -> Bool
Z <@ Z = False 
Z <@ x | not(x =@ Z) = True 
x <@ Z | not(x =@ Z) = False 
(S x) <@ (S y) = x <@ y 


-- less than or equal
(<=@) :: Nat -> Nat -> Bool
x <=@ y = if (x =@ y) || (x <@ y) then True else False


-- Integer square root function
isqrt Z = Z
isqrt (S x) | (sqr (S (isqrt x))) <=@  (S x) = (S (isqrt x))
            | (S x) <@ (sqr (S (isqrt x))) = isqrt x

-- test with Quickcheck
instance Arbitrary Nat where
 arbitrary = oneof [return Z, (S  <$>  arbitrary) ]

isqrtPostCondition :: Nat  -> Bool
isqrtPostCondition x  = (sqr (isqrt x) <=@ x) && (x <@ sqr(S (isqrt x)))
check = quickCheck isqrtPostCondition
-- +++ OK, passed 100 tests.

Answer 1

Your goal is to “prove” --I'm using bullets “•” for syntactic separators-- $$ ∀x \;•\;\; ∃y \;•\;\; y² ≤ x < (y+1)²$$

---

Proof Methods

In the natural deduction style, one proves “∀ x : ℕ • P x” by proving two statements:

Base case      :: P 0
Inductive step :: P a ⇒ P (S a) , for a : ℕ and S successor function

Where, in this case, $$P x \;\;≡\;\; ∃y \;•\; y² ≤ x < (y+1)²$$

In the constructive fashion, one proves “∃ y • Q x” by actually finding such a $y$ using whatever data is available.

Base case

For the [base] case the input x is 0, and we need to find some $y$ with $y² ≤ x < (y+1)²$. Clearly $y = 0$ works as shown in the proof your posted.

Inductive step

For the [inductive] case where the input x is of the shape S a, we need to find a $y$ with $y² ≤ S a < (y+1)²$, (*).

1. However, we have the assumption $P a$ which gives us a $b$ with $b² ≤ a < (b+1)²$ --which looks really close to the goal (*).

2. To reach our goal (*), let's do the simplest thing possible: replace $a$ with $S a$ in (1) thereby obtaining $b² ≤ S a < (b + 1)²$. Because of (1), and the transitivity of ≤, the left part is true and the whole thing reduces to: $$S a < (b + 1)²$$

3. So if this is true, then we are done and the answer is $b$.

4. If it is not true, then we must have it complement: $$(b + 1)² ≤ S a$$

   • But from (1) we also have $a < (b + 1)² = b² + 2b + 1$ thus we obtain $S a = a + 1 < (b² + 2b + 1) + 1 ≤ b² + 4b + 2 = ((b + 1) + 1)²$

   • Hence, we have found that $(b + 1)² ≤ S a < ((b + 1) + 1)²$ and so we may take the output $y$ to be $b + 1$ for our goal (*).

---

Curry-Howard: Proving ≅ Programming

The above was a proof [sketch] which corresponds to the a program.

A proof of $$∀ x : ℕ • ∃ y : ℕ • R(x, y)$$ corresponds to the program

-- Output y = prog x satisfies relationship R(x, y), for all input x.
prog :: Int → Int
prog 0  = “the y found in the base case of the proof”
prog n  = “the y found in the inductive step, 
             along with any conditionals and recursive calls”

Applying this to our above proof yields,

prog :: Int → Int
prog 0 = 0
prog n = let a = n - 1 ; b = prog a
         in
           if   a + 1 <= (b + 1) * (b + 1)
           then b
           else b + 1

Hope that helps :-)