The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday, April 05, 2014 10:34:31 PM Ömer Sinan Ağacan wrote:
> Thanks for your answer! I tried using eq_nat_dec without using lemmas,
> just to see how error will change and how does that help Coq inferring
> stop = n, but it's still giving same error message:
> 
>   Fixpoint nth_triangle_aux {T : Type} (idx stop : nat) (tr :
> triangle_t T idx) : Vector.t T stop :=
>     if eq_nat_dec idx stop then
>       match tr with triangle _ _ v _ => v end
>     else
>       match tr with triangle _ _ _ tr' => nth_triangle_aux (S idx) stop tr'
> end.
> 
>   Error:
>   In environment
>   nth_triangle_aux : forall (T : Type) (idx stop : nat),
>                      triangle_t T idx -> Vector.t T stop
>   T : Type
>   idx : nat
>   stop : nat
>   tr : triangle_t T idx
>   e : idx = stop
>   T0 : Type
>   n : nat
>   v : Vector.t T0 n
>   t : triangle_t T0 (S n)
>   The term "v" has type "Vector.t T0 n" while it is expected to have type
>    "Vector.t ?23 stop".
> 
> Is there anything else I need to do for telling Coq that stop = n?

Here's one way to get it to displaying "Error: Cannot guess decreasing 
argument of fix.":

First, I noticed that the original definition of triangle_t unnecessarily 
makes 
T a "non-fixed" parameter of the coinductive definition; so I revised that to:

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

Then:

  Fixpoint nth_triangle_aux {T : Type} (idx stop : nat) (tr :
triangle_t T idx) : Vector.t T stop :=
    match eq_nat_dec idx stop with
    | left e => match e in (_ = stop') return Vector.t T stop' with
                | eq_refl => match tr in (triangle_t _ idx')
                             return (Vector.t T idx') with
                             triangle _ v _ => v
                             end
                end
    | right ne =>
      match tr in (triangle_t _ n) return (S idx = S n -> Vector.t T stop) 
with
      triangle n _ tr' => fun eq : S idx = S n =>
             match eq in (_ = Sn) return (triangle_t T Sn -> Vector.t T stop)
             with
             | eq_refl => fun tr' => nth_triangle_aux (S idx) stop tr'
             end tr'
      end eq_refl
    end.

As Adam already pointed out, reading up on methods to work with dependent 
types in general would help with understanding this, or coming up with 
similar 
constructs.  Or, as I hinted before but I guess I wasn't explicit enough, 
making it a Program Fixpoint will let the Program facility help you with 
constructing equalities in matches, and using equalities to do "conversions". 
 
(Although I often find myself wishing Program worked more like the upcoming 
"invert" tactic, rather than the old "inversion" tactic, i.e. using less 
auxiliary equality proofs.  So I sometimes end up writing things out that way 
anyway.)

Another small comment: the match on an equality wouldn't be necessary in the 
second case (right ne), if you were willing to rewrite it as

match tr with
| triangle n _ tr' => nth_triangle_aux (S n) stop tr'
end
-- 
Daniel Schepler