The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

> Definition nat_cases (n: nat) :
>   { n' : nat | n = S n' } + {n = 0} :=
>   match n with
>   | O => inright _ eq_refl
>   | S n' => inleft _ (exist _ n' eq_refl)
>   end.
>
> Goal ∀ n : nat, True.
>   intros n.
>   refine
>     match nat_cases n with
>     | inleft (exist n' NZ) => _
>     | inright Z => _
>     end.
> Abort.

Thanks for your answer. I tried using this but I'm getting this error:

> Recursive call to fn has principal argument equal to "n'" instead of
> a subterm of "steps_left".

but n' is already a subterm of steps_left. What am I doing wrong?
Here's my program: (error is given when last line is executed)

  Require Import Omega.
  Require Import Coq.Vectors.Vector.
  Require Import Coq.Vectors.VectorDef.
  Open Scope vector_scope.
  Require Import Bool.
  Require Import List.
  Require Import Arith.
  Require Import Arith.EqNat.
  Require Import Program.

  Definition admit {T: Type} : T.  Admitted.

  CoInductive triangle_t (T : Type) : nat -> Type :=
  | triangle : forall (n : nat), Vector.t T n -> triangle_t T (S n) ->
triangle_t T n.

  Definition nat_cases (n: nat) :
    { n' : nat | n = S n' } + {n = 0} :=
    match n with
    | O => inright _ eq_refl
    | S n' => inleft _ (exist _ n' eq_refl)
    end.

  Definition nth_triangle_aux
    : forall T steps_left stop,
      stop >= steps_left -> triangle_t T (stop - steps_left) -> Vector.t T 
stop.
    refine (fix fn T (steps_left stop : nat)
                     (pf : stop >= steps_left)
                     (tr : triangle_t T (stop - steps_left))
                     : Vector.t T stop :=
      match nat_cases steps_left return Vector.t T stop with
      | inleft (exist n' NZ) => _
      | inright Z => _
      end).
    apply fn with (steps_left := n').
      rewrite NZ in pf. omega.
      rewrite NZ in tr. inversion tr; subst.
        assert (S (stop - S n') = stop - n'). omega.
        rewrite H in X0. apply X0.
    subst. rewrite <- minus_n_O in tr. inversion tr; auto.
  Defined.

---
Ömer Sinan Ağacan
http://osa1.net