Case Rule Overhaul

New Colors

2 new colors will need to be added to each color scheme: default are yellow and blue.

New Visual Confirmation to Case Rules

Proof by cases has two aspects to verify correctness:

1. Valid cases
2. Exhaustive cases

Thus, there should be some visual indicator for the user that a given case rule application is one of the following:

1. Valid and exhaustive (green)
2. Valid and not exhaustive (blue/yellow)
   1. Valid but not necessary (yellow), which means the branch can be removed without affecting the validity of any other branch.
   2. Valid but not exhaustive (blue). The user will need to add more valid branches to exhaust all possible cases.
3. Invalid (red)

The goal is to make this feedback visible to the user. This would allow users to generate cases more easily.

Implementation Details

Currently, case rules are not required to specify which cell the rule applies to. The first step would be forcing the user to select which cell to apply the case rule to.

For speed, brute force matching checks should be cached somewhere within the case rule object. Because case rules should only apply to a given cell once, a singleton case rule manager can keep track of a given case rule instance for a given cell and return the given case rule. Then, the case rule instance can store the generated cases at that location. Those cases should not need to be regenerated unless the original case rule tree node is removed.

Additionally, boards should cache a bitmask for future comparisons. This would be nice in other instances as well.

Then, for each new transition case rule that uses the same cell, that transition can match to a given index in the array of generated cases and be set to blue if it matches. An internal array should keep track of which cases have been created already. If the case does not match any of the generated cases, then it should be set to red. If the case matches an already matched case, it should be set to yellow. When the final blue case is added, all blue transitions should be updated to green. If any correct case is removed, all green transitions should return to blue. Removing a red or yellow node should not affect any sibling transitions.

Theretically, it would be possible to add a transition in a non-sibling transition that uses the same case rule and cell as some other level or branch of the tree. Of course, the transition should be set to red. This transition should not impact any other transition.