- 集合論に基づいた言語を作りたい
789 ：１[sage]：2015/01/06(火) 00:03:50.53 ID:iQ4UNt/k - Coqで任意の自然数nに対してn*(n+1)が偶数であることを証明しようとしたがどうしてもできない。
だれかHELP.
|
- 集合論に基づいた言語を作りたい
790 ：１[sage]：2015/01/06(火) 00:34:25.70 ID:iQ4UNt/k - 定義はこれで。
Theorem t:
forall (n:nat),exists m , (n*(n+1) = 2 * m).
|
- 集合論に基づいた言語を作りたい
792 ：１[sage]：2015/01/06(火) 21:04:14.92 ID:iQ4UNt/k - 「nが奇数ならn+1は偶数」を証明しようとして詰まってる。
Require Import Even.
Lemma l:
forall (n : nat), odd n -> even (n+1).
intros.
induction n.
simpl.
apply even_S.
これでodd 0とかいうのが出てくるけど、ここからどうしていいかわからない。
|
- 集合論に基づいた言語を作りたい
793 ：１[sage]：2015/01/06(火) 21:10:59.52 ID:iQ4UNt/k - 「自然数nに対してn*(n+1)が偶数である」
本題のこっちはここまで進んだ。
Require Import Even.
Theorem t:
forall (n:nat), even (n*(n+1)).
intros.
apply even_mult_aux.
|
- 集合論に基づいた言語を作りたい
794 ：１[sage]：2015/01/06(火) 23:17:17.43 ID:iQ4UNt/k - Coq難しすぎんよ〜
もう寝る。
|