Archive: 2017/8

Understanding Fix_eq in Coq

The problemWhen we try to prove that one general recursion defined in coq is actually correct, in the sense that the fixpoint gives exact the same result if we unfold it once. In words of Coq, it is 1