The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

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