The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-07-13 14:29 GMT+02:00 Ö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.

If the order of the arguments matter you can also mark the argument on which you recurse with the 'struct' keyword.

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

Note: I have separated the 'A' argument from 'l' and 'idx'. It is not mandatory, but I prefer to put only the minimum set of arguments for the recursion.
'A' is constant here, so no need to pass it in recursive calls, as you set it implicit, you may have not take care of it but your original recursive call was "@rev_at_aux A idx' t".
This is similar to parameters/indice also talked in this thread.

 

  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.

In a first time, you could try to do it with the eliminator.

When

Inductive vector (A : Type) : nat -> Type :=
| Nil : vector A O
| Cons : A -> forall n, vector A n -> vector A (S n).

is declared (I do not recall the exact definition), three terms are automatically defined (unless you use special options):

vector_ind
vector_rec
vector_rect

they more or less have the same type (only difference is whether target is Prop, Set or Type instead of '*' in the following):
forall A (P : forall n, vector A n -> *), (P O (Nil A)) -> (forall a n (v : vector A n) -> P n v -> P (S n) (Cons A a n v)) -> forall n (v : vector A n) -> P n v.

This term is called the enumerator and is used by the "induction" tactic (more or less a wrapper for "apply …_ind").
Using it is less readable, but easier to write (no guardedness issue, no dependant pattern matching).

Once you have defined a term using this eliminator, say 'X', you can try to do a "Define Y := Eval cbv delta [X vector_ind] in X." (not sure of the case for 'Eval').
Then "Print Y." should give you a term using the "raw dependant pattern matching".
And "Define Z := Eval simpl in Y." should simplify it if too ugly.

In a second time, you can try to understand and write your own raw dependant matching.
 

Thanks again,

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

--
.../Sedrikov\...