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 Equality of Unusual Array Type? #109

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

The following is failing for reasons unknown:

type intlist is (int|(int[]) this)

assert "index out of bounds (not less than length)":
    forall(intlist[] ys, intlist[] xs):
        if:
            xs == [1, 2, 3]
            ys == xs
        then:
            0 < |ys|

The strange thing is that replacing type intlist is (int|(int[]) this) with type intlist is (int this) and it's fine? The failing proof trace is:

64. exists(intlist[] ys, intlist[] xs).((((xs == [1, 2, 3]) && (ys == xs))  () 
 68. exists(intlist[] ys, intlist[] xs).((xs == [1, 2, 3]) && (xs ==  (Simp 64) 
 67. (xs == [1, 2, 3]) && (xs == ys) && (0 >= |ys|)               (Exists-E 68) 
 52. xs == [1, 2, 3]                                                 (And-E 67) 
 65. xs == ys                                                        (And-E 67) 
 66. 0 >= |ys|                                                       (And-E 67) 
 69. xs is int[]                                                      (Eq-S 52) 
 70. [1, 2, 3] == ys                                               (Eq-S 65,52) 
 71. ys is int[]                                                      (Eq-S 70) 
 72. |ys| >= 0                                                    (ArrLen-I 66) 
 73. |ys| == 0                                                    (Ieq-I 72,66) 
 74. 0 == |ys|                                                        (Simp 73) 
 75. 0 >= 0                                                        (Eq-S 66,74) 
 77. true                                                             (Simp 75)

Whilst the successful trace is:

61. exists(intlist[] ys, intlist[] xs).((((xs == [1, 2, 3]) && (ys == xs))  () 
 65. exists(intlist[] ys, intlist[] xs).((xs == [1, 2, 3]) && (xs ==  (Simp 61) 
 64. (xs == [1, 2, 3]) && (xs == ys) && (0 >= |ys|)               (Exists-E 65) 
 49. xs == [1, 2, 3]                                                 (And-E 64) 
 62. xs == ys                                                        (And-E 64) 
 63. 0 >= |ys|                                                       (And-E 64) 
 66. [1, 2, 3] == ys                                               (Eq-S 62,49) 
 68. ys == [1, 2, 3]                                                  (Simp 66) 
 71. 0 >= |[1, 2, 3]|                                              (Eq-S 63,68) 
 44. false                                                            (Simp 71)

The difference is that this is being inferred in the former trace: 69. xs is int[] (Eq-S 52) ... eh?

UPDATE: this is coming from CongruenceClosure.applyEqualityTypeAxiom() ... but what?