coq_practice_2.v

Require Import Arith.

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

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.
  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.



Goal forall m n : nat, (n * 10) + m = (10 * n) + m.
Proof.
  intros.
  apply NPeano.Nat.add_cancel_r.
  apply mult_comm.
Qed.

Goal forall n m p q : nat, (n + m) + (p + q) = (n + p) + (m + q).
Proof.
  intros.
  apply NPeano.Nat.add_shuffle1.
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.
  simpl.

  rewrite  plus_assoc_reverse.
  rewrite  plus_assoc_reverse.
  apply NPeano.Nat.add_cancel_l.
  rewrite NPeano.Nat.add_assoc.
  rewrite NPeano.Nat.add_comm.
  apply NPeano.Nat.add_cancel_l.
  rewrite mult_plus_distr_r.
  apply NPeano.Nat.add_cancel_l.
  rewrite plus_0_r.
  apply mult_comm.  
Qed.


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 = 1).
  rewrite <- mult_assoc.
  replace (1 * /x) with (/x).
  rewrite <- inv_l with (/x).
  trivial.
  
  rewrite one_unit_l.
  trivial.

  rewrite <- H.
  rewrite <- inv_l with x.

  replace (x * /x) with (1 * x * /x).
  rewrite <- inv_l with (/x).
  rewrite mult_assoc.
  trivial.
  rewrite <- mult_assoc.
  apply one_unit_l.

Qed.

Lemma one_unit_r : forall x, x * 1 = x.
Proof.
  intros.
  rewrite <- inv_l with x.
  rewrite mult_assoc.
  rewrite inv_r.
  apply one_unit_l.

Qed.