Coqの練習だよ。

mathgirl.v

Inductive P : Set :=
    I : P
  | PS : P -> P.

Fixpoint Padd (n m : P) : P :=
  match n with
  | I => PS m
  | PS n' => PS (Padd n' m)
  end.

Lemma Padd_assoc : forall (a b c: P), Padd a (Padd b c) = Padd (Padd a b) c.

Proof.

intros.

induction a.

reflexivity.

simpl.

rewrite IHa.

reflexivity.

Qed.

Lemma Padd_comm : forall (n m : P), Padd n m = Padd m n.

Proof.

intros.

assert (Padd I m = Padd m I).

induction m.

reflexivity.

replace (PS m) with (Padd I m).

rewrite <- Padd_assoc.

rewrite <- IHm.

reflexivity.

reflexivity.

induction n.

rewrite H.

reflexivity.

replace (PS n) with (Padd I n).

rewrite Padd_assoc.

rewrite <- H.

rewrite <- Padd_assoc.

rewrite IHn.

rewrite <- Padd_assoc.

reflexivity.

reflexivity.

Qed.

Fixpoint IPN (n : P) : nat :=
  match n with
  | I => 1
  | PS n' => S (IPN n')
  end.

Definition II := PS I.

Require Import Reals.

Open Scope R_scope.

Fixpoint H (n : P) : R :=
  match n with
  | I => 1
  | PS n' => 1 / (INR (IPN (PS n'))) + H n'
  end.

Goal forall (n : P), H n > 0.

intros.

induction n.

simpl.

unfold Rgt.

apply Rlt_0_1.

Qed.

Goal forall (n : P), H (Padd n I) - H n > H (Padd n II) - H (Padd n I).

intro n.

unfold Padd.

Qed.