The Coq mailing list

[Anton Trunov <anton.a.trunov AT gmail.com>]

Hi Klaus,

FWIW, there is a function `cast`, defined in 
https://coq.inria.fr/library/Coq.Vectors.VectorEq.html

Here is another take on `vmap_map`:

From Coq Require Import Vector List.

Lemma vmap_map : forall {A B} {f : A -> B} {v: list A},
  Vector.map f (Vector.of_list v) = cast (Vector.of_list (map f v)) 
(map_length _ _).
Proof.
  intros A B f v.
  generalize (map_length f v).
  induction v; intro.
  - reflexivity.
  - now simpl; rewrite <- IHv.
Qed.

—
Kind regards,
Anton

> On 20 Jan 2017, at 16:34, Dominique Larchey-Wendling 
> <dominique.larchey-wendling AT loria.fr>
>  wrote:
> 
> Hi Klaus,
> 
> The eq_cong term you define already exists in the library
> (possibly with the parameters in a different order), it
> is the recursion principle of equality:
> 
> eq_rect
> 
> You need to open eq_cong (Defined instead of Qed) to be able
> to compute with it.
> 
> The problem with dependent types is that, unless you are
> very careful and very modest in your expectations, you are
> rapidly confronted with having to compute with proof terms.
> 
> But this is basically a nightmare for at least two reasons:
> 
> 1/ proofs are usually much more complicated than programs
> 2/ Coq is specifically designed to be as much as proof
>   irrelevant as it can without additional axioms. Thus
>   all the proof terms are opaque and you cannot compute
>   with them ... so basically, for computing with proofs,
>   you have to rewrite and open all the proofs you use in
>   the standard library ...
> 
> Notice that when the dependent parameter is of a type with
> a decidable equality, or simply has unique identity proofs,
> then you might be able to avoid point 2) (opening all
> proof terms) as is done in the following solution to
> your problem.
> 
> Welcome in the wonderful world on dependent types !!!!
> 
> Best regards,
> 
> Dominique
> 
> (**************************************************)
> 
> Require Import Arith List Vector Eqdep_dec.
> 
> Fact uip_nat (n m : nat) (H1 H2 : n = m) : H1 = H2.
> Proof.
>  apply UIP_dec, eq_nat_dec.
> Qed.
> 
> Section eq_rect.
> 
>  Variables (A : Type) (P : A -> Type).
> 
>  Fact eq_rect_sym x tx y (H : x = y) ty :
>     ty = eq_rect _ P tx _ H -> eq_rect _ P ty _ (eq_sym H) = tx.
>  Proof.
>    subst; auto.
>  Qed.
> 
>  Fact eq_rect_trans x y z (tx : P x) (ty : P y) (tz : P z) (H1 : x = y)
> (H2 : y = z) :
>     eq_rect _ P (eq_rect _ P tx _ H1) _ H2 = eq_rect _ P tx _ (eq_trans
> H1 H2).
>  Proof.
>    subst; auto.
>  Qed.
> 
> End eq_rect.
> 
> Fact S_fun (n m : nat) : n = m -> S n = S m.
> Proof. intros []; auto. Defined.
> 
> Fact eq_rect_cons A n x (v : t A n) m (H : n = m) :
>     cons A x m (eq_rect _ (t A) v _ H) = eq_rect _ (t A) (cons A x n v)
> _ (S_fun _ _ H).
> Proof.
>  subst; auto.
> Qed.
> 
> Section vmap_map.
> 
>  Variables (A B : Type) (f : A -> B).
> 
>  Lemma vmap_map (l: list A) :
>    Vector.map f (Vector.of_list l) = eq_rect _ (t B) (of_list (List.map
> f l)) _ (map_length f l).
>  Proof.
>    induction l as [ | x l IHl ]; simpl.
> 
>    generalize (map_length f (@List.nil A)).
>    simpl; intros H1.
>    rewrite uip_nat with (H1 := H1)
>                         (H2 := eq_refl); auto.
> 
>    rewrite IHl, eq_rect_cons; f_equal.
>    apply uip_nat.
>  Qed.
> 
> End vmap_map.
> 
> 
> 
> 
> Le 20/01/2017 à 11:45, Klaus Ostermann a écrit :
>> I want to state (and prove) a lemma that conversion of
>> lists to vectors commutes with mapping.
>> 
>> Hence my lemma should look something like this:
>> 
>> Lemma vmap_map: forall  {A B}{f : A -> B}{ l: list A},
>> Vector.map f (Vector.of_list l) = Vector.of_list (map f l).
>> 
>> This lemma is not accepted by Coq because:
>> 
>>> The term "Vector.of_list (map f l)" has type "Vector.t B (length (map
>> f l))"
>>> while it is expected to have type "Vector.t B (length l)".
>> 
>> There's a lemma in the standard library, which proves the required
>> equality, namely map_length:
>> 
>> map_length
>>     : forall (A B : Type) (f : A -> B) (l : list A),
>>       length (map f l) = length l
>> 
>> But how can I tell Coq that it should accept my lemma due to map_length?
>> 
>> One thing I tried was to reformulate the lemma using an explicit auxiliary
>> congruence lemma:
>> 
>> Lemma eq_cong: forall {A} {x : A} {y : A} P, x = y -> P x -> P y.
>> 
>> With this auxiliary Lemma, I can reformulate map_vmap in such a way
>> that Coq accepts the lemma:
>> 
>> Lemma vmap_map: forall  {A B}{f : A -> B}{ v: list A},
>> Vector.map f (Vector.of_list v) = eq_cong (Vector.t B) (map_length f v)
>> (Vector.of_list (map f v)).
>> 
>> However, it's no longer the same lemma, and it's awkward to use.
>> 
>> Presumably I'm missing something very obvious, but I'd be grateful for
>> suggestions.
>> 
>> Klaus
>> 
>> 
>> 
>> 
>> 
>