coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] can't implement a simple function with certified type, Ömer Sinan Ağacan, 07/13/2014
- Re: [Coq-Club] can't implement a simple function with certified type, Jonathan, 07/13/2014
- Re: [Coq-Club] can't implement a simple function with certified type, Ömer Sinan Ağacan, 07/13/2014
- Re: [Coq-Club] can't implement a simple function with certified type, Jonathan, 07/13/2014
- Re: [Coq-Club] can't implement a simple function with certified type, Cedric Auger, 07/15/2014
- Re: [Coq-Club] can't implement a simple function with certified type, Cedric Auger, 07/15/2014
- Re: [Coq-Club] can't implement a simple function with certified type, Jonathan, 07/13/2014
- Re: [Coq-Club] can't implement a simple function with certified type, Ömer Sinan Ağacan, 07/13/2014
- Re: [Coq-Club] can't implement a simple function with certified type, Jonathan, 07/13/2014
Archive powered by MHonArc 2.6.18.