Quoting Tobias Nipkow <nipkow at in.tum.de>: > IIRC, 1 used to abbreviate Suc 0. Making "1 = Suc 0" a simp rule > mimiced that.
Aha! The real reason comes out. Now things are starting to make sense... > It allows you to write 1 on the rhs of an equation > because (if used as a simp rule) the 1 will be replaced by Suc 0. Of > course this does not work on the lhs... Yes, this is a real problem. There are even simp rules in the distribution that will never fire because they have "1::nat" on the lhs. > Even if we did not make "1 = Suc 0" a simp rule, we would still need to > decide how to phrase the library theorems. This would still bias the > user. This remains to be seen; I think the library theorems could probably remain agnostic about 1 vs. Suc 0. Theorems could come in both styles, and each theorem would ensure that the representation is preserved. I might have to try this out, and see how well it works. Actually, I suppose it wouldn't hurt to make sure the library theorems follow this policy, even with "1 = Suc 0" [simp] in place. - Brian
