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

Simplification in RecordEqualityCaseAnalysis #116

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

Currently, RecordEqualityCaseAnalysis could perform more simplification as it is constructing new terms. As an example, consider this:

type Point is ({int x, int y} r)

assert:
    forall(Point p, Point q):
        if:
            p == {x: 1, y: 2}
            q.x == 1
            q.y == 2
        then:
            p == q

This produces the following proof:

 74. exists(Point p, Point q).((((p == {x: 1, y: 2}) && (q.x == 1) && (q.y = () 
 78. exists(Point p, Point q).((p == {x: 1, y: 2}) && (1 == q.x) && ( (Simp 74) 
 77. (p == {x: 1, y: 2}) && (1 == q.x) && (2 == q.y) && (p != q)  (Exists-E 78) 
 62. p == {x: 1, y: 2}                                               (And-E 77) 
 75. 1 == q.x                                                        (And-E 77) 
 76. 2 == q.y                                                        (And-E 77) 
 69. p != q                                                          (And-E 77) 
 79. {x: 1, y: 2} != q                                             (Eq-S 69,62) 
 80. q != {x: 1, y: 2}                                                (Simp 79) 
 85. (q.x != {x: 1, y: 2}.x) || (q.y != {x: 1, y: 2}.y)              (Req-C 80) 
 88. (1 != q.x) || (2 != q.y)                                         (Simp 85) 
 91. (1 != 1) || (2 != 2)                                       (Eq-S 88,75,76) 
 57. false                                                            (Simp 91)

We can see that when Req-C is applied it produces unsimplified expressions of the form {x: 1, y: 2}.x.