2012-03-14から1日間の記事一覧
今度は算術でやってみました。 Coq < Goal forall n, n = 0 \/ 1 <= n. 1 subgoal ============================ forall n : nat, n = 0 \/ 1 <= n こんなのを証明してみましょう。帰納法に決まってるので帰納法を使います。 Unnamed_thm < induction n. 2 s…
今度は算術でやってみました。 Coq < Goal forall n, n = 0 \/ 1 <= n. 1 subgoal ============================ forall n : nat, n = 0 \/ 1 <= n こんなのを証明してみましょう。帰納法に決まってるので帰納法を使います。 Unnamed_thm < induction n. 2 s…