1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
-- | An example showing the usage of the What4 backend in copilot-theorem for
-- propositional logic on boolean streams.
module Main where
import qualified Prelude as P
import Control.Monad (void, forM_)
import Language.Copilot
import Copilot.Theorem.What4
spec :: Spec
spec = do
-- * Non-inductive propositions
-- The constant value true, which is translated as the corresponding SMT
-- boolean literal (and is therefore provable).
void $ prop "Example 1" (forAll true)
-- The constant value false, which is translated as the corresponding SMT
-- boolean literal (and is therefore not provable).
void $ prop "Example 2" (forAll false)
-- An "a or not a" proposition which does not require any sort of inductive
-- argument (but see examples 5 and 6 below for versions that do require
-- induction to solve). This is easily proven.
let a = [False] ++ b
b = not a
void $ prop "Example 3" (forAll (a || b))
-- An "a or not a" proposition using external streams, which is also provable.
let a = extern "a" Nothing
void $ prop "Example 4" (forAll (a || not a))
-- * Simple inductive propositions
--
-- While Copilot.Theorem.What4 is not able to solve all inductive propositions
-- in general (see the "Complex inductive propositions" section below), the
-- following inductive propositions are simple enough that the heuristics in
-- Copilot.Theorem.What4 can solve them without issue.
-- An inductively defined flavor of true.
let a = [True] ++ a
void $ prop "Example 5" (forAll a)
-- An inductively defined "a or not a" proposition (i.e., a more complex
-- version of example 3 above).
let a = [False] ++ b
b = [True] ++ a
void $ prop "Example 6" (forAll (a || b))
-- A bit more convoluted version of example 6.
let a = [True, False] ++ b
b = [False] ++ not (drop 1 a)
void $ prop "Example 7" (forAll (a || b))
-- * Complex induction propositions
--
-- The heuristics in Copilot.Theorem.What4 are not able to prove these
-- inductive propositions, so these will be reported as unprovable, even
-- though each proposition is actually provable.
-- An inductively defined flavor of true (i.e., a more complex version of
-- example 5 above).
let a = [True] ++ ([True] ++ ([True] ++ a))
void $ prop "Example 8" (forAll a)
-- An inductively defined "a or not a" proposition (i.e., a more complex
-- version of example 6 above).
let a = [False] ++ ([False] ++ ([False] ++ b))
b = [True] ++ ([True] ++ ([True] ++ a))
void $ prop "Example 9" (forAll (a || b))
main :: IO ()
main = do
spec' <- reify spec
-- Use Z3 to prove the properties.
results <- prove Z3 spec'
-- Print the results.
forM_ results $ \(nm, res) -> do
putStr $ nm <> ": "
case res of
Valid -> putStrLn "valid"
Invalid -> putStrLn "invalid"
Unknown -> putStrLn "unknown"
|
