Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] can't implement a simple function with certified type

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] can't implement a simple function with certified type


Chronological Thread 
  • From: Ömer Sinan Ağacan <omeragacan AT gmail.com>
  • To: coq club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] can't implement a simple function with certified type
  • Date: Sun, 13 Jul 2014 15:29:32 +0300

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



Archive powered by MHonArc 2.6.18.

Top of Page