The Coq mailing list

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

I made it working with a small addition to the code:

  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).
    destruct steps_left.
    inversion NZ.
    apply fn with (steps_left := steps_left).
      rewrite NZ in pf. omega.
      rewrite NZ in tr. inversion tr; subst.
        assert (S (stop - S n') = stop - n'). omega.
        rewrite H in X0. inversion NZ; subst. apply X0.
    subst. rewrite <- minus_n_O in tr. inversion tr; auto.
  Defined.

I'm still wondering if there's a way to tell Coq that n' is already a
subterm of steps_left.

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


2014-04-07 0:21 GMT+03:00 Ö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