2012-03-22から1日間の記事一覧

補足:inversionやinduction

Coq

ちょっと説明してないのもどうかと思ったので。 述語のdestructの話は、計算レベルで制限されている話で、問題になりやすいのはinversionやinductionだと思う(inductionはかなり稀か)。 「ゴールがSetやTypeに属する型であるときに、述語をinversionしたら…

述語のdestruct

Coq

これ見る人いるのかな・・・ 昨日の話と全然連続しないが、昨日のシリーズの続き。 Propに属する帰納型(以下、述語と記述)の展開の話。 Coqのマニュアルだとここの4.5.4のAllowed elimination sortsのあたり。 実際のところ、使用者からして気になる部分は…