2012-03-16から1日間の記事一覧
append の結合性の別証明。f_equal を使ったらどうなるかやってみました。 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 …
今度は等式の証明でやってみました。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…
