satos---jp

## coq_practice_1.v
Theorem tautology : forall P : Prop, P -> P.
Proof.
  intros P H.
  assumption.
Qed.

Theorem Modus_ponens : forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
  intros.
  apply H0.

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

## coq_practice_3_(11~14).v
Require Import Arith.
Require Import Arith Ring.

Fixpoint sum_odd(n:nat) : nat :=
  match n with
  | O => O
  | S m => 1 + m + m + sum_odd m
  end.

Goal forall n, sum_odd n = n * n.

## coq_practice_4_(16~18).v
Definition tautology : forall P : Prop, P -> P
  := fun p => fun p => p.


Definition Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P
  := fun p q (H : ~ q /\ (p -> q)) ( H0 : p) =>
  match H with
  | conj H1 H2 => H1 (H2 H0)
  end.

## coq_practice_19.v
Parameter A : Set.
Definition Eq : A -> A -> Prop :=
  fun p q => p = q.


Lemma Eq_eq : forall x y, Eq x y <-> x = y.
Proof.
  intros.
  unfold Eq.

## coq_practice_21_(1,2).v
(* 必要な公理を入れる *)
Require Import Coq.Logic.Classical.
Lemma ABC_iff_iff :
    forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
Proof.
  intros.
  tauto.
Qed.

(* 必要な公理を入れる *)

## coq_practice_19_kai.v
Parameter A : Set.
Definition Eq : A -> A -> Prop :=
  fun p q => (forall a: A-> Prop, a p <-> a q).


Lemma Eq_eq : forall x y, Eq x y <-> x = y.
Proof.
  intros.
  unfold Eq.
  unfold iff.

## coq_practice_21.v
(* 必要な公理を入れる*)
Require Import Coq.Logic.Classical.
Lemma ABC_iff_iff :
    forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
Proof.
  intros.
  tauto.
Qed.

(* 必要な公理を入れる *)

## coq_practice_26.v
Require Import Arith.
Goal (221 * 293 * 389 * 397 + 17 = 14 * 119 * 127 * 151 * 313)%nat.
Proof.
  ring.
Qed.

## coq_practice_27.v
Require Import ZArith.

Lemma hoge : forall z : Z, (z ^ 4 - 4 * z ^ 2 + 4 > 0)%Z.
Proof.
  intros.
  assert (((z ^ 2 - 2)<>0)%Z -> (((z ^ 2 - 2)^2) > 0) % Z).
    intro.

    assert (forall p : Z, ((p<>0)%Z -> (p ^ 2 > 0) % Z)).
      intro.
	Theorem tautology : forall P : Prop, P -> P.
	Proof.
	intros P H.
	assumption.
	Qed.

	Theorem Modus_ponens : forall P Q : Prop, P -> (P -> Q) -> Q.
	Proof.
	intros.
	apply H0.
	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.
	Require Import Arith.
	Require Import Arith Ring.

	Fixpoint sum_odd(n:nat) : nat :=
	match n with
	\| O => O
	\| S m => 1 + m + m + sum_odd m
	end.

	Goal forall n, sum_odd n = n * n.
	Definition tautology : forall P : Prop, P -> P
	:= fun p => fun p => p.



	Definition Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P
	:= fun p q (H : ~ q /\ (p -> q)) ( H0 : p) =>
	match H with
	\| conj H1 H2 => H1 (H2 H0)
	end.
	Parameter A : Set.
	Definition Eq : A -> A -> Prop :=
	fun p q => p = q.



	Lemma Eq_eq : forall x y, Eq x y <-> x = y.
	Proof.
	intros.
	unfold Eq.
	(* 必要な公理を入れる *)
	Require Import Coq.Logic.Classical.
	Lemma ABC_iff_iff :
	forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
	Proof.
	intros.
	tauto.
	Qed.

	(* 必要な公理を入れる *)
	Parameter A : Set.
	Definition Eq : A -> A -> Prop :=
	fun p q => (forall a: A-> Prop, a p <-> a q).


	Lemma Eq_eq : forall x y, Eq x y <-> x = y.
	Proof.
	intros.
	unfold Eq.
	unfold iff.
	(* 必要な公理を入れる*)
	Require Import Coq.Logic.Classical.
	Lemma ABC_iff_iff :
	forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
	Proof.
	intros.
	tauto.
	Qed.

	(* 必要な公理を入れる *)
	Require Import Arith.
	Goal (221 * 293 * 389 * 397 + 17 = 14 * 119 * 127 * 151 * 313)%nat.
	Proof.
	ring.
	Qed.
	Require Import ZArith.

	Lemma hoge : forall z : Z, (z ^ 4 - 4 * z ^ 2 + 4 > 0)%Z.
	Proof.
	intros.
	assert (((z ^ 2 - 2)<>0)%Z -> (((z ^ 2 - 2)^2) > 0) % Z).
	intro.

	assert (forall p : Z, ((p<>0)%Z -> (p ^ 2 > 0) % Z)).
	intro.