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

Problems with Type Tests #103

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

The following fails for reasons unknown:

type binop is ({expr left, int op} b) where (b.op == 1)

type expr is (int|binop this)

assert:
    forall(binop e1):
        {left: e1, op: 1} is expr

The proof looks like this:

 64. exists(binop e1).(({left: e1, op: 1} is !expr))                         () 
 65. exists(binop e1).({left: e1, op: 1} is !expr)                    (Simp 64) 
 72. binop(e1) && ({left: e1, op: 1} is !expr)                    (Exists-E 65) 
 71. binop(e1)                                                       (And-E 72) 
 61. {left: e1, op: 1} is !expr                                      (And-E 72) 
 81. expr(e1.left) && ((e1.op == 1))                               (Macro-I 71) 
 87. binop({left: e1, op: 1}.left) && !expr({left: e1, op: 1})        (Is-I 61) 
 89. expr(e1.left) && (1 == e1.op)                                    (Simp 81) 
 90. binop(e1) && !expr({left: e1, op: 1})                            (Simp 87) 
 77. expr(e1.left)                                                   (And-E 89) 
 88. 1 == e1.op                                                      (And-E 89) 
 86. !expr({left: e1, op: 1})                                        (And-E 90) 
 93. (e1.left is int) || (e1.left is binop)                        (Macro-I 77) 
 98. ({left: e1, op: 1} is !int) && ({left: e1, op: 1} is !binop)  (Macro-I 86) 
┌──────────────────────────────────────────────────────────────────────────────┐
│ 91. e1.left is int                                                 (Or-E 93) │
│ 149. e1.left is int&!int                                           (Is-I 91) │
│ 54. false                                                         (Is-I 149) │
├──────────────────────────────────────────────────────────────────────────────┤
│ 92. e1.left is binop                                               (Or-E 93) │
│ 95. {left: e1, op: 1} is !int                                     (And-E 98) │
│ 97. {left: e1, op: 1} is !binop                                   (And-E 98) │
│ 151. expr(e1.left) && binop(e1.left)                               (Is-I 92) │
│ 84. binop({left: e1, op: 1}.left)                                  (Is-I 95) │
│ 100. binop({left: e1, op: 1}.left) && !binop({left: e1, op: 1})    (Is-I 97) │
│ 102. {left: e1, op: 1} is !expr&!int                               (Is-I 61) │
│ 150. binop(e1.left)                                              (And-E 151) │
│ 103. binop(e1) && !binop({left: e1, op: 1})                       (Simp 100) │
│ 105. {left: e1, op: 1} is !int&!binop                              (Is-I 95) │
│ 158. expr(e1.left.left) && ((e1.left.op == 1))                 (Macro-I 150) │
│ 99. !binop({left: e1, op: 1})                                    (And-E 103) │
│ 107. {left: e1, op: 1} is !binop&!expr&!int                        (Is-I 97) │
│ 160. expr(e1.left.left) && (1 == e1.left.op)                      (Simp 158) │
│ 112. !expr({left: e1, op: 1}.left) || (({left: e1, op: 1}.op != (Macro-I 99) │
│ 113. (binop({left: e1, op: 1}.left) && !binop({left: e1, op: 1})) (Is-I 107) │
│ 115. {left: e1, op: 1} is !expr&!int&!int&!binop                  (Is-I 102) │
│ 154. expr(e1.left.left)                                          (And-E 160) │
│ 159. 1 == e1.left.op                                             (And-E 160) │
│ 117. !expr(e1) || false                                           (Simp 112) │
│ 118. (binop(e1) && !binop({left: e1, op: 1})) && !expr({left: e1, (Simp 113) │
│ 119. (binop({left: e1, op: 1}.left) && !expr({left: e1, op: 1}))  (Is-I 115) │
│ 121. {left: e1, op: 1} is !int&!binop&!binop&!expr&!int           (Is-I 105) │
│ 163. (e1.left.left is int) || (e1.left.left is binop)          (Macro-I 154) │
│ 125. ((e1 is !int) && (e1 is !binop)) || false                 (Macro-I 117) │
│ 126. (binop(e1) && !expr({left: e1, op: 1})) && !binop({left: e1, (Simp 119) │
│ 128. {left: e1, op: 1} is !binop&!expr&!int&!expr&!int&!binop     (Is-I 107) │
│┌─────────────────────────────────────────────────────────────────────────────┤
││ 161. e1.left.left is int                                         (Or-E 163) │
││┌────────────────────────────────────────────────────────────────────────────┤
│││ 124. (e1 is !int) && (e1 is !binop)                             (Or-E 125) │
│││ 130. {left: e1, op: 1} is !expr&!int&!binop&!binop&!expr&!int   (Is-I 115) │
│││ 122. e1 is !int                                                (And-E 124) │
│││ 123. e1 is !binop                                              (And-E 124) │
│││ 132. binop(e1) && !binop(e1)                                    (Is-I 123) │
│││ 131. !binop(e1)                                                (And-E 132) │
│││ 136. !expr(e1.left) || ((e1.op != 1))                        (Macro-I 131) │
│││ 138. !expr(e1.left) || (1 != e1.op)                             (Simp 136) │
│││ 140. !expr(e1.left) || (1 != 1)                              (Eq-S 138,88) │
│││ 141. !expr(e1.left) || false                                    (Simp 140) │
│││ 145. ((e1.left is !int) && (e1.left is !binop)) || false     (Macro-I 141) │
│││┌───────────────────────────────────────────────────────────────────────────┤
││││ 144. (e1.left is !int) && (e1.left is !binop)                  (Or-E 145) │
││││ 142. e1.left is !int                                          (And-E 144) │
││││ 143. e1.left is !binop                                        (And-E 144) │
││││ 147. expr(e1.left) && !binop(e1.left)                          (Is-I 143) │
││││ 165. e1.left is binop&!int                                      (Is-I 92) │
││││ 146. !binop(e1.left)                                          (And-E 147) │
││││ 166. e1.left is !int&!binop                                    (Is-I 142) │
││││ 170. !expr(e1.left.left) || ((e1.left.op != 1))             (Macro-I 146) │
││││ 172. e1.left is !binop&binop&!int                              (Is-I 143) │
││││ 174. !expr(e1.left.left) || (1 != e1.left.op)                  (Simp 170) │
││││ 175. (expr(e1.left) && !binop(e1.left)) && binop(e1.left)      (Is-I 172) │
││││ 177. e1.left is binop&!int&!int&!binop                         (Is-I 165) │
││││ 178. !expr(e1.left.left) || (1 != 1)                       (Eq-S 174,159) │
││││ 179. (expr(e1.left) && binop(e1.left)) && !binop(e1.left)      (Is-I 177) │
││││ 181. e1.left is !int&!binop&!binop&binop&!int                  (Is-I 166) │
││││ 182. !expr(e1.left.left) || false                              (Simp 178) │
││││ 184. e1.left is !binop&binop&!int&binop&!int&!binop            (Is-I 172) │
││││ 188. ((e1.left.left is !int) && (e1.left.left is !binop)) | (Macro-I 182) │
││││ 190. e1.left is binop&!int&!binop&!binop&binop&!int            (Is-I 177) │
││││┌──────────────────────────────────────────────────────────────────────────┤
│││││ 187. (e1.left.left is !int) && (e1.left.left is !binop)       (Or-E 188) │
│││││ 185. e1.left.left is !int                                    (And-E 187) │
│││││ 186. e1.left.left is !binop                                  (And-E 187) │
││││├──────────────────────────────────────────────────────────────────────────┤
│││││ 54. false                                                     (Or-E 188) │
││││└──────────────────────────────────────────────────────────────────────────┤
│││├───────────────────────────────────────────────────────────────────────────┤
││││ 54. false                                                      (Or-E 145) │
│││└───────────────────────────────────────────────────────────────────────────┤
││├────────────────────────────────────────────────────────────────────────────┤
│││ 54. false                                                       (Or-E 125) │
││└────────────────────────────────────────────────────────────────────────────┤
│├─────────────────────────────────────────────────────────────────────────────┤
││ 162. e1.left.left is binop                                       (Or-E 163) │
│└─────────────────────────────────────────────────────────────────────────────┤
└──────────────────────────────────────────────────────────────────────────────┘
./test2.wyal:5: null
assert:
^^^^^^^^^

That is kind of ridiculous for such a small assertion!

DavePearce commented 7 years ago

This has been resolved by fixing #82. That said, the proof is still:

 64. exists(binop e1).(({left: e1, op: 1} is !expr))                         () 
 65. exists(binop e1).({left: e1, op: 1} is !expr)                    (Simp 64) 
 72. binop(e1) && ({left: e1, op: 1} is !expr)                    (Exists-E 65) 
 71. binop(e1)                                                       (And-E 72) 
 61. {left: e1, op: 1} is !expr                                      (And-E 72) 
 81. expr(e1.left) && ((e1.op == 1))                               (Macro-I 71) 
 87. binop({left: e1, op: 1}.left) && !expr({left: e1, op: 1})        (Is-I 61) 
 89. expr(e1.left) && (1 == e1.op)                                    (Simp 81) 
 90. binop(e1) && !expr({left: e1, op: 1})                            (Simp 87) 
 88. 1 == e1.op                                                      (And-E 89) 
 86. !expr({left: e1, op: 1})                                        (And-E 90) 
 98. ({left: e1, op: 1} is !int) && ({left: e1, op: 1} is !binop)  (Macro-I 86) 
 97. {left: e1, op: 1} is !binop                                     (And-E 98) 
 104. binop({left: e1, op: 1}.left) && !binop({left: e1, op: 1})      (Is-I 97) 
 107. binop(e1) && !binop({left: e1, op: 1})                         (Simp 104) 
 103. !binop({left: e1, op: 1})                                     (And-E 107) 
 116. !expr({left: e1, op: 1}.left) || (({left: e1, op: 1}.op !=  (Macro-I 103) 
 121. !expr(e1) || false                                             (Simp 116) 
 127. ((e1 is !int) && (e1 is !binop)) || false                   (Macro-I 121) 
┌──────────────────────────────────────────────────────────────────────────────┐
│ 126. (e1 is !int) && (e1 is !binop)                               (Or-E 127) │
│ 125. e1 is !binop                                                (And-E 126) │
│ 130. binop(e1) && !binop(e1)                                      (Is-I 125) │
│ 129. !binop(e1)                                                  (And-E 130) │
│ 134. !expr(e1.left) || ((e1.op != 1))                          (Macro-I 129) │
│ 136. !expr(e1.left) || (1 != e1.op)                               (Simp 134) │
│ 138. !expr(e1.left) || (1 != 1)                                (Eq-S 136,88) │
│ 139. !expr(e1.left) || false                                      (Simp 138) │
│ 143. ((e1.left is !int) && (e1.left is !binop)) || false       (Macro-I 139) │
│┌─────────────────────────────────────────────────────────────────────────────┤
││ 142. (e1.left is !int) && (e1.left is !binop)                    (Or-E 143) │
││ 140. e1.left is !int                                            (And-E 142) │
││ 146. e1 is {!int left, ...}                                      (Is-I 140) │
││ 54. false                                                        (Is-I 146) │
│├─────────────────────────────────────────────────────────────────────────────┤
││ 54. false                                                        (Or-E 143) │
│└─────────────────────────────────────────────────────────────────────────────┤
├──────────────────────────────────────────────────────────────────────────────┤
│ 54. false                                                         (Or-E 127) │
└──────────────────────────────────────────────────────────────────────────────┘
DavePearce commented 7 years ago

Right, this is not resolved as the following variation still fails:

type binop is ({expr left, int op} b) where (b.op == 1)

type expr is (int|binop this)

assert:
    forall(expr e1):
        if:
            e1 == {left: 1, op: 1}
        then:
            {left: e1, op: 1} is expr

The proof as it stands is:

82. exists(expr e1).((((e1 == {left: 1, op: 1})) && (({left: e1, op: 1} is  () 
 84. exists(expr e1).((e1 == {left: 1, op: 1}) && ({left: e1, op: 1}  (Simp 82) 
 91. expr(e1) && ((e1 == {left: 1, op: 1}) && ({left: e1, op: 1}  (Exists-E 84) 
 90. expr(e1)                                                        (And-E 91) 
 83. (e1 == {left: 1, op: 1}) && ({left: e1, op: 1} is !expr)        (And-E 91) 
 94. (e1 is int) || (e1 is binop)                                  (Macro-I 90) 
 72. e1 == {left: 1, op: 1}                                          (And-E 83) 
 77. {left: e1, op: 1} is !expr                                      (And-E 83) 
┌──────────────────────────────────────────────────────────────────────────────┐
│ 92. e1 is int                                                      (Or-E 94) │
│ 98. {left: 1, op: 1} is int                                     (Eq-S 92,72) │
│ 68. false                                                          (Is-I 98) │
├──────────────────────────────────────────────────────────────────────────────┤
│ 93. e1 is binop                                                    (Or-E 94) │
│ 97. e1 is {int left, int op}                                       (Eq-S 72) │
│ 100. ({left: 1, op: 1} is int) || ({left: 1, op: 1} is binop)   (Eq-S 94,72) │
│ 106. expr({left: e1, op: 1}.left) && !expr({left: e1, op: 1})      (Is-I 77) │
│ 99. {left: 1, op: 1} is binop                                   (Eq-S 93,72) │
│┌─────────────────────────────────────────────────────────────────────────────┤
││ 98. {left: 1, op: 1} is int                                      (Or-E 100) │
││ 68. false                                                         (Is-I 98) │
│├─────────────────────────────────────────────────────────────────────────────┤
││ 107. expr(e1) && !expr({left: e1, op: 1})                        (Simp 106) │
││ 111. binop({left: 1, op: 1})                                      (Is-I 99) │
││ 105. !expr({left: e1, op: 1})                                   (And-E 107) │
││ 118. expr({left: 1, op: 1}.left) && (({left: 1, op: 1}.op ==  (Macro-I 111) │
││ 123. ({left: e1, op: 1} is !int) && ({left: e1, op: 1} is !bi (Macro-I 105) │
││ 128. expr(1) && true                                             (Simp 118) │
││ 120. {left: e1, op: 1} is !int                                  (And-E 123) │
││ 122. {left: e1, op: 1} is !binop                                (And-E 123) │
││ 125. expr(1)                                                    (And-E 128) │
││ 127. true                                                       (And-E 128) │
││ 103. expr({left: e1, op: 1}.left)                                (Is-I 120) │
││ 130. expr({left: e1, op: 1}.left) && !binop({left: e1, op: 1})   (Is-I 122) │
││ 132. {left: e1, op: 1} is !expr&!int                              (Is-I 77) │
││ 135. (1 is int) || (1 is binop)                               (Macro-I 125) │
││ 136. expr(e1) && !binop({left: e1, op: 1})                       (Simp 130) │
││ 138. {left: e1, op: 1} is !int&!binop                            (Is-I 120) │
││┌────────────────────────────────────────────────────────────────────────────┤
│││ 133. 1 is int                                                   (Or-E 135) │
│││ 129. !binop({left: e1, op: 1})                                 (And-E 136) │
│││ 140. {left: e1, op: 1} is !binop&!expr&!int                     (Is-I 122) │
│││ 145. !expr({left: e1, op: 1}.left) || (({left: e1, op: 1}.op (Macro-I 129) │
│││ 146. (expr({left: e1, op: 1}.left) && !binop({left: e1, op: 1}) (Is-I 140) │
│││ 148. {left: e1, op: 1} is !expr&!int&!binop                     (Is-I 132) │
│││ 150. !expr(e1) || false                                         (Simp 145) │
│││ 151. (expr(e1) && !binop({left: e1, op: 1})) && !expr({left: e1 (Simp 146) │
│││ 152. (expr({left: e1, op: 1}.left) && !expr({left: e1, op: 1})) (Is-I 148) │
│││ 156. ((e1 is !int) && (e1 is !binop)) || false               (Macro-I 150) │
│││ 157. (expr(e1) && !expr({left: e1, op: 1})) && !binop({left: e1 (Simp 152) │
│││┌───────────────────────────────────────────────────────────────────────────┤
││││ 155. (e1 is !int) && (e1 is !binop)                            (Or-E 156) │
││││ 153. e1 is !int                                               (And-E 155) │
││││ 154. e1 is !binop                                             (And-E 155) │
││││ 159. expr(e1) && !binop(e1)                                    (Is-I 154) │
││││ 158. !binop(e1)                                               (And-E 159) │
││││ 166. !expr(e1.left) || ((e1.op != 1))                       (Macro-I 158) │
││││ 168. !expr(e1.left) || (1 != e1.op)                            (Simp 166) │
││││ 172. ((e1.left is !int) && (e1.left is !binop)) || (1 != e1 (Macro-I 168) │
││││┌──────────────────────────────────────────────────────────────────────────┤
│││││ 171. (e1.left is !int) && (e1.left is !binop)                 (Or-E 172) │
│││││ 169. e1.left is !int                                         (And-E 171) │
│││││ 175. e1 is {!int left, ...}                                   (Is-I 169) │
│││││ 68. false                                                     (Is-I 175) │
││││├──────────────────────────────────────────────────────────────────────────┤
│││││ 167. 1 != e1.op                                               (Or-E 172) │
│││││ 183. (e1.op >= (1 + 1)) || (1 >= (e1.op + 1))                (Neq-C 167) │
│││││ 190. (e1.op >= 2) || (0 >= e1.op)                             (Simp 183) │
│││││┌─────────────────────────────────────────────────────────────────────────┤
││││││ 186. e1.op >= 2                                              (Or-E 190) │
│││││├─────────────────────────────────────────────────────────────────────────┤
││││││ 189. 0 >= e1.op                                              (Or-E 190) │
│││││└─────────────────────────────────────────────────────────────────────────┤
││││└──────────────────────────────────────────────────────────────────────────┤
│││├───────────────────────────────────────────────────────────────────────────┤
││││ 68. false                                                      (Or-E 156) │
│││└───────────────────────────────────────────────────────────────────────────┤
││├────────────────────────────────────────────────────────────────────────────┤
│││ 134. 1 is binop                                                 (Or-E 135) │
││└────────────────────────────────────────────────────────────────────────────┤
│└─────────────────────────────────────────────────────────────────────────────┤
└──────────────────────────────────────────────────────────────────────────────┘

How does 167 not give a contradiction with 72?

How does 153 not give a contradiction with 154?

DavePearce commented 7 years ago

UPDATE part of the problem is that e1 == {left: 1, op: 1} is not triggering equality case analysis. One possible reason is that this (currently) requires both lhs and rhs to have record type. But, in this case, e1 has type expr. Presumably, later when it is retyped, the equality case analysis doesn't notice?

DavePearce commented 7 years ago

Resolved by #109