Coq演習2014課題

1.v

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

10.v

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.
  rewrite <- (one_unit_l (x * /x)).
  rewrite <- (inv_l (x * /x)).
  rewrite <- mult_assoc.
  apply f_equal.
  rewrite <- mult_assoc.
  apply f_equal.
  rewrite mult_assoc.
  rewrite inv_l.
  apply one_unit_l.
Qed.

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

11.v

Require Import Arith.

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.
Proof.
  intros.
  induction n.
  simpl.
  reflexivity.
  simpl.
  apply f_equal.
  rewrite IHn.
  rewrite (mult_comm n (S n)).
  simpl.
  apply plus_assoc_reverse.
Qed.

12.v

Require Import Lists.List.

Fixpoint sum (xs: list nat) : nat :=
  match xs with
    | nil => 0
    | x :: xs => x + sum xs
  end.

Theorem Pigeon_Hole_Principle :
  forall (xs : list nat), length xs < sum xs -> (exists x, 1<x /\ In x xs).
Proof.
  intros.
  induction xs.
  - exfalso.
    simpl in H.
    apply (Lt.lt_irrefl 0).
    assumption.
  - destruct a.
    + simpl in H.
      simpl.
      assert (exists x: nat, 1<x /\ In x xs).
      { apply IHxs.
        apply Lt.lt_trans with (S (length xs));[apply  Lt.lt_n_Sn | assumption].
      }
      destruct H0.
      exists x.
      destruct H0.
      split.
      * assumption.
      * right.
        assumption.
    + simpl in H.
      apply Lt.lt_S_n in H.
      destruct a.
      *{simpl in H.
        assert (exists x: nat, 1<x /\ In x xs) by apply (IHxs H).
        destruct H0.
        exists x.
        destruct H0.
        split.
        - assumption.
        - simpl.
          right.
          assumption.
       }
      *{exists (S (S a)).
        split.
        - apply Lt.lt_n_S.
          apply Lt.lt_0_Sn.
        - simpl.
          left.
          reflexivity.
       }
Qed.

13.v

Inductive pos : Set :=
 | SO : pos
 | S : pos -> pos.
Fixpoint plus (n m:pos) : pos :=
 match n with
 | SO => S m
 | S p => S (plus p m)
 end.

Infix "+" := plus.

Theorem plus_assoc : forall n m p, n + (m + p) = (n + m) + p.
Proof.
  intros.
  induction n.
  simpl.
  reflexivity.
  simpl.
  rewrite IHn.
  reflexivity.
Qed.

14.v

(*(x 0) + (x 0) <> 1を示すもっとうまい方法ありそう*)

(*ArithをImportした*)
Require Import Arith.

Theorem FF: ~exists f, forall n, f (f n) = S n.
Proof.
  intro.
  destruct H.
  cut (forall n:nat, x n = n + x 0).
  - intro.
    assert (forall n:nat, n + (x 0) + (x 0) = S n).
    { intros.
      repeat rewrite <- H0.
      apply H.
    }
    clear H.
    clear H0.
    assert (~(0 + x 0 + x 0 = S 0)).
    { simpl.
      generalize (x 0).
      intros.
      destruct n.
      - trivial.
      - simpl.
        apply not_eq_S.
        rewrite plus_comm.
        simpl.
        apply not_eq_sym.
        apply O_S.
    }
    apply H.
    apply H1.
  - intro.
    induction n.
    + simpl.
      reflexivity.
    + simpl.
      rewrite <- H.
      rewrite IHn.
      rewrite H.
      reflexivity.
Qed.

15.v

Require Import Lists.List.
Require Import Arith.

Inductive Tree:Set :=
  | Node: list Tree -> Tree.

Fixpoint depth (t:Tree) : nat :=
 match t with
 | Node nil => 0
 | Node lt => 1 + (fix maxdepth (l:list Tree) : nat :=
  match l with
  | nil => 0
  | (t'::l')%list => max (depth t') (maxdepth l')
  end) lt
 end.

Lemma lemma1: forall (t:Tree) (l:list Tree) (n:nat), depth (Node (t::l)%list) <= S n -> depth t <=
 n.
  intros.
  simpl in H.
  apply Le.le_S_n in H.
  apply Max.max_lub_l in H.
  assumption.
Qed.

Lemma lemma2: forall (t:Tree) (l:list Tree), ~(depth (Node (t::l)%list) <= 0).
  intros.
  intro.
  apply Lt.le_not_lt in H.
  apply H.
  simpl.
  apply Lt.lt_0_Sn.
Qed.

Lemma lemma3: forall (A:Set) (l l':list A), (forall (a b: A), In a l \/ In a l' -> In b l \/ In b l' -> {a=b} + {a<>b}) -> {l=l'} + {l <> l'}.
Proof.
  intro.
  induction l.
  - intros.
    destruct l'.
    + left.
      reflexivity.
    + right.
      intro.
      discriminate H0.
  - intros.
    destruct l'.
    + right.
      intro.
      discriminate H0.
    + assert ({a = a0} + {a <> a0}).
      { apply H.
        - left.
          apply in_eq.
        - right.
          apply in_eq.
      }
      destruct H0.
      *{assert ({l = l'} + {l <> l'}).
        { apply IHl.
          intros.
          apply H.
          - simpl.
            destruct H0.
            + left.
              right.
              assumption.
            + right.
              right.
              assumption.
          - simpl.
            destruct H1.
            + left.
              right.
              assumption.
            + right.
              right.
              assumption.
        }
      destruct H0.
      - left.
        rewrite e.
        rewrite e0.
        reflexivity.
      - right.
        rewrite e.
        intro.
        apply n.
        injection H0.
        trivial.
       }
      * right.
        intro.
        apply n.
        injection H0.
        trivial.
Qed.

Lemma lemma4: forall (a:Tree) (l:list Tree) (n:nat), depth (Node (a :: l)%list) <= S n -> depth (Node l) <= S n.
Proof.
  induction l.
  - intros.
    simpl.
    apply Le.le_0_n.
  - intros.
    simpl in H.
    apply Le.le_S_n in H.
    apply Max.max_lub_r in H.
    simpl.
    apply Le.le_n_S.
    assumption.
Qed.

Theorem Tree_dec: forall a b:Tree, {a=b} + {a<>b}.
Proof.
  assert (forall (n:nat) (a b:Tree), depth a <= n -> depth b <= n -> {a=b} + {a<>b}).
  { intro.
    induction n.
    - destruct a.
      destruct l.
      + left.
        destruct b.
        destruct l.
        * reflexivity.
        * intros.
          exfalso.
          apply (lemma2 t l).
          assumption.
      + intros.
        exfalso.
        apply (lemma2 t l).
        assumption.
    - intros.
      destruct a.
      destruct b.
      assert (forall (t:Tree) (l:list Tree), depth (Node l) <= S n -> In t l -> depth t <= n).
      { intros.
        induction l1.
        - exfalso.
          apply (in_nil H2).
        - apply in_inv in H2.
          destruct H2.
          + rewrite <- H2.
            apply lemma1 in H1.
            assumption.
          + apply IHl1.
            * apply (lemma4 a).
              assumption.
            * assumption.
      }
      assert ({l=l0} + {l<>l0}).
      { apply lemma3.
        intros.
        apply IHn.
        - destruct H2.
          + apply H1 with l;[assumption | assumption].
          + apply (H1 a l0 H0 H2).
        - destruct H3.
          apply (H1 b l H H3).
          apply (H1 b l0 H0 H3).
      }
      destruct H2.
      + left.
        f_equal.
        assumption.
      + right.
      intro.
      apply n0.
      injection H2.
      trivial.
  }
  intros.
  apply (H (max (depth a) (depth b))).
  - apply Max.le_max_l.
  - apply Max.le_max_r.
Qed.

16.v

Definition tautology : forall P : Prop, P -> P
  := fun (P:Prop) (H:P) => H.

Definition Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P
  := fun (P Q:Prop) (H: ~Q /\ (P -> Q)) =>
 match H with
 | conj nQ PiQ => fun (x:P) => nQ (PiQ x)
 end.

Definition Disjunctive_syllogism : forall P Q : Prop, (P \/ Q) -> ~P -> Q
  := fun (P Q : Prop) (H0: P \/ Q) (H1: ~P) => 
  match H0 with
  | or_introl HP => False_ind Q (H1 HP)
  | or_intror HQ => HQ
  end.

Definition tautology_on_Set : forall A : Set, A -> A
  := fun (A:Set) (H:A) => H.

Definition Modus_tollens_on_Set : forall A B : Set, (B -> Empty_set) * (A -> B) -> (A -> Empty_set)
  := fun (A B : Set) (BiEpAiB : (B -> Empty_set) * (A -> B)) =>
  match BiEpAiB with
  | (BiE, AiB) => fun (x : A) => (BiE (AiB x))
  end.

Definition Disjunctive_syllogism_on_Set : forall A B : Set, (A + B) -> (A -> Empty_set) -> B
  := fun (A B : Set) (ApB: A+B) (AiE : A -> Empty_set) =>
  match ApB with
  | inl x => Empty_set_rec (fun _ : Empty_set => B) (AiE x)
  | inr y => y
  end.

17.v

Theorem hoge : forall P Q R : Prop, P \/ ~(Q \/ R) -> (P \/ ~Q) /\ (P \/ ~R).
Proof.
  (* 例 : 最初の1行は refine (fun P Q R => _). に置き換えられる *)
  refine (fun P Q R => _).
  refine (fun H => _).
  refine (match H with
    | or_introl HP => _
    | or_intror HnQR => _
    end).
  - refine (conj _ _).
    + refine (or_introl _).
      refine HP.
    + refine (or_introl _).
      refine HP.
  - refine (conj _ _).
    + refine (or_intror _).
      refine (fun HQ => _).
      refine (HnQR _).
      refine (or_introl _).
      refine HQ.
    + refine (or_intror _).
      refine (fun HR => _).
      refine (HnQR _).
      refine (or_intror _).
      refine HR.
Qed.

18.v

Require Import Arith.

Definition Nat : Type :=
  forall A : Type, (A -> A) -> (A -> A).

Definition NatPlus(n m : Nat) : Nat :=
  fun _ f x => n _ f (m _ f x).

Definition nat2Nat : nat -> Nat := nat_iter.

Eval compute in (NatPlus (nat2Nat 2) (nat2Nat 2)).

Definition Nat2nat(n : Nat) : nat := n _ S O.

Lemma NatPlus_plus :
  forall n m, Nat2nat (NatPlus (nat2Nat n) (nat2Nat m)) = n + m.
Proof.
  induction n.
  - induction m.
    + unfold nat2Nat.
      unfold Nat2nat.
      unfold NatPlus.
      simpl.
      reflexivity.
    + simpl (nat2Nat (S m)).
      unfold Nat2nat.
      unfold NatPlus.
      simpl.
      f_equal.
      unfold Nat2nat in IHm.
      unfold NatPlus in IHm.
      simpl in IHm.
      assumption.
  - intros.
    unfold Nat2nat.
    unfold NatPlus.
    simpl.
    f_equal.
    unfold Nat2nat in IHn.
    unfold NatPlus in IHn.
    apply IHn.
Qed.

19.v

Parameter A : Set.

(*Inductive Eq (a:A) : A->Prop := Eq_refl : Eq a a.*)

Definition Eq : A -> A -> Prop := fun (a b:A) => forall (f:A->Prop), f a -> f b.

Check Eq.

Lemma Eq_eq : forall x y, Eq x y <-> x = y.
Proof.
  intros.
  split.
  - intros.
    apply H.
    reflexivity.
  - unfold Eq.
    intros.
    rewrite <- H.
    assumption.
Qed.

2.v

Theorem Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P.
Proof.
  intros.
  destruct H.
  intro.
  apply H.
  apply H0.
  exact H1.
Qed.

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

21_2.v

Goal
  forall P Q R : Prop,
  (IF P then Q else R) ->
  exists b : bool,
  (if b then Q else R).
Proof.
  intros.
  case H.
  - intro hPaQ.
    destruct hPaQ as [hP hQ].
    exists true.
    assumption.
  - intro hnPaR.
    destruct hnPaR as [hnP hR].
    exists false.
    assumption.
Qed.

21_3.v

Require Import Coq.Logic.ClassicalDescription.

Goal
  forall P Q R : nat -> Prop,
  (forall n, IF P n then Q n else R n) ->
  exists f : nat -> bool,
  (forall n, if f n then Q n else R n).
Proof.
  intros.
  assert (exists f: nat->bool, forall n:nat, if f n then P n else ~ (P n)).
  { apply (unique_choice (fun n (b:bool) => if b then P n else ~(P n))).
    intros.
    assert ({P x}+{~(P x)}) by apply excluded_middle_informative.
    case H0.
    - intro Px.
      exists true.
      unfold unique.
      split.
      + assumption.
      + intros.
        destruct x';[reflexivity|contradiction].
    - exists false.
      unfold unique.
      split.
      + assumption.
      + destruct x';[contradiction|reflexivity].
  }
  destruct H0 as [f].
  exists f.
  intro.
  specialize (H0 n).
  specialize (H n).
  destruct (f n);destruct H;tauto.
(*  destruct (f n).
  - destruct H;[tauto|tauto].
  - destruct H;[tauto|tauto].*)
Qed.

22.v

Require Import Coq.Logic.ClassicalDescription.
Require Import Coq.Logic.FunctionalExtensionality.

Record isomorphism{A B : Type} (f : A -> B) : Prop := {
  inverse : B -> A;
  is_retraction b : f (inverse b) = b;
  is_section a : inverse (f a) = a
}.

Notation isomorphic A B :=
  (exists f, @isomorphism A B f).

Lemma neg_unique :
  forall A,
    { isomorphic (A -> Empty_set) Empty_set } +
    { isomorphic (A -> Empty_set) unit }.
Proof.
  intros.
  specialize (excluded_middle_informative (isomorphic A Empty_set)).
  intros.
  destruct H as [H|H].
  - right.
    destruct H.
    destruct H.
    exists (fun _ => tt).
    exists (fun _ => x).
    + intros.
      case b.
      reflexivity.
    + intros.
      apply functional_extensionality.
      intros.
      case (x x0).
  - left.
    assert (f: Empty_set->A).
    { intros.
      case H0.
    }
    assert (g: (A->Empty_set)->Empty_set).
    { intros.
      exfalso.
      apply H.
      exists X.
      exists f.
      - intro.
        case b.
      - intro.
        case (X a).
    }
    exists g.
    exists (fun e => (fun _ => e)).
    + intros.
      case b.
    + intros.
      apply functional_extensionality.
      intros.
      case (a x).
Qed.

23.v

Definition compose {A B C} (f : A -> B) (g : B -> C) :=
  fun x => g (f x).

Parameter X Y : Type.
Parameter f : X -> Y.

Axiom epi : forall Z (g h : Y -> Z), compose f g = compose f h -> g = h.

Require Import Coq.Logic.Classical.
Require Import Coq.Logic.ClassicalDescription.
Require Import Coq.Logic.FunctionalExtensionality.

Lemma surj : forall y, exists x, f x = y.
Proof.
  assert ((exists y:Y, forall x:X, f x <> y) -> ~(forall Z (g h : Y->Z), (compose f g = compose f h -> g = h))).
  { intro.
    apply ex_not_not_all.
    exists bool.
    destruct H.
    apply ex_not_not_all.
    exists (fun y => true).
    apply ex_not_not_all.
    assert (exists f: Y->bool, forall y:Y, IF y = x then f y = false else f y = true).
    { apply (unique_choice (fun a b => IF a = x then b = false else b = true)).
      intro.
      assert ({x0 = x} + {x0 <> x}) by apply excluded_middle_informative.
      case H0.
      - intros.
        exists false.
        unfold unique.
        split.
        + left.
          split;[assumption|reflexivity].
        + intros.
          destruct H1.
          * destruct H1.
            auto.
          * tauto.
      - clear H0.
        intros.
        exists true.
        unfold unique.
        split.
        + right.
          auto.
        + intros.
          destruct H0.
          * tauto.
          * destruct H0.
            auto.
    }
    destruct H0 as [f].
    exists f.
    intro.
    absurd ((fun _ : Y => true) = f).
    - intro.
      absurd (forall x, (fun _ : Y => true) x = f x).
      + apply ex_not_not_all.
        exists x.
        replace (f x) with false.
        * congruence.
        *{destruct (H0 x).
          - destruct H3.
            auto.
          - tauto.
          }
      + apply equal_f.
        assumption.
    - apply H1.
      unfold compose.
      apply functional_extensionality.
      intros.
      destruct (H0 (Top.f x0)).
      + exfalso.
        destruct H2.
        apply (H x0).
        apply H2.
      + destruct H2.
        auto.
  }
  apply NNPP.
  intro.
  apply not_all_ex_not in H0.
  destruct H0.
  apply H.
  - exists x.
    intro.
    intro.
    apply H0.
    exists x0.
    assumption.
  - intros.
    apply epi.
    assumption.
Qed.

Require Import Coq.Logic.IndefiniteDescription.

Lemma split_epi : exists g, compose g f = id.
Proof.
  assert (exists g: Y->X, forall y: Y, f (g y) = y).
  { apply (functional_choice (fun y x => f x = y)).
    apply surj.
  }
  destruct H as [g].
  exists g.
  apply functional_extensionality.
  unfold compose, id.
  assumption.
Qed.

26.v

Require Import Arith Ring.

Goal (221 * 293 * 389 * 397 + 17 = 14 * 119 * 127 * 151 * 313)%nat.
Proof.
  ring.
Qed.

27.v

Require Import ZArith.

Lemma hoge : forall z : Z, (z ^ 4 - 4 * z ^ 2 + 4 > 0)%Z.
Proof.
  assert (forall z:Z, z > 0 -> z^2 > 0)%Z.
  {
    intros.
    replace (z^2)%Z with (z*z)%Z by ring.
    apply Zmult_gt_0_compat;assumption.
  }
  intros.
  destruct (Z_dec (z^2 - 2) 0).
  - destruct s.
    + assert (- (z^2 - 2) > 0)%Z by omega.
      replace (z^4 - 4 * z^2 + 4)%Z with ((-(z^2 - 2))^2)%Z by ring.
      apply H.
      assumption.
    + replace (z^4 - 4 * z^2 + 4)%Z with ((z^2 - 2)^2)%Z by ring.
      apply H.
      assumption.
  - exfalso.
    assert ((2 <= z \/ z <= -2) \/ z = -1 \/ z = 0 \/ z = 1)%Z by omega.
    destruct H0.
    + assert (z ^ 2 = 2)%Z by omega.
      assert (4 <= z^2)%Z.
      {
        replace 4%Z with (2*2)%Z by omega.
        destruct H0.
        - replace (z^2)%Z with (z*z)%Z by ring.
          apply Zmult_le_compat;omega.
        - replace (z^2)%Z with (-z*-z)%Z by ring.
          apply Zmult_le_compat;omega.
      }
      assert (4 <= 2)%Z.
      {
        rewrite <- H1.
        assumption.
      }
      assert (~(4<=2))%Z by omega.
      apply H4.
      apply H3.
    + assert (z^2 <> 2)%Z.
      {
        destruct H0.
        - rewrite H0.
          replace ((-1)^2)%Z with 1%Z by ring.
          omega.
        - destruct H0;rewrite H0.
          + replace (0^2)%Z with 0%Z by ring.
            omega.
          + replace (1^2)%Z with 1%Z by ring.
            omega.
      }
    apply H1.
    omega.
Qed.

28.v

Require Import Reals.
Require Import Fourier.

Theorem PI_RGT_3_05 : (PI > 3 + 5/100)%R.
Proof.
  specialize (Alt_PI_ineq 5).
  intro.
  destruct H.
  clear H0.
  assert (3 + 5 / 100 < 4 * sum_f_R0 (tg_alt PI_tg) (S (2 * 5)))%R.
  {
    unfold sum_f_R0.
    unfold tg_alt.
    unfold PI_tg.
    simpl.
    field_simplify.
    assert (0 < 967171378320 / 316234143225 - 305 / 100)%R.
    {
      field_simplify.
      replace (0/1)%R with 0%R by field.
      apply Rlt_mult_inv_pos;prove_sup.
    }
    replace (305 / 100)%R with (0 + 305 / 100)%R by field.
    replace (967171378320 / 316234143225)%R with ((967171378320 / 316234143225 - 305 / 100) + (305 / 100))%R by field.
    apply Rplus_lt_compat_r.
    assumption.
  }
  apply Rge_gt_trans with (4 * sum_f_R0 (tg_alt PI_tg) (S (2 * 5)))%R.
  - rewrite Alt_PI_eq in H.
    fourier.
  - fourier.
Qed.

29.v

Require Import ZArith.
Require Import Coq.ZArith.Znumtheory.

Definition prime1(z : Z) : Prop :=
  z <> 0%Z /\
  forall a b, ((z | a * b) -> (z | a) \/ (z | b))%Z.

Definition prime2(z : Z) : Prop :=
  forall a b, (z = a * b -> (a | 1) \/ (b | 1))%Z.

Lemma lemma1: forall n: Z, (Z.abs n = 0 -> n = 0)%Z.
Proof.
  intros.
  specialize (Zabs_dec n).
  intro.
  destruct H0;omega.
Qed.

(*Zmult_oneとかZdivide_1を使えば良かった*)
Lemma lemma2 : forall n m:Z, (1 = n * m -> Z.abs m = 1)%Z.
Proof.
  intros.
  specialize (Zabs_pos m).
  intros.
  assert (Z.abs m = 0 \/ Z.abs m = 1 \/ Z.abs m > 1)%Z by omega.
  clear H0.
  destruct H1.
  - apply lemma1 in H0.
    subst m.
    replace (n * 0)%Z with 0%Z in H by ring.
    congruence.
  - destruct H0.
    + assumption.
    + exfalso.
      assert (1 = Z.abs n * Z.abs m)%Z.
      {
        replace 1%Z with (Z.abs 1)%Z by auto.
        rewrite <- Zabs_Zmult.
        f_equal.
        assumption.
      }
      specialize (Zabs_pos n).
      intros.
      assert (Z.abs n = 0 \/ Z.abs n >= 1)%Z by omega.
      clear H2.
      destruct H3.
      * apply lemma1 in H2.
        subst n.
        simpl in H.
        congruence.
      * assert (Z.abs n * Z.abs m >= Z.abs n * 2)%Z by (apply Zmult_ge_compat_l;omega).
        assert (Z.abs n * 2 >= 1 * 2)%Z by (apply Zmult_ge_compat_r;omega).
        assert (Z.abs n * Z.abs m >= 2)%Z by omega.
        rewrite <- H1 in H5.
        absurd (1 >= 2)%Z.
        omega.
        assumption.
Qed.

Lemma prime1_prime2_iff z : prime1 z <-> prime2 z.
Proof.
  split.
  - unfold prime1.
    unfold prime2.
    intros.
    destruct H.
    specialize (H1 a b).
    subst.
    assert (a * b | a * b)%Z.
    {
      exists 1%Z.
      ring.
    }
    specialize (H1 H0).
    clear H0.
    destruct H1.
    + right.
      destruct H0.
      exists x.
      replace (x * (a * b))%Z with (a * (x * b))%Z in H0 by ring.
      assert (a = a * 1)%Z by ring.
      rewrite H1 in H0 at 1.
      clear H1.
      apply Z.mul_reg_l with a.
      * intro.
        subst.
        apply H.
        ring.
      * assumption.
    + left.
      destruct H0.
      exists x.
      replace (x * (a * b))%Z with (b * (x * a))%Z in H0 by ring.
      assert (b = b * 1)%Z by ring.
      rewrite H1 in H0 at 1.
      clear H1.
      apply Z.mul_reg_l with b.
      * intro.
        subst.
        apply H.
        ring.
      * assumption.
  - unfold prime1.
    unfold prime2.
    intros.
    assert (z_ne_0: (z<>0)%Z).
    {
      intro.
      subst.
      specialize (H 0 0)%Z.
      assert (0%Z = (0 * 0)%Z) by omega.
      specialize (H H0).
      clear H0.
      assert (~(0 | 1))%Z.
      intro.
      destruct H0.
      replace (x*0)%Z with 0%Z in H0 by ring.
      congruence.
      apply H0.
      tauto.
    }
    split.
    + assumption.
    + intros.
      assert (Z.gcd a z = 1 \/ Z.gcd a z = Z.abs z)%Z.
      {
        destruct H0.
        specialize (Z.gcd_divide_r a z)%Z.
        intro.
        destruct H1.
        specialize (H x0 (Z.gcd a z) H1).
        destruct H;destruct H.
        - right.
          apply lemma2 in H.
          rewrite H1 at 2.
          rewrite Zabs_Zmult.
          rewrite H.
          specialize (Z.gcd_nonneg a z).
          intros.
          apply Zabs_eq in H2.
          rewrite H2.
          ring.
        - left.
          apply lemma2 in H.
          specialize (Z.gcd_nonneg a z).
          intros.
          apply Zabs_eq in H2.
          omega.
      }
      destruct H0.
      specialize (Z.gcd_divide_r a z)%Z.
      intros.
      destruct H2.
      destruct H1.
      *{right.
        specialize (Zgcd_is_gcd a z).
        intro.
        rewrite H1 in H3.
        apply Gauss with a.
        - exists x.
          assumption.
        - unfold rel_prime.
          apply Zis_gcd_sym.
          assumption.
       }
      *{left.
        specialize (H x0 (Z.gcd a z) H2).
        destruct H.
        - destruct H.
          specialize (Z.gcd_divide_l a z)%Z.
          intro.
          destruct H3.
          exists (x2 * Z.sgn z)%Z.
          rewrite H3.
          rewrite H1.
          rewrite <- Zsgn_Zabs.
          ring.
        - rewrite H1 in H.
          destruct H.
          apply lemma2 in H.
          specialize (Zabs_pos z).
          intro.
          apply Zabs_eq in H3.
          rewrite H3 in H.
          specialize (Zabs_dec z).
          rewrite H.
          clear H H3.
          intro.
          destruct H;subst z.
          + exists a.
            ring.
          + exists (-a)%Z.
            ring.
       }
Qed.

3.v

Theorem Disjunctive_syllogism : forall P Q : Prop, (P \/ Q) -> ~P -> Q.
Proof.
 intros.
 destruct H.
 exfalso.
 apply H0.
 apply H.
 exact H.
Qed.

30.v

Require Import QArith.
Require Import ZArith.
Require Import Coq.ZArith.Znumtheory.

Lemma sqrt_2 : forall q : Q, ~(q * q == 1 + 1)%Q.
Proof.
  intros.
  intro.
  unfold Qeq in H.
  replace (Qden (1 + 1)%Q) with 1%positive in H by (simpl;reflexivity).
  replace (Qnum (1 + 1)%Q) with 2%Z in H by (simpl;reflexivity).
  unfold Qmult in H.
  simpl in H.
  ring_simplify in H.
  replace (' (Qden q * Qden q)~0) with (2 * (' Qden q) * (' Qden q))%Z in H by (simpl;reflexivity).
  specialize (Zgcd_is_gcd (Qnum q) (Zpos (Qden q)))%Z.
  intro.
  set (n := Qnum q) in H.
  set (d := ' Qden q) in H.
  set (g := (Z.gcd (Qnum q) (' Qden q))%Z) in H0.
  assert (g > 0).
  {
    specialize (Z.gcd_nonneg (Qnum q) (' Qden q)).
    intro.
    assert (g = 0 \/ g > 0).
    {
      subst g.
      omega.
    }
    destruct H2.
    - subst g.
      specialize (Z.gcd_divide_r (Qnum q) (' Qden q))%Z.
      intro.
      destruct H3.
      rewrite H2 in H3.
      ring_simplify in H3.
      congruence.
    - assumption.
  }
  specialize (Z.gcd_divide_r (Qnum q) (' Qden q))%Z.
  specialize (Z.gcd_divide_l (Qnum q) (' Qden q))%Z.
  intros.
  assert ((n / g) * (n / g) = 2 * (d / g) * (d / g))%Z.
  {
    rewrite <- Zdivide_Zdiv_eq_2;[|omega|subst d n g;assumption].
    rewrite <- Zdivide_Zdiv_eq_2;[|omega|subst d n g;assumption].
    rewrite <- Zdivide_Zdiv_eq_2;[|omega|subst d n g;assumption].
    replace (n / g * n)%Z with (n * (n / g))%Z by ring.
    rewrite <- Zdivide_Zdiv_eq_2;[|omega|subst d n g;assumption].
    replace (2 * d / g * d)%Z with (d * (2 * d / g))%Z by ring.
    rewrite <- Zdivide_Zdiv_eq_2;[|omega|].
    replace (n * n)%Z with (n ^ 2)%Z by ring.
    rewrite H.
    replace (d * (2 * d))%Z with (2 * d * d)%Z by ring.
    reflexivity.
    destruct H3.
    exists (2 * x)%Z.
    subst d.
    subst g.
    rewrite H3 at 1.
    ring.
  }
  assert (prime 2)%Z.
  {
    apply prime_intro.
    omega.
    intros.
    replace (n0)%Z with 1%Z by omega.
    unfold rel_prime.
    apply Zis_gcd_intro.
    - exists 1;ring.
    - exists 2;ring.
    - intros.
      assumption.
  }
  assert ((2 | (n / g)) \/ (2 | (n / g)))%Z.
  {
    apply prime_mult.
    - assumption.
    - exists ((d / g) * (d / g))%Z.
      rewrite H4.
      ring.
  }
  assert ((2 | n / g))%Z by (destruct H6;assumption).
  clear H6.
  destruct H7.
  rewrite H6 in H4.
  ring_simplify in H4.
  assert (2 * x ^ 2 = (d / g) ^ 2)%Z by omega.
  clear H4.
  assert ((2 | (d / g)) \/ (2 | (d / g)))%Z.
  {
    apply prime_mult.
    - assumption.
    - exists (x^2)%Z.
      ring_simplify.
      omega.
  }
  assert ((2 | (d / g))%Z) by (destruct H4;assumption).
  clear H4.
  assert (rel_prime (n/g) (d/g))%Z.
  {
    apply Zis_gcd_rel_prime.
    - subst d.
      apply Zgt_pos_0.
    - specialize (Z.gcd_nonneg n d).
      subst d n g.
      omega.
    - subst d n g.
      assumption.
  }
  clear H7 H5 H3 H2 H1 H0 H.
  unfold rel_prime in H4.
  destruct H4.
  clear H H0.
  specialize (H1 2)%Z.
  assert (~(2 | 1))%Z.
  {
    unfold Zdivide.
    intro.
    destruct H.
    assert (forall x:Z, 1 <> x * 2)%Z.
    {
      intro.
      omega.
    }
    specialize (H0 x0).
    apply H0.
    assumption.
  }
  apply H.
  apply H1.
  - exists x.
    omega.
  - assumption.
Qed.

31.v

(* Section の練習 *)

Section Poslist.
  (* このセクションの中では、Aが共通の変数として使える。 *)
  Variable A : Type.
  (* 非空なリスト *)
  Inductive poslist : Type :=
    a : A -> poslist
   |cons : A -> poslist -> poslist.

  Section Fold.
    (* 二項演算 *)
    Variable g : A -> A -> A.

   (* gによって畳み込む。
    * 次のどちらかを定義すること。どちらでもよい。
    * 左畳み込み : リスト [a; b; c] に対して (a * b) * c を計算する。
    * 右畳み込み : リスト [a; b; c] に対して a * (b * c) を計算する。
    *)
    Fixpoint fold (l:poslist) : A :=
      match l with
        a x => x
       |cons x l' => g x (fold l')
      end.
    (* DefinitionをFixpointなどに置き換えてもよい。 *)
  End Fold.
End Poslist.
(* Poslistから抜けたことにより、poslistは変数Aについて量化された形になる。 *)

(* このリストに関するmap関数 *)
Section PoslistMap.
  Variable A B : Type.
  Variable f : A -> B.

  Definition map : poslist A -> poslist B :=
    (fix map' (l:poslist A) : poslist B := match l with
     a x => a _ (f x)
    |cons x l' => cons _ (f x) (map' l')
    end).
End PoslistMap.

(* 今回は証明すべきことはないので、定義を正確に *)

32.v

Require Import Arith.

Module Type SemiGroup.
  Parameter G : Type.
  Parameter mult : G -> G -> G.
  Axiom mult_assoc :
    forall x y z : G, mult x (mult y z) = mult (mult x y) z.
End SemiGroup.

Module NatMult_SemiGroup <: SemiGroup.
  Definition G := nat.
  Definition mult := mult.
  Definition mult_assoc := mult_assoc.
End NatMult_SemiGroup.

Module NatMax_SemiGroup <: SemiGroup.
  Definition G := nat.
  Definition mult := max.
  Definition mult_assoc := Max.max_assoc.
End NatMax_SemiGroup.

Module SemiGroup_Product (G0 G1:SemiGroup) <: SemiGroup.
  Definition G := (G0.G * G1.G)%type.
  Definition mult := fun (x y:G) =>
  match x with (x0, x1) =>
    match y with (y0, y1) =>
      (G0.mult x0 y0, G1.mult x1 y1)
    end
  end.
  Definition mult_assoc : forall x y z : G, mult x (mult y z) = mult (mult x y) z.
  Proof.
    intros.
    destruct x.
    destruct y.
    destruct z.
    simpl.
    rewrite G0.mult_assoc.
    rewrite G1.mult_assoc.
    reflexivity.
  Qed.
End SemiGroup_Product.

33.v

Require Import Arith Ring.

Module Type Monoid.
  Parameter M : Type.
  Parameter mult : M -> M -> M.
  Axiom mult_assoc :
    forall x y z : M, mult x (mult y z) = mult (mult x y) z.
  Parameter e : M.
  Axiom id_r : forall x : M, mult x e = x.
  Axiom id_l : forall x : M, mult e x = x.
End Monoid.

Require Import List.

Module ListBool_Monoid <: Monoid.
  Definition M := list bool.
  Definition mult := app (A:=bool).
  Definition mult_assoc := app_assoc (A:=bool).
  Definition e : list bool := nil.
  Definition id_r := app_nil_r (A:=bool).
  Definition id_l := app_nil_l (A:=bool).
End ListBool_Monoid.

Module Monoid_Power (Import M: Monoid).
  Fixpoint pow (x:M.M) (n:nat) : M.M :=
    match n with
      O => M.e
     |S n' => M.mult x (pow x n')
    end.

Lemma exponent1 : forall (x : M.M) (n m: nat), M.mult (pow x n) (pow x m) = pow x (n + m).
Proof.
  intros.
  induction n.
  - simpl.
    rewrite M.id_l.
    reflexivity.
  - simpl.
    rewrite <- M.mult_assoc.
    rewrite IHn.
    reflexivity.
Qed.

Lemma exponent2 : forall (x : M.M) (n m: nat), pow (pow x n) m = pow x (n * m).
Proof.
  induction n;intros.
  - simpl.
    induction m.
    + simpl.
      reflexivity.
    + simpl.
      rewrite IHm.
      apply M.id_r.
  - simpl.
    rewrite <- exponent1.
    rewrite <- IHn.
    induction m.
    + simpl.
      symmetry.
      apply M.id_r.
    + simpl.
      rewrite IHm.
      replace (mult x (pow x n)) with (pow x (S n)) by (simpl;reflexivity).
      replace (mult x (pow x m)) with (pow x (S m)) by (simpl;reflexivity).
      rewrite IHn.
      repeat rewrite exponent1.
      f_equal.
      ring.
Qed.
End Monoid_Power.

Module Type ListBoolPower := ListBool_Monoid <+ Monoid_Power.
Print ListBoolPower.

36.v

Require Import ZArith.

Section Principal_Ideal.
  Variable a : Z.

  Definition pi : Set := { x : Z | ( a | x )%Z }.
  Program Definition plus(a b : pi) : pi := (a + b)%Z.
  Next Obligation.
    destruct a0.
    destruct b.
    simpl.
    destruct d.
    destruct d0.
    exists (x1+x2)%Z.
    subst x x0.
    ring.
  Qed.

  Program Definition mult(a : Z) (b : pi) : pi := (a * b)%Z.
  Next Obligation.
    destruct b.
    simpl.
    destruct d.
    subst x.
    exists (a0*x0)%Z.
    ring.
  Qed.
End Principal_Ideal.

37.v

Require Import SetoidClass.
Require Import Omega.

Record int := {
  Ifst : nat;
  Isnd : nat
}.

Program Instance ISetoid : Setoid int := {|
  equiv x y := Ifst x + Isnd y = Ifst y + Isnd x
|}.
Next Obligation.
Proof.
  split.
  - unfold Reflexive.
    reflexivity.
  - unfold Symmetric.
    intros.
    omega.
  - unfold Transitive.
    intros.
    omega.
Qed.

Definition zero : int := {|
  Ifst := 0;
  Isnd := 0
|}.

Definition int_minus(x y : int) : int := {|
  Ifst := Ifst x + Isnd y;
  Isnd := Isnd x + Ifst y
|}.

Lemma int_sub_diag : forall x, int_minus x x == zero.
Proof.
  destruct x.
  simpl.
  omega.
Qed.

(* まず、int_minus_compatを証明せずに、下の2つの証明を実行して、どちらも失敗することを確認せよ。*)
(* 次に、int_minus_compatを証明し、下の2つの証明を実行せよ。 *)
Instance int_minus_compat : Proper (equiv ==> equiv ==> equiv) int_minus.
Proof.
  unfold Proper.
(*  Print Scopes.
  Print respectful.*)
  unfold respectful.
  intros.
  destruct x.
  destruct y.
  destruct x0.
  destruct y0.
  simpl.
  simpl in H.
  simpl in H0.
  omega.
Qed.

Goal forall x y, int_minus x (int_minus y y) == int_minus x zero.
Proof.
  intros x y.
  rewrite int_sub_diag.
  reflexivity.
Qed.

Goal forall x y, int_minus x (int_minus y y) == int_minus x zero.
Proof.
  intros x y.
  setoid_rewrite int_sub_diag.
  reflexivity.
Qed.

38.v

(* モノイド *)
Class Monoid(T:Type) := {
  mult : T -> T -> T
    where "x * y" := (mult x y);
  one : T
    where "1" := one;
  mult_assoc x y z : x * (y * z) = (x * y) * z;
  mult_1_l x : 1 * x = x;
  mult_1_r x : x * 1 = x
}.

Delimit Scope monoid_scope with monoid.
Local Open Scope monoid_scope.

Notation "x * y" := (mult x y) : monoid_scope.
Notation "1" := one : monoid_scope.

(* モノイドのリストの積。DefinitionをFixpointに変更するなどはOK *)
Definition product_of{T:Type} {M:Monoid T} : list T -> T := (fix product_of' l :=
match l with
  nil => 1%monoid
 |cons x l' => (x * product_of' l')%monoid
end).


Require Import Arith.

(* 自然数の最大値関数に関するモノイド。
 * InstanceをProgram Instanceにしてもよい *)
SearchPattern (max _ 0 = _).
Instance MaxMonoid : Monoid nat := {
  mult := max;
  one := 0;
  mult_assoc := Max.max_assoc;
  mult_1_l := Max.max_0_l;
  mult_1_r := Max.max_0_r
}.

Require Import List.

Eval compute in product_of (3 :: 2 :: 6 :: 4 :: nil). (* => 6 *)
Eval compute in product_of (@nil nat). (* => 0 *)

39.v

(* bindの記法を予約 *)
Reserved Notation "x >>= y" (at level 110, left associativity).

(* モナド *)
Class Monad(M:Type -> Type) := {
  bind {A B} : M A -> (A -> M B) -> M B
    where "x >>= f" := (bind x f);
  ret {A} : A -> M A;
  left_identity {A B} : forall (a: A) (f: A -> M B), bind (ret a) f = f a;
  right_identity {A B}: forall (m: M A) (f: A -> M B), bind m ret = m;
  assoc {A B C}: forall (m : M A) (f:A -> M B) (g: B -> M C), bind (bind m f) g = bind m (fun x => bind (f x) g)
}.

Notation "x >>= f" := (@bind _ _ _ _ x f).

Require Import List.

Print flat_map.

Program Instance ListMonad : Monad list := {|
  bind A B m f := flat_map f m;
  ret A x := x::nil
|}.
Next Obligation.
  apply app_nil_r.
Qed.
Next Obligation.
  induction m.
  - simpl.
    reflexivity.
  - simpl.
    f_equal.
    assumption.
Qed.
Lemma flat_map_app : forall (A B:Type) (l l':list A) (f:A -> list B), flat_map f (l ++ l') = flat_map f l ++ flat_map f l'.
Proof.
  intros.
  induction l.
  - simpl.
    reflexivity.
  - simpl.
    rewrite IHl.
    apply app_assoc.
Qed.

Next Obligation.
  induction m.
  - simpl.
    reflexivity.
  - simpl.
    rewrite flat_map_app.
    rewrite IHm.
    reflexivity.
Qed.
(* 以下、ListMonadが定義できるまでNext Obligation -> Qed を繰り返す *)

(* モナドの使用例 *)

Definition foo : list nat := 1 :: 2 :: 3 :: nil.

(* 内包記法もどき *)
(*
  do x <- foo
     y <- foo
     (x, y)
*)
Definition bar := Eval lazy in
  foo >>= (fun x =>
  foo >>= (fun y =>
  ret (x, y))).

Print bar.

4.v

Theorem DeMorgan1 : forall P Q : Prop, ~P \/ ~Q -> ~(P /\ Q).
Proof.
  intros.
  intro.
  destruct H0.
  destruct H.
  apply H.
  apply H0.
  apply H.
  apply H1.
Qed.

Theorem DeMorgan2 : forall P Q : Prop, ~P /\ ~Q -> ~(P \/ Q).
Proof.
  intros.
  destruct H.
  intro.
  destruct H1.
  apply (H H1).
  apply (H0 H1).
Qed.

Theorem DeMorgan3 : forall P Q : Prop, ~(P \/ Q) -> ~P /\ ~Q.
Proof.
  intros.
  split.
  intro.
  apply H.
  left.
  exact H0.
  intro.
  apply H.
  right.
  exact H0.
Qed.

41.v

Ltac split_all := try (split;split_all).

(* 以下は動作確認用 *)

Lemma bar :
  forall P Q R S : Prop,
    R -> Q -> P -> S -> (P /\ R) /\ (S /\ Q).
Proof.
  intros P Q R S H0 H1 H2 H3.
  split_all.
  - assumption.
  - assumption.
  - assumption.
  - assumption.
Qed.

Lemma baz :
  forall P Q R S T : Prop,
    R -> Q -> P -> T -> S -> P /\ Q /\ R /\ S /\ T.
Proof.
  intros P Q R S T H0 H1 H2 H3 H4.
  split_all.
  - assumption.
  - assumption.
  - assumption.
  - assumption.
  - assumption.
Qed.

Lemma quux :
  forall P Q : Type, P -> Q -> P * Q.
Proof.
  intros P Q H0 H1.
  split_all.
  - assumption.
  - assumption.
Qed.

Record foo := {
  x : (False -> False) /\ True /\ (False -> False);
  y : True;
  z : (False -> False) /\ True
}.

Lemma hogera : foo.
Proof.
  split_all.
  - intros H; exact H.
  - intros H; exact H.
  - intros H; exact H.
Qed.

42.v

Require Import Arith.
Require Import Omega.
Require Import Recdef.
Require Import Arith.Div2.

Function log(n:nat) {wf lt n} :=
  if le_lt_dec n 1 then
    0
  else
    S (log (Div2.div2 n)).
Proof.
  - intros.
    apply lt_div2.
    omega.
  - unfold well_founded.
    intros.
    induction a.
    + apply Acc_intro.
      intros.
      omega.
    + apply Acc_intro.
      intros.
      assert (y = a \/ y < a) by omega.
      destruct H0.
      * subst y.
        assumption.
      * destruct IHa.
        specialize (H1 y).
        apply (H1 H0).
Qed.

43.v

Ltac split_all := match goal with
| |- (_ /\ _) => split;split_all
| _ => idtac
end.

(* 以下は動作確認用 *)

Lemma bar :
  forall P Q R S : Prop,
    R -> Q -> P -> S -> (P /\ R) /\ (S /\ Q).
Proof.
  intros P Q R S H0 H1 H2 H3.
  split_all.
  - assumption.
  - assumption.
  - assumption.
  - assumption.
Qed.

Lemma baz :
  forall P Q R S T : Prop,
    R -> Q -> P -> T -> S -> P /\ Q /\ R /\ S /\ T.
Proof.
  intros P Q R S T H0 H1 H2 H3 H4.
  split_all.
  - assumption.
  - assumption.
  - assumption.
  - assumption.
  - assumption.
Qed.

Lemma quux :
  forall P Q : Type, P -> Q -> P * Q.
Proof.
  intros P Q H0 H1.
  split_all.
  split.
  - assumption.
  - assumption.
Qed.

44.v

Require Import Arith.
Require Import Omega.
Require Import Recdef.
Require Import Arith.Div2.
Require Import Arith.Even.

Function log(n:nat) {wf lt n} :=
  if le_lt_dec n 1 then
    0
  else
    S (log (Div2.div2 n)).
Proof.
  - intros.
    apply lt_div2.
    omega.
  - unfold well_founded.
    intros.
    induction a.
    + apply Acc_intro.
      intros.
      omega.
    + apply Acc_intro.
      intros.
      assert (y = a \/ y < a) by omega.
      destruct H0.
      * subst y.
        assumption.
      * destruct IHa.
        specialize (H1 y).
        apply (H1 H0).
Qed.
(* ここまでは課題42 *)

Fixpoint pow(n:nat) :=
  match n with
  | O => 1
  | S n' => 2 * pow n'
  end.

Lemma log_pow_lb: forall n, 1 <= n -> pow (log n) <= n.
Proof.
  intros n H.
  functional induction (log n).
  simpl.
  assumption.
  simpl.
  assert (pow (log (div2 n)) <= div2 n).
  {
    apply IHn0.
    do 2 (destruct n;[omega|]).
    simpl.
    omega.
  }
  apply le_trans with (double (div2 n)).
  unfold double.
  omega.
  destruct (even_odd_dec n).
  apply even_double in e0.
  omega.
  apply odd_double in o.
  omega.
Qed.

45.v

Require Import ZArith.
Local Open Scope Z_scope.

Inductive Collatz: Z -> Prop :=
| CollatzOne: Collatz 1
| CollatzEven: forall x, Collatz x -> Collatz (2*x)
| CollatzOdd: forall x, Collatz (3*x+2) -> Collatz (2*x+1).

Ltac Collatz_one_step := match goal with
| |- Collatz 1 => apply CollatzOne
| |- Collatz ?X => replace X with (2 * Zdiv2 X) by (simpl;reflexivity);apply CollatzEven;simpl
| |- Collatz ?X => replace X with (2 * Zdiv2 X + 1) by (simpl;reflexivity);apply CollatzOdd;simpl
end.

Ltac SolveCollatz := repeat Collatz_one_step.

Ltac solve_collatz_1000 := repeat match goal with
| _:1 <= ?X <= 1 |- Collatz ?X =>
  assert (X=1) by omega;
  subst X;
  SolveCollatz
| H:1 <= ?X <= ?Y |- Collatz ?X =>
  let H0 := fresh in rename H into H0;
  assert (H:X = Y \/ 1 <= X <= Y-1) by omega;
  clear H0;
  simpl in H;
  destruct H;[subst X;SolveCollatz|]
end.

Theorem Collatz_1000: forall x, 1 <= x <= 1000 -> Collatz x.
Proof.
  intros.
  solve_collatz_1000.
Qed.

5.v

Theorem NotNot_LEM : forall P : Prop, ~ ~(P \/ ~P).
Proof.
  intro.
  intro.
  apply H.
  right.
  intro.
  apply H.
  left.
  exact H0.
Qed.

6.v

Require Import Arith.

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

7.v

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

(*specializeを使ってみた*)
Goal forall P Q : nat -> Prop, P 0 -> (forall x, P x -> Q x) -> Q 0.
Proof.
  intros.
  specialize (H0 0).
  apply (H0 H).
Qed.

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

8.v

Require Import Arith.

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

9.v

Require Import Arith.

Goal forall n m p q : nat, (n + m) + (p + q) = (n + p) + (m + q).
Proof.
  apply 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.
  rewrite (plus_comm (m*n) (m*m)).
  rewrite <- plus_permute_2_in_4.
  apply f_equal.
  rewrite (mult_comm m n).
  replace 2 with (1+1) by (simpl;reflexivity).
  rewrite mult_plus_distr_r.
  rewrite mult_1_l.
  rewrite mult_plus_distr_r.
  reflexivity.
Qed.