The Coq mailing list

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

Thanks for the answer,

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

This works! Great. Even though I still can't implement solution using
vectors, I can have this:

  Fixpoint rev_at_aux {A} idx (l : list A) : list A :=
    match idx with
    | 0 => rev l
    | S idx' =>
        match l with
        | [] => []
        | h :: t => h :: rev_at_aux idx' t
        end
    end.

  Require Import Omega.

  Definition rev_at {A} (l : list A) idx (p : idx < length l) : list A :=
    rev_at_aux idx l.

  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.

  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. destruct idx as [|idx'].
    + apply rev_length.
    + destruct l. reflexivity. simpl. f_equal.
      simpl in p. apply lt_S_n in p.
      apply rev_at_l with (p := p).
  Defined.

Also, I still need `rev_at_l` theorem, I was hoping to eliminate that.
I can eliminate that but I'd need to prove same thing using `assert`
or something similar, I'm trying to not to use tactics here.(not
because of a problem, just for learning purposes) So there are still
some room for improvements.

I also checked extracted OCaml code and it's very good:

  let rec rev_at_aux idx l =
    match idx with
    | O -> rev l
    | S idx' ->
      (match l with
       | Nil -> Nil
       | Cons (h, t) -> Cons (h, (rev_at_aux idx' t)))
  let rev_at l idx = rev_at_aux idx l
  let rev_at' l idx = rev_at l idx

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

What's difference between index and parameter?

I'm still open for suggestions to implement it using vectors and refine.

Thanks again,

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