search

Whiley / WhileyTheoremProver

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
Apache License 2.0
8 stars 2 forks source link

Problem with Congruence Closure #93

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

The following fails to verify:

define invariant(int[] items, int n) is:
    forall (int i):
        if:
            i < n
        then:
            items[i] == 0

assert:
    forall (int[] items, int n):
        if:
            invariant(items,n)
            items[n] == 0
        then:
            invariant(items,n+1)

The generated proof is:

...
 101. 0 == items[n]                                                 (And-E 102) 
 122. exists(int i).((((((1 + n) + 1) >= ((i + 1) + 1))) && ((ite (Macro-I 105) 
 135. forall(int i).(((((i + 1) >= (n + 1))) || ((items[i] == 0))) (Macro-I 89) 
 139. exists(int i).((n >= i) && (0 != items[i]))                    (Simp 122) 
 143. forall(int i).((i >= n) || (0 == items[i]))                    (Simp 135) 
 138. (n >= i) && (0 != items[i])                                (Exists-E 139) 
 145. (n >= n) || (0 == items[n])                            (Forall-I 143,101) 
 136. n >= i                                                        (And-E 138) 
 137. 0 != items[i]                                                 (And-E 138) 
 148. true || (0 == items[n])                                        (Simp 145) 
 149. i >= 0                                                 (ArrIdx-I 136,137) 
 154. (items[i] >= (0 + 1)) || (0 >= (items[i] + 1))                (Neq-C 137) 
 156. true || (0 == 0)                                           (Eq-S 148,101) 
 157. n >= 0                                                    (Ieq-I 149,136) 
 161. (items[i] >= 1) || (0 >= (1 + items[i]))                       (Simp 154) 
 162. true || true                                                   (Simp 156) 
┌──────────────────────────────────────────────────────────────────────────────┐
│ 158. items[i] >= 1                                                (Or-E 161) │
│┌─────────────────────────────────────────────────────────────────────────────┤
││ 147. true                                                        (Or-E 162) │
││ 165. (i >= n) || (0 == items[i])                         (Forall-I 143,158) │
││┌────────────────────────────────────────────────────────────────────────────┤
│││ 163. i >= n                                                     (Or-E 165) │
│││ 166. n == i                                                (Ieq-I 163,136) │
│││ 167. i == n                                                (Ieq-I 163,136) │
│││ 168. i == i                                                 (Eq-S 167,166) │
││├────────────────────────────────────────────────────────────────────────────┤

Here, we should reach a contradiction from 101 and 158.

DavePearce commented 7 years ago

This is really another instance of #91. In particular renaming variable n to a in the assertion itself and it verifies.