The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

You made error in the definition of w.

Require Import Arith.

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.

Lemma foo: forall n, w n (2 * n + 1).

 induction n.

  apply C0.

  eapply CS; eauto. ring.

Qed.

On Thu, Oct 2, 2014 at 7:08 PM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

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.

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