[Haskell-beginners] Formal proof with haskell

[Daniel Fischer]

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<z)) || ( (x<y) && (y<z) )
>                     where y = (x+z)/2
> 
> It is easy to see that simple substitution lead to
> proof1 x z = (not (x<z)) || (x<z) = True
> 
> 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).