The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Mon, 7 Apr 2014 00:21:28 +0300,
Ömer Sinan Ağacan 
<omeragacan AT gmail.com>
 a écrit :

> > 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

Sorry for indentation breaking. n' was not a subterm of steps_left, but
rather a subterm of "nat_cases steps_left", which is completely
different from Coq point of view. The following code works:

  Definition nth_triangle_aux
    : forall T steps_left stop,
      stop >= steps_left -> triangle_t T (stop - steps_left) ->
  Vector.t T stop. intros T.
    refine (fix fn (steps_left stop : nat)
            : (stop >= steps_left) -> (triangle_t T (stop -
  steps_left)) -> Vector.t T stop :=
      fun pf tr =>
      match steps_left as sl return steps_left = sl -> Vector.t T stop
  with | S n' => fun NZ => _
      | O => fun Z => _
      end (eq_refl steps_left)).
    subst. rewrite <- minus_n_O in tr. inversion tr; auto.
    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.
  Defined.


But I often prefer to do things like that, where you do not have to
introduce equalities to eliminate them later.

  Definition nth_triangle_aux
    : forall T steps_left stop,
      stop >= steps_left -> triangle_t T (stop - steps_left) ->
  Vector.t T stop. intros T.
    refine (fix fn (steps_left stop : nat)
            : (stop >= steps_left) -> (triangle_t T (stop -
  steps_left)) -> Vector.t T stop :=
      match steps_left as sl
      return (stop >= sl) -> (triangle_t T (stop - sl)) -> Vector.t T
  stop with | S n' => _
      | O => _
      end).
    rewrite <- minus_n_O. intros _ [n v _]. exact v.
    intros pf tr; apply fn with (steps_left := n').
      apply le_trans with (S n'); auto.
      assert (S (stop - S n') = stop - n'). omega.
        case H; case tr.
        auto.
  Defined.