It seems to help Dafny with instantiation of quantifiers during proofs if you give the quantified expression a name by encapsulating it in a predicate. If you don’t you can end up in a situation where you prove some quantified property, but are then unable to subsequently assert that quantified property, I think due to Dafny not understanding that the quantification is the same. Naming the property (or more likely, only writing it in one place rather than two places) fixes this. <\/p>\n
For example rather than writing:<\/p>\n
\r\n ...\r\n ensures forall c :: P(a, c) == P(b, c);\r\n ...\r\n assert forall c :: P(a, c) == P(b, c);\r\n<\/pre>\nWrite this:<\/p>\n
\r\n predicate Q(a:S,b:S)\r\n { forall c :: P(a, c) == P(b, c) }\r\n ...\r\n ensures Q(a, b);\r\n ...\r\n assert Q(a, b);\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"It seems to help Dafny with instantiation of quantifiers during proofs if you give the quantified expression a name by encapsulating it in a predicate. If you don’t you can end up in a situation where you prove some quantified … Continue reading