Making Invariants Inductive

inductive.md

Clarification about Chris Done's question:

http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refinement-types-101.lhs/#comment-772831034

Let me split into two questions:

(1) What's the deal with "making the invariant inductive",

(2) If indeed the issue was (1) then why does this other fix* work?

where other fix = adding the extra equations and NOT making the invariant inductive.

Short Answer to Both Questions

The short answer to your question(s) is that the following is not valid,

Forall n:nat, n > 0 => n * (n-1) > n

but the following is valid:

Forall n:int, n > 1 => n * (n-1) > n

Lets use your fact as the simpler example -- the same explanations work for fib.

{-@ fact :: n:{Int | n >= 0} -> {b : Int | b >= n} @-}
fact :: Int -> Int
fact 0 = 1
fact n = n * fact(n - 1)

Question (1)

The above program is desugared/ANF-ed into the following:

fact n = if n == 0
         then 1                          -- VC-i
         else let tmp = fact (n-1) in
              n * tmp                    -- VC-ii

Consequently, to verify it you get two "verification conditions" that must be proved valid by the SMT solver:

(VC-i)   n >= 0  /\ n == 0  /\ b = 1                       => b >= n      

(VC-ii)  n >= 0  /\ n /= 0  /\ tmp >= (n-1) /\ b = n * tmp => b >= n  

VC-i (due to THEN branch says)

IF

• n >= 0 from precondition,
• n == 0 from then branch condition,
• b == 1 returned value is 1,

THEN

• b >= n post-condition holds.

This is easily proved true by the SMT solver.

VC-ii (due to ELSE branch says)

IF

• n >= 0 from precondition,
• n /= 0 from else branch condition,
• tmp >= n-1 from post-condition of call to fact,
• b == n * tmp returned value is n * tmp,

THEN

• b >= n postcondition holds.

Now (VC-ii) is in fact NOT proved by the SMT solver, because it is NOT true, a simple counterexample is n=1, tmp=0. By IH is too weak what I meant is that the "contract" (pre/post-condition) does not reflect the fact that when the input is n=0 the output is actually >= 1.

Note: If you strengthen the post-condition to b >= n && b >= 1 then it works out.

Question (2)

But why then does this other fix work? Well, lets do the same process:

{-@ fact :: n:{Int | n >= 0} -> {b : Int | b >= n} @-}
fact :: Int -> Int
fact 0 = 1
fact 1 = 1
fact n = n * fact(n - 1)

Now, notice that the above program gets de-sugared into:

fact n = if n == 0
         then 1                               -- VC-i
         else if n == 1
              then 1                          -- VC-ii
              else let tmp = fact (n-1) in
                   n * tmp                    -- VC-iii

This in turn, yields three VCs (in the same manner as above), namely:

(VC-i)    n >= 0  /\ n == 0 /\ b = 1                               => b >= n      

(VC-ii)   n >= 0  /\ n /= 0 /\ n == 1 /\ b == 1                    => b >= n  

(VC-iii)  n >= 0  /\ n /= 0 /\ n /= 1 /\ tmp >= n-1 /\ b = n * tmp => b >= n  

Crucially the extra equation you added actually changes the inductive/recursive case, by adding the hypothesis n /= 1. Thus, the (VC-iii) (and of course the first two) are in fact valid and are proven so by the SMT solver. In other words, you can make the VC true by strengthening either the

1. consequences, by adding b>=1 to the post-condition, OR,
2. hypotheses, by adding the base-case that strengthens the pre-condition for the recursive call.

Does that help?