The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/12/2014 07:26 PM, Ömer Sinan Ağacan wrote:
> Hi all,
>
> I'm trying to implement a somewhat certified version of a very simple
> function and I'm very confused.
>
> The function is this: reverse a list at given index. For example,
> `rev_at 1 [1; 2; 3; 4]` should return `[1; 4; 3; 2]`.
>
> I want to have a type that 1) ensures that given index < length of
> list 2) return value is of same length with the argument.
>
> Here's what I tried.
>
> First, I implemented a simply typed version and then wrapped it with
> precisely typed version:
>
>    Fixpoint rev_at_aux {A} (l : list A) idx : list A :=
>      match idx with
>      | 0 => rev l
>      | S idx' =>
>          match l with
>          | [] => []
>          | h :: t => h :: rev_at_aux t idx'
>          end
>      end.
>
>    Definition rev_at {A} (l : list A) idx (p : idx < length l) : list A :=
>      rev_at_aux l idx.
>
> Now this definition works fine but it's missing (2). For that I
> modified the definition:
>
>    Definition rev_at' {A} (l : list A) idx (p : idx < length l) : {l' :
> list A | length l' = length l}.
>      apply exist with (x := rev_at l idx p). unfold rev_at. unfold
> rev_at_aux. induction idx as [|idx'].
>      + (* I'm stuck, I have a fix application and I can't use simpl. *)
>    Abort.

Try this trick: put the idx arg before the l arg in rev_at_aux. Keep 
rev_at the same.  Then use compute [rev_at_aux] instead of the unfold 
rev_at_aux.  Then you should be able to see how to continue.

I think what happened is that Fixpoint decided to use the list l for 
structural recursion - and that means without destructing l, you won't 
be able to step into rev_at_aux.  Putting idx before l changes this to 
doing structural recursion on idx.

Alternatively, you probably could have done induction over l instead of 
idx in rev_at', as you did below.

> But I have no idea how to implement this. I tried refine but I never
> managed to use that as mentioned below.
>
> I know I can prove a theorem saying that `length (rev_at l idx p) = length l`:
>
>    Require Import Omega.
>
>    Theorem rev_at_l : forall A l idx p, length (@rev_at A l idx p) = length l.
>    Proof.
>      intros. generalize dependent idx. induction l as [|h t]; intros.
>      + destruct idx; auto.
>      + destruct idx as [|idx'].
>        - unfold rev_at. unfold rev_at_aux. apply rev_length.
>        - simpl in p. assert (idx' < length t). omega.
>          simpl. f_equal. apply IHt with (p := H).
>    Qed.
>
> But for learning purposes, I'd like to implement this without
> implementing theorems separately.
>
> Second, I tried using vectors:
>
>    Require Vector.
>
>    Definition rev_at'' : forall A len (v : Vector.t A len) (idx : nat)
> (p : idx < len), Vector.t A len.
>      refine (fix f A len v idx p :=
>        match v with
>        | Vector.nil => Vector.nil
>        | Vector.cons h len' t => _
>        end).
>
> .. and I failed again. I never managed to use refine for anything
> useful. In this case, I'm getting this weird type error:
>
>    Error: The term
>     "fix f (A : ?548) (len : ?549) (v : Vector.t ?556 ?557) (idx : ?551)
>            (p : ?552) {struct v} : forall A0 : Type, Vector.t A0 ?570 :=
>        match
>          v as v0 in (Vector.t _ n) return (forall A0 : Type, Vector.t A0 ?570)
>        with
>        | [] => Vector.nil
>        | Vector.cons h len' t => ?568
>        end" has type
>     "forall (A : ?548) (len : ?549) (v : Vector.t ?556 ?557) (idx : ?551)
>        (p : ?552) (A0 : Type), Vector.t A0 ?570"
>     while it is expected to have type
>     "forall (A : Type) (len : nat),
>      Vector.t A len -> forall idx : nat, idx < len -> Vector.t A len".
>
> If I replace first case with underscore, it works(what's wrong with
> current version?) but then I can't prove goals because there are lost
> information. For example, in second case, I don't have `len = S len'`
> or `v = Vector.cons h len' t`. I'm trying to figure out how to use
> refine for some long time now but I never understand how to do
> anything useful with all the information lost when refine is used.
>
> So I'm stuck and confused. Can anyone help me defining this?
>
> Thanks.

The important difference here between lists and vectors is that the 
Vector type has a dependent index, not just a parameter (which is all 
list has).   Matching on types that have dependent indexes generally 
requires the more complex varieties of match expressions as described in 
refman chapter 17.  Adam Chlipala's CPDT book does decent job of guiding 
you through this morass.

-- Jonathan