Coq の manual に、 Coq の (positive) coinductive type は subject reduction を壊す、 と書いてある
Coq reference manual, Coinductive types and corecursive functions, Caveat
subject reduction というのは、たしか、reduction を行っても (計算が進んでも) 型が変わらない、という性質である
具体例は載っていないのだが気になって検索してみると、以下を見つけた
Towards a fix to the loss of subject reduction with corecursion?
あまりよくわかっていないが、ぜんぜん違う型に変わってしまうわけではなく、 等しいことを証明できるけれど、型検査器が見抜けるほどには等しくない (convertible でない)、というようなものに変わるようだ
[latest]