昨日 (http://lkozima.hatenablog.com/entry/2013/07/19/225156) よくわからないとか言っていたのが冷静に考えたらできた。なんかこういうのを考えていて， Inductive mov : nat -> nat -> Prop := | mov_1 : forall m, mov (S m) m | mov_2 : forall m, mov…

……が，期待通りに生成されないと思ったけどよく考えてみるとどうなるべきなのかわからなかった話。 準備 例として，石取りゲームみたいなのを考えます。いくつかの石があって，一度に三つまで取ってよいということにしましょう。そうすると，プレイヤーのと…

型健全性というと type preservation と progress が成り立ってればよいというのがよくある話ですが，それでなぜ健全といえるのかというところをわざわざ形式的に書いてみた話です。といっても，わかりやすい説明をしようという気はあまりなくて，知ってる人…