coqex_2

coqex_2

Coq演習 第2回

coqex_2_6.v

Require Import Arith.

Goal forall x y, x < y -> x + 10 < y + 10.
Proof.
intro.
intro.
apply plus_lt_compat_r.
Qed.

coqex_2_7.v

Goal forall P Q : nat -> Prop, P 0 -> (forall x, P x -> Q x) -> Q 0.
Proof.
intros.
exact (H0 0 H).
Qed.

Goal forall P : nat -> Prop, P 2 -> (exists y, P (1 + y)).
Proof.
intros.
exists 1.
assumption.
Qed.

Goal forall P : nat -> Prop, (forall n m, P n -> P m) -> (exists p, P p) -> forall q, P q.
Proof.
intros.
destruct H0.
exact (H x q H0).
Qed.

coqex_2_8.v

Require Import Arith.

Goal forall m n : nat, (n * 10) + m = (10 * n) + m.
Proof.
intros.
rewrite mult_comm.
reflexivity.
Qed.

coqex_2_9.v

Require Import Arith.

Goal forall n m p q : nat, (n + m) + (p + q) = (n + p) + (m + q).
Proof.
exact plus_permute_2_in_4.
Qed.

Goal forall n m : nat, (n + m) * (n + m) = n * n + m * m + 2 * n * m.
Proof.
intros.
rewrite mult_plus_distr_r.
rewrite mult_plus_distr_l.
rewrite mult_plus_distr_l.
replace (m * n) with (n * m) by apply mult_comm.
replace (n * m + m * m) with (m * m + n * m).
rewrite plus_permute_2_in_4.
replace (n * m) with (n * m * 1).
rewrite <- mult_plus_distr_l.
replace (n * m * (1 + 1)) with (2 * n * m).
reflexivity.
replace (1 + 1) with 2.
rewrite mult_assoc_reverse.
rewrite mult_comm.
reflexivity.
simpl.
reflexivity.
rewrite mult_1_r.
reflexivity.
rewrite plus_comm.
reflexivity.
Qed.