Skip to content

Commit 1afdeb9

Browse files
committed
copilot-theorem: Remove outdated section about proof schemes in README. Refs #452.
The section did not reflect the current state of copilot-theorem anymore. We will make a decision later whether a replacement is necessary, but for now it is simply removed.
1 parent a5340b4 commit 1afdeb9

File tree

1 file changed

+0
-36
lines changed

1 file changed

+0
-36
lines changed

copilot-theorem/README.md

Lines changed: 0 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -98,42 +98,6 @@ and where `bmcMax` corresponds to the `--bmc_max` option of *kind2* and is
9898
equivalent to the `maxK` option of the K-Induction prover. Its default value is
9999
0, which stands for infinity.
100100

101-
### Proof schemes
102-
103-
Let's consider again this example:
104-
105-
```haskell
106-
spec :: Spec
107-
spec = do
108-
void $ prop "gt0" (forAll $ x > 0)
109-
void $ prop "neq0" (forAll $ x /= 0)
110-
where
111-
x = [1] ++ (1 + x)
112-
```
113-
114-
and let's say we want to prove `"neq0"`. Currently, the two available solvers
115-
fail at showing this non-inductive property (we will discuss this limitation
116-
later). Therefore, we can prove the more general inductive lemma `"gt0"` and
117-
deduce our main goal from this. For this, we use the proof scheme
118-
119-
```haskell
120-
assert "gt0" >> check "neq0"
121-
```
122-
instead of just `check "neq0"`. A proof scheme is chain of primitives schemes
123-
glued by the `>>` operator. For now, the available primitives are:
124-
125-
* `check "prop"` checks whether or not a given property is true in the current
126-
context.
127-
* `assume "prop"` adds an assumption in the current context.
128-
* `assert "prop"` is a shortcut for `check "prop" >> assume "prop"`.
129-
* `assuming :: [PropId] -> ProofScheme -> ProofScheme` is such that `assuming
130-
props scheme` assumes the list of properties *props*, executes the proof
131-
scheme *scheme* in this context, and forgets the assumptions.
132-
* `msg "..."` displays a string in the standard output
133-
134-
We will discuss the limitations of this tool and a way to use it in practice
135-
later.
136-
137101
### Some examples
138102

139103
Some examples are in the *examples* folder, including:

0 commit comments

Comments
 (0)