In SSReflect style, is it idiomatic to prove propositions as a `Prop`

or instead a `bool`

? E.g. would `Lemma foo : (n1 == n2) && (n3 == n4)`

be preferred over `Lemma foo : n1 = n2 /\ n3 = n4`

, or vice versa? Does the answer change if `implb`

can be used instead of `->`

, such that the entire statement could be a `bool`

?

I think the answer is, that this depends on the way the lemma is intended to be used. Typical examples are equalities between equalities (e.g., `(n + p == m + p) = (n == m)`

in `ssrnat`

. Your lemma `foo`

should actually be a type (e.g., `(n1 = n2)*(n3 = n4)`

), because then one can use `rewrite foo`

if the goal contains either `n1`

or `n3`

. Generally, `_ ==> _`

is a lot more cumbersome to use than `_ -> _`

so it's mainly used where one cannot have a `Prop`

, e.g. in the predicate for `filter`

or some set expression. I hope this helps.

Last updated: Oct 05 2023 at 02:01 UTC