The Coq mailing list

[Christophe Bal <projetmbc AT gmail.com>]

Thanks for the answers.

Christophe.

PS : the use of  n-...  indices in formula is not a necessity, so I would use only n+... indices.

2014-10-02 18:30 GMT+02:00 Cedric Auger <sedrikov AT gmail.com>:

2014-10-02 18:08 GMT+02:00 Pierre Courtieu <pierre.courtieu AT gmail.com>:

Here is an attempt but I reach something wrong. Are you sure about
this statement?

Require Import Ring.
Require Import Arith.

Inductive w: nat -> nat -> Prop :=
 | C0: w 0 1
 | CS : forall n x y, w n y -> n*x = (S n)*y+1 -> w (S n) x.

You got tricked with indice, Pierre. The correct form is the following one:

Inductive w: nat -> nat -> Prop :=
 | C0: w 0 1
 | CS : forall n x y, w n y -> (S n)*x = (S (S n))*y+1 -> w (S n) x.

That confirms my intuition that we should never use "u_{n-k}" when k>0 to define sequences, but only "u_{n+}" where k≥0.

That would have made the following description:

w₀=1
(n+1)×wₙ₊₁ = (n+2)×wₙ+1

I mostly prefer to write the second equation this way, as it is meaningful for all natural number n even when n=0.
I cannot try if the remaining part of Pierre’s proof works, as I have no Coq installation.

You could also consider this way to do the proof:

Lemma foo1: forall n m, w n m -> 2 * n + 1 = m.
Proof.
  intros n m Hnm; induction Hnm.
…
Qed.

Lemma foo2: forall n, exists m, w n m.
Proof.
  induction n.
…
Qed.

Lemma foo: forall n, w n (2 * n + 1).
Proof.
  intros n; destruct (foo2 n) as [m Hm]; rewrite (foo1 n m Hm); exact Hm.
Qed.
 

Lemma foo: forall n, w n (2 * n + 1).
Proof.
  induction n.
  - constructor.
  - simpl in *.
    eapply CS.
    apply IHn.
    ring_simplify.
    (* wrong *)


2014-10-02 17:35 GMT+02:00 Christophe Bal <projetmbc AT gmail.com>:
> Hello.
>
> Sorry for this very low level question (I still not found the time to learn
> seriously Coq).
>
> 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 ?
>
> Christophe

--
.../Sedrikov\...