From bd9e0bd7095a0942f9b53a09571570e134737c61 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 28 May 2020 07:06:19 +0200 Subject: [PATCH] Simplify examples --- examples/example-2.spec | 31 +++++++++++++++++++++---------- examples/example-exact-cover.spec | 6 +++--- examples/example-prime.spec | 20 +++++++------------- 3 files changed, 31 insertions(+), 26 deletions(-) diff --git a/examples/example-2.spec b/examples/example-2.spec index 389b946..d93f4b9 100644 --- a/examples/example-2.spec +++ b/examples/example-2.spec @@ -2,29 +2,40 @@ input: n -> integer. assume: n >= 0. -# p/1 is an auxiliary predicate, so replace all occurrences of p/1 with its completed definition +# p/1 is an auxiliary predicate output: q/1. +# Multiplication with positive numbers preserves the order of integers axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3). + # Induction principle instantiated for p. # This axiom is necessary because we use Vampire without higher-order reasoning -axiom: (p(0) and forall N (N >= 0 and p(N) -> p(N + 1))) -> (forall N p(N)). +axiom: p(0) and forall N (N >= 0 and p(N) -> p(N + 1)) -> forall N p(N). +# Verify that q computes the floor of the square root of n spec: exists N (forall X (q(X) <-> X = N) and N >= 0 and N * N <= n and (N + 1) * (N + 1) > n). -lemma(forward): forall N N * N >= N. -lemma(forward): forall X (q(X) -> exists N X = N). -lemma(forward): forall X (p(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n)). -lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and not p(N2 + 1))). -lemma(forward): forall N2 (N2 >= 0 and not p(N2 + 1) -> (N2 + 1) * (N2 + 1) > n). +#lemma(forward): forall N N * N >= N. +#lemma(forward): forall X (q(X) -> exists N X = N). +#lemma(forward): forall X (q(X) <-> exists N (X = N and N >= 0 and N * N <= n and not p(N + 1))). +#lemma(forward): exists N (q(N) <-> N >= 0 and N * N <= n and (N + 1) * (N + 1) > n). +#lemma(forward): exists N p(N). +lemma(forward): forall X (p(X) <-> exists N (X = N and N >= 0 and N * N <= n)). +lemma(forward): forall N (N >= 0 and not p(N + 1) -> (N + 1) * (N + 1) > n). lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n)). -lemma(forward): exists N2 (forall X (X = N2 -> (q(X) <-> N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n))). -lemma(forward): exists N2 p(N2). lemma(forward): forall N1, N2 (N1 >= 0 and N2 >= 0 and N1 < N2 -> N1 * N1 < N2 * N2). lemma(forward): forall N (N >= 0 and p(N + 1) -> p(N)). lemma(forward): not p(n + 1). lemma(forward): forall N1, N2 (N2 > N1 and N1 >= 0 and p(N2) -> p(N1)). -lemma(forward): forall N2, N3 (q(N2) and N3 > N2 -> not q(N3)). +lemma(forward): forall N1, N2 (q(N1) and N2 > N1 -> not q(N2)). + +#lemma(backward): forall N (q(N) -> p(N) and not p(N + 1)). +lemma(backward): forall X1 (q(X1) -> p(X1) and exists X2 (exists N (X2 = N + 1 and N = X1) and not p(X2))). + +lemma(backward): forall N (q(N) <- p(N) and not p(N + 1)). + +lemma(backward): forall N (q(N) <- p(N) and not p(N + 1)). +lemma(backward): forall X1 (q(X1) <- p(X1) and exists X2 (exists N (X2 = N + 1 and N = X1) and not p(X2))). diff --git a/examples/example-exact-cover.spec b/examples/example-exact-cover.spec index 73f175c..9cb672e 100644 --- a/examples/example-exact-cover.spec +++ b/examples/example-exact-cover.spec @@ -1,10 +1,10 @@ # Auxiliary predicate to determine whether a variable is integer -axiom: forall X (is_int(X) <-> exists N X = N). +#axiom: forall X (is_int(X) <-> exists N X = N). # Perform the proofs under the assumption that n is a nonnegative integer input constant. n stands # for the total number of input sets input: n -> integer. -assume: n >= 0. +#assume: n >= 0. # s/2 is the input predicate defining the sets for which the program searches for exact covers input: s/2. @@ -15,7 +15,7 @@ output: in/1. # Perform the proofs under the assumption that the second parameter of s/2 (the number of the set) # is always an integer -assume: forall X, Y (s(X, Y) -> is_int(Y)). +#assume: forall X, Y (s(X, Y) -> exists N (Y = N)). # Only valid sets can be included in the solution spec: forall X (in(X) -> X >= 1 and X <= n). diff --git a/examples/example-prime.spec b/examples/example-prime.spec index c02a101..af690c0 100644 --- a/examples/example-prime.spec +++ b/examples/example-prime.spec @@ -1,19 +1,13 @@ input: n -> integer. output: prime/1. +# TODO: not necessary if using the lemma below in both directions assume: n >= 1. -axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3). - -lemma: forall N N + 0 = N. -lemma: forall I, J, N (I * J = N and I > 0 and N > 0 -> J > 0). - -lemma(backward): forall X1 (composite(X1) <- (exists N1, N10 (X1 = N1 and 1 <= N1 and N1 <= n and 2 <= N10 and N10 <= N1 - 1 and exists N11 (N1 = (N10 * N11) and 0 < N11)))). -lemma(backward): forall N (composite(N) -> (exists N10 (1 <= N and N <= n and 2 <= N10 and N10 <= N - 1 and exists N11 (N = (N10 * N11) and 0 < N11)))). - -lemma: forall X1 (composite(X1) <-> (exists N1, N10 (X1 = N1 and 1 <= N1 and N1 <= n and 2 <= N10 and N10 <= N1 - 1 and exists N11 (N1 = (N10 * N11) and 0 < N11)))). - -#spec: forall X (composite(X) -> p__is_integer__(X)). -#spec: forall N (composite(N) <-> N > 1 and N <= n and exists I, J (I > 1 and J > 1 and I * J = N)). -spec: forall X (prime(X) -> p__is_integer__(X)). +spec: forall X (prime(X) -> exists N (X = N)). spec: forall N (prime(N) <-> N > 1 and N <= n and not exists I, J (I > 1 and J > 1 and I * J = N)). + + + + +lemma(backward): forall N (composite(N) <-> N > 1 and N <= n and exists I, J (I > 1 and J > 1 and I * J = N)).