Re: [fstar-club] fibonacci_greater_than_arg solution

[Nikhil Swamy via fstar-club]

Hi Michael,

Thanks for your note.

The explanation for that proof isn't quite right---it supposes that Z3 
automatically proves that fibonacci(n) >= 1, which it cannot do, since that 
requires an induction.

Instead, the proof goes something like what's shown below. Thanks to Aseem for 
coming up with this explanation.

I'll update the tutorial accordingly.

Best wishes,
Nik

val fibonacci : nat -> Tot nat
let rec fibonacci n =
  if n <= 1 then 1 else fibonacci (n - 1) + fibonacci (n - 2)

val fibonacci_greater_than_arg : n:nat{n >= 2} -> Lemma (fibonacci n >= n)
// BEGIN: FibonacciGreaterThanArgProof
let rec fibonacci_greater_than_arg n =
  match n with
  | 2 -> ()
  | _ -> fibonacci_greater_than_arg (n-1)

(*
 The proof uses the induction hypothesis:
   forall x, 2 <= x < n ==> fibonacci x >= x

 Z3 proves the base case, when n=2.

 Our remaining goal is to prove that for n >= 3
  fibonacci n >= n or equivalently fibonacci (n-1) + fibonacci (n-2) > n

 From the induction hypothesis we have,
   fibonacci(n - 1) >= n - 1

 To conclude, it suffices to prove that prove that fibonacci(n - 2) >= 1.

 Z3 is able to prove this as follows:

 We have: fibonacci(n - 1) = fib (n - 2) + fib (n - 3) >= n - 1 > 1

 Assume, for contradiction, that fibonacci (n - 2) = 0.
   Then fibonacci (n - 3) > 1. (H)

   If n = 3, then fibonacci(n - 2) = fibonacci(1) = 1. Which is a contradiction.

   If n > 3, then
     0 = //by assumption
     fibonacci (n - 2) = //by definition
     fibonacci (n - 3) + fibonacci (n - 4) >= //since fibonacci(n-4) : nat >= 0
     fibonacci (n - 3) > //by (H), above
     1

   So, we have a contradiction.

 So fibonacci (n - 2) >= 1
*)

// END: FibonacciGreaterThanArgProof



Sent from Outlook<http://aka.ms/weboutlook>

________________________________
From: fstar-club <fstar-club-boun...@lists.gforge.inria.fr> on behalf of 
Michael Delorimier via fstar-club <fstar-club@lists.gforge.inria.fr>
Sent: Monday, January 4, 2021 10:09 PM
To: fstar-club@lists.gforge.inria.fr <fstar-club@lists.gforge.inria.fr>
Subject: [fstar-club] fibonacci_greater_than_arg solution

In the solution to fibonacci_greater_than_arg in the tutorial 
https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Ffstar-lang.org%2Ftutorial&amp;data=04%7C01%7Cnswamy%40microsoft.com%7Ccaf43eaff1694c43ddf108d8b15efe8e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637454369355635374%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&amp;sdata=MtLggjQZM0AeVR%2F60vFSod7oATBbt9rbZpK6DDHDp3c%3D&amp;reserved=0
 it looks like

For fibonacci (n-1) we use the property
   forall x, fibonacci x > 1

should be changed to

For fibonacci (n-2) we use the property
   forall x, fibonacci x > 1

Nice tutorial by the way.
-Michael
_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.gforge.inria.fr%2Fmailman%2Flistinfo%2Ffstar-club&amp;data=04%7C01%7Cnswamy%40microsoft.com%7Ccaf43eaff1694c43ddf108d8b15efe8e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637454369355635374%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&amp;sdata=69Y%2FWoYQkTjMvZfckSnDfu0BdvAgnR0w6Gg0ydPfigw%3D&amp;reserved=0

_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club