divisibility world #88
Description
My vision for divisibility world can be summarised as: addition is to inequality as multiplication is to divisibility. Just as we define a <= b to be exists c, b = a + c, we can define a | b to be exists c, b = a * c. The tactics introduced in inequality world to deal with introducing and eliminating inequality hypotheses and goals will be usable to deal with divisibility, so probably no new tactics are needed. Perhaps give the user dvd_def : a | b \iff \exists c, b = a * c?
This world should depend on advanced multiplication world, because we need the tactics introduced in <= world and we need a bunch of implication facts about multiplication (just like we <= world needed a bunch of advanced facts about addition).
My vision for some of the levels:
- 1 | n
- n | n
- n | 0
- if a | b and b | c then a | c
- If 0 | n then n = 0
- if a | b and b != 0 then a <= b
- if a | b and b | a then a = b
There are a ton of other basic examples e.g. if a | b then a | bc and ac | bc and a | cb, if a | b and a | c then a | b + c, and the more subtle converse; if a | b and a | b + c then a | c. Also if a | 1 then a = 1 (this is needed to show 1 is preprime). I'm not entirely sure how many of these to put into the world. Perhaps the world should be built with prime number world in mind, where the boss level would be to show that 2 is prime. So in fact perhaps the final design decisions should be made about this world only when the route to the proof that 2 is prime has been clarified. I am reluctant just to flood this world with 20 random facts about divisibility; I would prefer to stick to the rule "at most 10 levels in a world unless we absolutely need a couple more" rather than "stick in as much stuff as you like" because I think that after a while a world can get boring if it's just the same old stuff, whereas new worlds are exciting because they introduce new concepts.
Note that there is some preliminary work done on this world on a very old div-world branch (which contains a bunch of other stuff too, so probably a new branch is required)