Software Foundations

Lists.v

自分で問題を考えましょう。
- [cons] （[::]）、 [snoc]、 [append] （[++]） に関する、自明でない定理を考えて書きなさい。

とかいう問題が一番なにしたらいいか分からない。
定理ってどうやって思い付けばいいの？

Lemma nil_rev : forall l : natlist, rev l = -> l = .

rev_injectiveの証明途中に、上とか考えて、証明したけど、まだ出て来てないinversioを使用してる。
inversionがどういう動きをしてるのか、未だに謎だわ。

そして、rev_injectiveは証明出来てない。
以前のメモによると、rev(rev l) = l を使用してた。なるほど。全く覚えてない。