The Coq mailing list

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

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.

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.

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