The Coq mailing list

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

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

This worked great, thanks! Generated OCaml code also better now:

  (** val nth_triangle_aux : nat -> nat -> 'a1 triangle_t -> 'a1 t **)

  let rec nth_triangle_aux steps_left stop tr =
    match steps_left with
    | O -> let Triangle (n, x, x0) = Lazy.force tr in x
    | S n' ->
      nth_triangle_aux n' stop (let Triangle (n, x, x0) = Lazy.force tr in x0)

Thanks again!

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


2014-04-07 3:01 GMT+03:00 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:
>

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