morita_non https://blog.hatena.ne.jp/morita_non/ memo https://morita-non.hatenadiary.org/ MoreInd.v 帰納法のための明示的な証明オブジェクト を読む。目的の集合を数え上げ尽すことが出来れば、コンストラクタは何でもよい。という意味だと理解。そういうわけで、以前の l=rev l -> pal l も、 list Xのコンストラクタを変えて、新たな帰納法の原理を作れば出来るんじゃね？と考えた。 Definition list_ind2 : forall (X:Type) (P : list X -> Prop), P nil -> (forall (x:X), P [x]) -> (forall (x:X) (l:list X), P l -> P (x::(l++[x])))… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmorita-non.hatenadiary.org%2Fentry%2F20140728%2F1406559714" title="Software Foundations - memo" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2014-07-28 00:01:54 rich https://morita-non.hatenadiary.org/entry/20140728/1406559714 1.0 100%