Re: [Haskell-beginners] Formal proof with haskell

On Tuesday 20 September 2011, 14:53:02, Sebastien Lannez wrote:

Dear all,

I am currenlty learning Haskell.

I want to use it to solve combinatorial problems.

I want Haskell to prove a simple logical assertion (a tautology) ... Unfortunately, I failed to express it in Haskell.

The logical proposition: proof1 x z = ( (not (x

It is easy to see that simple substitution lead to proof1 x z = (not (x

Is Haskell smart enough to automatically solve such tautology ?

No. It's not a tautology without some extra assumptions, such as that (<) be a total order compatible with the arithmetic of the domain (and (x+z)/2 exists for all x and z and is different from either x or z). The compiler cannot make such assumptions. Another problem is that isItTrue :: Bool isItTrue = b || not b where b = {- some expression of type Bool -} is not equivalent to True, since b might not terminate. So the most you could get from the latter is (b `seq` True). In the first version of proof1, there are more potential points of nontermination, so the compiler cannot rewrite it to the second version. And, in particular, the two versions of proof1 can give different results without nontermination even with fairly run-of-the-mill datatypes, like Double: Prelude> let x :: Double; x = 0.0 Prelude> let z :: Double; z = 0.5^1074 Prelude> not (x < z) || (x < z) True Prelude> let y = (x+z)/2 in not (x < z) || ((x < y) && (y < z)) False Prelude> So, to rewrite proof1 = not (x < z) || ((x < y) && (y < z)) where y = (x+z)/2 to proof1 = True and be sure you have not changed the meaning of proof1, you need a lot of information not available to the compiler (it may be possible to make that information available to the compiler in languages like Agda or Coq, but I wouldn't bet on it).