Many theorems for division rings and fields have stronger versions for discrete fields, where we
assume x / 0 = 0. Before, we used primes to distinguish the versions, but that has the downside
that e.g. for rat and real, all the theorems are equally present. Now, I qualified the weaker ones
with division_ring.foo or field.foo. Maybe that is not ideal, but let's try it.
I also set implicit arguments with the following convention: an argument to a theorem should be
explicit unless it can be inferred from the other arguments and hypotheses.
These changes were needed because e.g. real.add_zero was "x + zero = x", and rewrite
would not match it to a goal "t + 0".
The fix was a lot harder than I expected. At first, migrate failed with resource
errors. In the end, what worked was this: I defined the coercion from num to real
directly (rather than infer num -> nat -> int -> rat -> real).
I still don't understand what the issues are, though. There are subtle issues with
numerals and coercions and migrate.
(We are not alone. Isabelle also suffers from the fact that there are too many
"zero"s and "one"s.)
Daniel is correct when he says the interaction between choice
case-splits, delta case-splits, and coercions can be subtle.
I believe the following condition
https://github.com/leanprover/lean/blob/master/src/frontends/lean/elaborator.cpp#L111
reduces counter-intuitive behavior. Example, the coercion should not
influence the resulting type.
BTW, by removing this condition, many files in the library broke when I
tried to compile from scratch
make clean-olean
make
I used the following workaround. Given a delta-delta constraint
f a =?= f b
If the terms are types, and no case-split will be performed, then
the delta-delta constraint is eagerly solved.
In principle, we don't need the condition that the terms are types.
However, many files break if we remove it. The problem is that many files in the standard
library are abusing the higher-order unification procedure. The
elaboration problems are quite tricky to solve.
I use the extra condition "the terms are types" because usually if they
are, "f" is morally injective, and we don't really want to unfold it.
Note that the following two cases do not work
check '{1, 2, 3}
check insert 1 (insert 2 (insert 3 empty))
Well, they work if we the num namespace is open, and they are
interpreted as having type (finset num)
