Proofs and development

[Marko van Eekelen]

Alan Grover wrote to the clean mailing list:
>
>I think that in some cases, mechanical reasoning alone could prove the
>equivalence (certain simple cases). I suspect that the programmer will have
>to supply help in a lot of other cases. In addition, laws and lemmas will
>have to be supplied to support the reasoning.
>
>This all has relation to literate programming, does anyone else have
>interest in that?
>

We certainly have interest in that. At the moment we have a student (Maarten de Mol) who has programmed (in Clean of course) a first prototype of a theorem prover for Clean. It has its own syntax (of course: an extended subset of the Clean syntax); it is not connected to the compiler; it is just for doing experiments trying to figure out what the possibilities are and for what purpose such a tool would be best suited. We are just beginning with this line of research.

Below some initial results are given: some function definitions and properties that have been proven automatically by the system itself (we aim for proving as much as possible automatically: the user can provide help to the system but an average programmer may not consider the corresponding effort worthwhile). The theorems T16,T17 and T18 are important since they involve proving equivalence of accumulating and non-accumulating recursive functions. The theorems T12 and T21 can be considered as non-trivial properties (It took 197 standard proofsteps for the system to prove T21).

I hope this gives you an idea of what is going on in our group concerning automatic reasoning about programs.

Marko van Eekelen.

/* Automatically proven theorems */

T1 [x:Peano] x + 0 = x
T2 [x:Peano, y:Peano] x + (Succ y) = Succ (x + y)
T3 Associative +

T4 [a:SET, x:List a] x ++ [] = x
T5 Associative ++

T6 Symmetric &&
T7 Symmetric ||

T8 Reflexive Listeq
T9 Symmetric Listeq
T10 Transitive Listeq

T11 [a:SET] [x:List a] [y:List a] Length (x ++ y) = (Length x) + (Length y)
T12 [x:List Peano] (Sum x) + (Length x) = Sum (Map Succ x)

T13 [a:SET] [x:List a] [y:List a] Nreverse (x ++ y) = (Nreverse y) ++ (Nreverse x)
T14 [a:SET] [x:List a] Length (Nreverse x) = Length x
T15 [a:SET] [x:List a] Nreverse (Nreverse x) = x

T16 [a:SET] [x:List a] [y:List a] Reverse (x ++ y) = (Reverse y) ++ (Reverse x)
T17 [a:SET] [x:List a] Length (Reverse x) = Length x
T18 [a:SET] [x:List a] Reverse (Reverse x) = x

T19 IsOdd x = IsEven (Succ x)
T20 [x:List Peano] [y:List Peano] LIsOdd (x ++ y) = IsOdd ((Length x) + (Length y))
T21 [x:List Peano] [y:List Peano] LIsOdd (x ++ y) = || (&& (LIsOdd x) (LIsEven y)) (&& (LIsOdd y) (LIsEven x))

---------------------------------------------------------------------
with the following definitions:
---------------------------------------------------------------------

/* Proposition definitions */ 

Reflexive :: (a -> (a -> Bool)) -> Prop
Reflexive x   := [y:a] x y y = True

Symmetric :: (a -> (a -> Bool)) -> Prop
Symmetric x   := [y:a] [z:a] x y z = True -> x z y = True

Transitive :: (a -> (a -> Bool)) -> Prop
Transitive x  := [y:a] [z:a] [p:a] x y z = True -> (x z p = True -> x y p = True)

Equi :: (a -> (a -> Bool)) -> Prop
Equi x        := Reflexive x AND (Symmetric x AND Transitive x)

Associative :: (a -> (a -> a)) -> Prop
Associative x  := [y:a] [z:a] [p:a] x (x y z) p = x y (x z p)

/* Type definitions */ 

:: List a = Nil | Cons a (List a).
:: Peano = Zero | Succ Peano.
:: Bool = True | False.

/* Function definitions */

+ :: INFIX Peano Peano -> Peano
+ 0        x  = x
+ (Succ x) y  = (Succ (x + y))

++ :: INFIX (List a) (List a) -> (List a)
++ []    x  = x
++ [x:y] z  = [x:y ++ z]

&& ::  Bool Bool -> Bool
&& True  x = x
&& False x = (False)

|| ::  Bool Bool -> Bool
|| True  x = True
|| False x = (x)

Listeq :: (List a) (List a) -> Bool
Listeq [] []         = True
Listeq [x:y] []      = False
Listeq [] [x:y]      = False
Listeq [x:y] [z:p]   = (&& (== x z) (== y p))

Length :: (List a) -> Peano
Length []    = 0
Length [x:y] = (Succ (Length y))

Sum :: (List Peano) -> Peano
Sum []     = 0
Sum [x:y]  = (x + (Sum y))

Map :: (a -> b) (List a) -> (List b)
Map x []    = []
Map x [y:z] = [x y:Map x z]

Nreverse :: (List a) -> (List a)
Nreverse []     = []
Nreverse [x:y]  = ((Nreverse y) ++ [x])

Reverse :: (List a) -> (List a)
Reverse x   = (Areverse [] x)

Areverse :: (List a) (List a) -> (List a)
Areverse x []     = x
Areverse x [y:z]  = (Areverse [y:x] z)

IsOdd :: Peano -> Bool
IsOdd 0 = False
IsOdd (Succ x) = (IsEven x)

IsEven :: Peano -> Bool
IsEven 0 = True
IsEven (Succ x) = (IsOdd x)

LIsOdd :: List Peano -> Bool
LIsOdd x = (IsOdd (Length x))

LIsEven :: List Peano -> Bool
LIsEven x = (IsEven (Length x))