Commit 750ea0bd by MARCHE Claude

example fibonacci updated (no Coq proofs anymore!)

parent 077ae9c6
 ... @@ -301,12 +301,19 @@ module FibonacciLogarithmic ... @@ -301,12 +301,19 @@ module FibonacciLogarithmic = if n = 0 then = if n = 0 then (1, 0) (1, 0) else begin else begin assert { 0 <= div n 2 }; let a, b = logfib (div n 2) in let a, b = logfib (div n 2) in let c = a + b in let c = a + b in if mod n 2 = 0 then if mod n 2 = 0 then (a*a + b*b, b*(a + c)) begin assert { 2 * (div n 2) = (div n 2) + (div n 2) }; (a*a+ b*b, b*(a + c)) end else else begin assert { 2 * (div n 2) + 1 = (div n 2) + (div n 2) + 1 }; (b*(a + c), c*c + b*b) (b*(a + c), c*c + b*b) end end end (* by induction, we easily prove that (* by induction, we easily prove that ... ...
 ... @@ -4,13 +4,12 @@ ... @@ -4,13 +4,12 @@ ... @@ -24,7 +23,7 @@ ... @@ -24,7 +23,7 @@ ... @@ -161,7 +160,7 @@ ... @@ -161,7 +160,7 @@ ... @@ -171,51 +170,42 @@ ... @@ -171,51 +170,42 @@ ... ...
No preview for this file type
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!