lkozima https://blog.hatena.ne.jp/lkozima/ 論理とか計算機とか数学とか https://lkozima.hatenablog.com/ 今度は等式の証明でやってみました。append の結合性。 Coq < Goal forall A (xs ys zs : list A), xs ++ ys ++ zs = (xs ++ ys) ++ zs. 1 subgoal ============================ forall (A : Type) (xs ys zs : list A), xs ++ ys ++ zs = (xs ++ ys) ++ zs induction をするに決まっている。 Unnamed_thm0 < induction xs. 2 subgoals A : Type ===========… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Flkozima.hatenablog.com%2Fentry%2F2012%2F03%2F16%2F002258" title="Ltac と proof term 3 - 論理とか計算機とか数学とか" 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 2012-03-16 00:22:58 rich https://lkozima.hatenablog.com/entry/2012/03/16/002258 1.0 100%