Proof/Haskell: Difference between revisions

Line 88:

subst :: IntExpr -> Equals -> Proof IntExpr

{- A convenience function used internally. -}

subst a (a' :== b) ~~= if~~ a == a'

subst a (a' :== b) | a == a' = return b

| otherwise = failf2 "subst: %s not the same as %s" a a'

then return b

~~else~~ failf2 "subst: %s not the same as %s" a a'

{- All the remaining functions are rules of inference, which allow

Line 108:

Line 107:

{- If a = A, b = B, ..., z = Z,

then a + b + ... + z = A + B + ... + Z. -}

equalTerms sum@(Sum l) eqs ~~= do~~

equalTerms sum@(Sum l) eqs

~~unless~~ (length l == length eqs) $

| length l == length eqs = zipWithM subst l eqs >>= return . (sum :==) . Sum

failf2 "equalTerms: %s and %s have different lengths" l eqs

| otherwise = failf2 "equalTerms: %s and %s have different lengths" l eqs

zipWithM subst l eqs >>= return . (sum :==) . Sum

containsFactor :: IntExpr -> IntExpr -> Proof Divides

{- If p == a*b,

then a | p. -}

expr@(Product l) `containsFactor` x ~~= if x `elem` l~~

expr@(Product l) `containsFactor` x

~~then~~ return $ x :| expr

| x `elem` l = return $ x :| expr

~~else~~ failf2 "containsFactor: %s not found in %s" x expr

| otherwise = failf2 "containsFactor: %s not found in %s" x expr

y `containsFactor` _ = failf "containsFactor: %s not a product" y