The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

Hello all.

I've just started learning coq (and studying type theory in general). I'm
following the CPDT and 'Software Foundations' books online. I'm trying to
write a (what I assume is a) simple proof involving bounded numbers, but
unfortunately I'm stuck on the induction step.

Here's what I have:

------------------------------------------------------------------------

Require Import Coq.Arith.Lt.

Inductive fin : nat -> Type :=
  | FZ : forall (b : nat), fin (S b)
  | FS : forall (b : nat), fin b -> fin (S b).

Implicit Arguments FZ [b].
Implicit Arguments FS [b].

Fixpoint fin_nat {b : nat} (f : fin b) : nat :=
  match f with
    | FZ _    => 0
    | FS _ f' => S (fin_nat f')
  end.

Definition fin_bound {b : nat} (_ : fin b) : nat := b.

Theorem eq_fin_bound_fb_b : forall (b : nat) (f : fin b),
  fin_bound f = b.
Proof. reflexivity. Qed.

Theorem lt_fin_nat_fb_b : forall (b : nat) (f : fin b),
  fin_nat f < fin_bound f.
Proof.

------------------------------------------------------------------------

Here's my session so far:

------------------------------------------------------------------------

Welcome to Coq 8.3pl1 (April 2011)

lt_fin_nat_fb_b < Show.
1 subgoal

  ============================
   forall (b : nat) (f : fin b), fin_nat f < fin_bound f

lt_fin_nat_fb_b < intros b f.
1 subgoal

  b : nat
  f : fin b
  ============================
   fin_nat f < fin_bound f

lt_fin_nat_fb_b < induction f.
2 subgoals

  b : nat
  ============================
   fin_nat FZ < fin_bound FZ

subgoal 2 is:
 fin_nat (FS f) < fin_bound (FS f)

lt_fin_nat_fb_b < simpl.
2 subgoals

  b : nat
  ============================
   0 < fin_bound FZ

subgoal 2 is:
 fin_nat (FS f) < fin_bound (FS f)

lt_fin_nat_fb_b < unfold fin_bound.
2 subgoals

  b : nat
  ============================
   0 < S b

subgoal 2 is:
 fin_nat (FS f) < fin_bound (FS f)

lt_fin_nat_fb_b < apply lt_O_Sn.

------------------------------------------------------------------------

The problem is when I now get to the second inductive step. I'm unable
to go further:

------------------------------------------------------------------------

1 subgoal

  b : nat
  f : fin b
  IHf : fin_nat f < fin_bound f
  ============================
   fin_nat (FS f) < fin_bound (FS f)

lt_fin_nat_fb_b < simpl.
1 subgoal

  b : nat
  f : fin b
  IHf : fin_nat f < fin_bound f
  ============================
   S (fin_nat f) < fin_bound (FS f)

lt_fin_nat_fb_b < unfold fin_bound.
1 subgoal

  b : nat
  f : fin b
  IHf : fin_nat f < fin_bound f
  ============================
   S (fin_nat f) < S b

...

lt_fin_nat_fb_b < unfold fin_nat.
1 subgoal

  b : nat
  f : fin b
  IHf : fin_nat f < fin_bound f
  ============================
   S
     ((fix fin_nat (b0 : nat) (f0 : fin b0) {struct f0} : nat :=
         match f0 with
         | FZ _ => 0
         | FS b1 f' => S (fin_nat b1 f')
         end) b f) < S b

I'm left scratching my head, unfortunately. I'm not sure what I need
to be able to solve this.

Any help would be appreciated.