Software Foundation

SF Induction.v #coq

normalizeにて、Prove It. とだけ書いてあるんですが、何を証明すればよいのでしょうか。これ？

取り敢えず、normalizeする前の二進数とした後の二進数で、同じ自然数に変換出来ることは証明したけど、
これって意味あるんだろうか？

そもそもどういう証明が出来たら、プログラムにとって嬉しいんだろうか？一般的に。