Implication inside an Existential Quantifier: Difference between revisions

With version 1.15 ProB produces a warning if you use an implication inside an existential quantifier. Here we explain why.

Take a look at

  f: 1..3 --> NAT &
  f = [0,0,0] &
  #i.(i:dom(f) => f(i)>0)

You may be surprised to learn that the existential quantifier on the third line is true, even though no element of the array f is greater than 0. Indeed, for i=0 or i=-1 or i=4 the body of the quantifier is true as i:dom(f) is false and hence the implication is true.

Usually, one intended to write a conjunction inside the quantifier, such as the following (which is false for f=[0,0,0]):

  #i.(i:dom(f) & f(i)>0)

Note that in Atelier-B a top-level implication is not allowed inside an existential quantifier; one can only use a conjunction at the top-level. However, this may only displace the problem, as the following predicate is acceptable for Atelier-B but is semantically equivalent to the first existential quantifier above:

#i.(i:INTEGER & (i:dom(f) => f(i)>0))

Note that in particular in Rodin you can accidentally introduce an implication due to its subtly different priorities. Let us look at the next Event-B context (in Camille syntax):

context TestExistImplicationOrder
constants x y
axioms
 @axm1 x=1
 @axm2 y=2
 theorem @thm3_true ∃z·(z∈1‥3 ∧ x=z) ⇒ y=44  // suprinsingly this formula is true; see invariant in Mammar/Laleau landing gear model
 theorem @thm4_false ¬( (∃z2·(z2∈1‥3 ∧ x=z2)) ⇒ y=44  )
end

You may be surprised to see that @thm3_true is actually provable within Rodin. One may expect the predicate to be equivalent to x:1..3 = y=44 which is false. Rodin, however parses the formula as an existential quantifier with the implication inside the body. Hence, z=0 or z=4 are solutions to the existential quantifier and the predicate is true.

When adding additional parentheses, the predicate becomes false and probably corresponds to what we expected to write:

 theorem @thm4_false  (∃z2·(z2∈1‥3 ∧ x=z2)) ⇒ y=44  
end

ProB will now emit a warning for @thm3_true (but not for @thm4_false).