Joshua Grosso (Aug 26 2021 at 20:28): Joshua Grosso (Aug 26 2021 at 20:28):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?
Christian Doczkal (Aug 27 2021 at 08:43):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: Apr 16 2024 at 23:01 UTC