A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis