Simplify the optimizer proof
I think the proof of the optimizer could be simplified by replacing the optimize function that lives in the typed world by an inductive relation. This relation would have a constructor for each optimisation step + constructors for being a congruence.
The main lemmas of the optimizer proof would be:
- forall i : typed instruction, there exists an i' of the same type such that (optimizer_rel i i') and optimize (untype i) = untype i'
- forall i i' such that optimizer_rel i i', (eval i) is equivalent to (eval i')
I think it would be simpler because:
- inductive relations that specify each step of the typed optimizer are already used in the proof
- the exact structure of the optimizer does not need to be followed so closely as in the current proof, the relation can be a superset of what is actually used in the untyped world.
The main benefit of simplifying the proof is that it would become easier to add more optim rules afterward.