ちょっといじった数学的帰納法

2010-09-19 - ひとり勉強会の練習問題。

||<Require Import Arith Omega.

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

Theorem Sum_of_nat:
 forall (n m: nat),
   m = 2 * sum n -> m = n*(n+1).
Proof.
 intro n.
 induction n.

 (以下は練習問題)

なんとか解けたけどかなり苦戦した。三日かかった。

Require Import Arith.
Require Import Omega.

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

Theorem Sum_of_nat:
 forall (n m: nat),
   m = 2 * sum n -> m = n*(n+1).
Proof.
  intro n.

  induction n.
    intros.
    simpl in H.
    simpl.
    auto.

    intros.
    rewrite H.
    simpl.
    ring_simplify.

  (* 2 * n + 2 * sum n + 2 = n * n + 3 * n + 2 *)
  (* 2*sum mを引っ張り出すために *)
  assert(forall (a b c d e:nat), a<=d+e -> b=d+e-a -> a+b+c=d+e+c).
    intros.
    rewrite H1.
    assert(forall (a b c:nat), a=c -> a+b=c+b).
      intros.
      omega.
    apply H2.
    apply (le_plus_minus_r a (d+e)).
    apply H0.

  apply H0.
  (* 後回し *)
  all: cycle 1.

  (* 2 * sum n = n * n + 3 * n - 2 * n *)
  rewrite IHn.
  apply IHn.
  auto.
  assert(forall(a:nat), a+3*n-2*n=a+n).
    intros.
    omega.
  rewrite H1.
  rewrite IHn.
  ring.
  auto.

  (* 2 * n <= n * n + 3 * n *)
  assert(forall x y z : nat, x * z + y * z = (x + y) * z).
    assert(forall a b:nat, a=b->b=a).
      auto.
    intros.
    apply H1.
    apply (Nat.mul_add_distr_r).
  rewrite H1.
  apply Nat.mul_le_mono_nonneg_r.
  omega.
  omega.
Qed.

それに、ここまで長手数かかるものなのかな〜
「もっと短手数で解けるよ」って方がいたら教えて下さい。