The Coq mailing list

[Frederic Chyzak <frederic.chyzak AT inria.fr>]

Hi,

On Thu, 2014-10-02 at 17:35 +0200, Christophe Bal wrote:

> Let's consider the sequence defined by  n w_n = (n + 1)w_{n-1} + 1
>  with the initial condition  w_0 = 1 .
>
> How can I verify the validity of  w_n = 2 n + 1 ?

To my mathematical eye, this problem reads: "Consider the sequence that
is (obviously well) defined by w_0 = 1 and, for n >= 1, by w_n = ((n+1)
w_{n-1} + 1) / n.  Prove that w_n (necessarily) equals 2 n + 1."

So, this is really a uniqueness question, and uniqueness turned out to
be more difficult (to me) to prove than existence.

For comparison's sake, below are three proofs (existence and
uniqueness):
- a first one with essentially the same Inductive formalization as in
the discussion so far,
- a variant that avoids using inversion,
- a last one that was my first reaction, by formalizing a sequence as a
(fun (n : nat) -> ...).

The goal of the second proof was really to avoid the random names
introduced by inversion.  It also gains one proof step in the uniqueness
proof.

With regard to style, I haven't tried to make any of these variants more
compact than another.  In particular, I haven't played with implicit
arguments, which would reduce the width of several lines.  But the last
proof is just shorter than the others.  I also tend to view is as more
intuitive: I can speak of (some explicit representation of) w_n
explicitly only in this last proof.

Frédéric



(* I never learnt Coq's (standard) tactics, so I use ssreflect's
instead. *)
Require Import ssreflect.
Require Import Arith.

(* The theory of recurrent sequences is really over a field.  It is only
by
   accident that the proposed recurrence has an integer solution.
Originally, I
   wanted to treat the case R = Q or R = the reals, but seeing the start
of the
   discussion, I did not want to be more different. *)
Definition R := nat.


(* Two helper lemmas that I could not find in the standard library.  I
have not
   searched seriously, though. *)
Module Helper.

Lemma mult_diff_zero (n : nat) (r r' : R) : S n * (r - r') = 0 -> r <=
r'.
Proof.
move=> h.
case: (mult_is_O (S n) (r - r') h) => // {h} h.
exact: (iffLR (NPeano.Nat.sub_0_le r r') h).
Qed.

Lemma simplify_by_nonzero (n : nat) (r r' : R) : S n * r = S n * r' -> r
= r'.
Proof.
move=> h.
have /mult_diff_zero h' : S n * (r - r') = 0.
  by rewrite mult_minus_distr_l h minus_diag.
have {h} /mult_diff_zero h'' : S n * (r' - r) = 0.
  by rewrite mult_minus_distr_l h minus_diag.
exact: le_antisym.
Qed.

End Helper.


Module SequenceAsAnInductive.

Inductive assoc : nat -> R -> Prop :=
| C0 : assoc 0 (1 : R)
| CS : forall (n : nat) (r r' : R),
    assoc n r -> S n * r' = S (S n) * r + 1 -> assoc (S n) r'.

Definition w0 (n : nat) : R := 2 * n + 1.

(* There exists a family of terms in (assoc n _), one for each (n :
nat).
   For instance, choose (w0 n) as the second argument. *)
Lemma existence (n : nat) : assoc n (w0 n).
Proof.
elim: n => [ | n val_at_n].
  exact: C0.
apply: (CS n (w0 n) (w0 (S n)) val_at_n).
rewrite /w0.
ring.
Qed.

(* Any family of terms in (assoc n _), one for each (n : nat), must have
the
  (w0 n) as their second arguments. *)
Lemma uniqueness (n : nat) (r : R) : assoc n r -> r = w0 n.
Proof.
elim: n r => [r a0r | n hn r' aSnr]; first by inversion a0r.
inversion aSnr => {H2 H r'0 n0 aSnr}.
move: (hn r H0) => hr {hn H0}.
apply: (Helper.simplify_by_nonzero n).
rewrite H1 hr /w0.
ring.
Qed.

End SequenceAsAnInductive.



Module SequenceAsAnInductiveNoInversion.

Require Import Arith.

Definition R := nat.

Inductive assoc : nat -> R -> Prop :=
| C0 : forall (n : nat) (r : R), n = 0 -> r = (1 : R) -> assoc n r
| CS : forall (n n' : nat) (r r' : R),
    n' = S n -> assoc n r -> S n * r' = S (S n) * r + 1 -> assoc n' r'.

Definition w0 (n : nat) : R := 2 * n + 1.

(* There exists a family of terms in (assoc n _), one for each (n :
nat).
   For instance, choose (w0 n) as the second argument. *)
Lemma existence (n : nat) : assoc n (w0 n).
Proof.
elim: n => [ | n val_at_n].
  exact: C0.
apply: (CS n (S n) (w0 n) (w0 (S n)) eq_refl val_at_n).
rewrite /w0.
ring.
Qed.

(* Any family of terms in (assoc n _), one for each (n : nat), must have
the
  (w0 n) as their second arguments. *)
Lemma uniqueness (n : nat) (r : R) : assoc n r -> r = w0 n.
Proof.
elim=> [_ _ -> -> //| {n r} n _ r' r -> anr h].
move: h anr => -> {r'} _ h.
apply: (Helper.simplify_by_nonzero n).
rewrite h /w0.
ring.
Qed.

End SequenceAsAnInductiveNoInversion.



Module SequenceAsAFun.

Definition w0 (n : nat) : R := 2 * n + 1.

Definition is_sol (w : nat -> R) : Prop :=
  w 0 = 1 /\ forall (n : nat), (n + 1) * w (S n) = (n + 2) * w n + 1.

Lemma existence : is_sol w0.
Proof.
split=> [//= | n].
rewrite /w0.
ring.
Qed.

Lemma uniqueness (w : nat -> R) : is_sol w -> forall (n : nat), w n = w0
n.
Proof.
case=> initial_cond rec.
elim=> [ | n ih {initial_cond}].
  rewrite initial_cond /w0.
  (* 'ring' would work out of the box if I did not use R instead of nat.
*)
  by rewrite mult_0_r plus_O_n.
apply: (Helper.simplify_by_nonzero n).
have {1}-> : S n = n + 1 by rewrite plus_comm //.
rewrite {}rec {}ih /w0 {w}.
ring.
Qed.

End SequenceAsAFun.