CoqEx6-10.v

Require Import Arith.

(* Q6 *)
Goal forall x y, x < y -> x + 10 < y + 10.
  Proof.
  intros.
  apply plus_lt_compat_r.
  apply H.
  Qed.


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

Goal forall P : nat -> Prop, P 2 -> (exists y, P (1+y)).
  Proof.
  intros.
  exists 1.
  simpl.
  apply H.
  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.
  apply (H x q).
  apply H0.
  Qed.

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

(* Q9 *)
Goal forall n m p q : nat, 
  (n + m) + (p + q) = (n+p) + (m + q).
  Proof.
  intros.
  rewrite plus_assoc.  
  rewrite plus_assoc.
  replace (n + m + p) with (n + p + m).
  reflexivity.
  rewrite <- plus_assoc.
  rewrite <- plus_assoc.
  replace (p + m) with (m + p).
  reflexivity.
  apply plus_comm.
  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.
  rewrite plus_assoc.
  simpl.
  rewrite plus_assoc.
  rewrite plus_0_r.
  rewrite mult_plus_distr_r.
  rewrite plus_assoc.
  rewrite <- plus_assoc.
  replace (m * n + m * m) with (m * m + m * n).
  rewrite plus_assoc.
  replace (n * n + n * m + m * m) with (n * n + m * m + n * m).
  replace (m * n) with (n * m).
  reflexivity.
  apply mult_comm.
  rewrite <- plus_assoc.
  replace (m * m + n * m) with (n * m + m * m).
  rewrite plus_assoc.
  reflexivity.
  rewrite plus_comm.
  reflexivity.
  rewrite plus_comm.
  reflexivity.
  Qed.


(* Q10 *)
Parameter G : Set.
Parameter mult : G -> G -> G.
Notation "x * y" := (mult x y).
Parameter one : G.
Notation "1" := one.
Parameter inv : G -> G.
Notation "/ x" := (inv x).
(* Notation "x / y" := (mult x (inv y)). *) (* 使ってもよい *)

Axiom mult_assoc : forall x y z, x * (y * z) = (x * y) * z.
Axiom one_unit_l : forall x, 1 * x = x.
Axiom inv_l : forall x, /x * x = 1.

Lemma inv_r : forall x, x * / x = 1.
Proof.
intros.
assert (/ / x * 1 = x).
rewrite <- (inv_l x).
rewrite mult_assoc.
rewrite (inv_l (/ x)).
apply one_unit_l.
remember (/ x) as y.
rewrite <- H.
rewrite <- mult_assoc.
rewrite one_unit_l.
rewrite inv_l.
reflexivity.
Qed.

Lemma one_unit_r : forall x, x * 1 = x.
Proof.
intros.
rewrite <- (inv_l x).
rewrite mult_assoc.
rewrite inv_r.
rewrite one_unit_l.
reflexivity.
Qed.