The Coq mailing list

[Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>]

Thanks a lot for your very helpful reply, Dominique.

I also found out now that I didn't do my homework before asking on the
mailing list. The keyword seems to be "heterogenous equality". There's
a section in Chlipala's book on it, and there also seems to be a library
("Heq")
to help in such situations.

For a beginner, though, it's somewhat disconcerting that something that
seems to be as trivial and straightforward as the Lemma I wanted to prove
suddenly seems to open a huge can of quite advanced worms. Having to deal
with obscurly named concepts (like "John Major equality") isn't helping
either ;)
 
Klaus

Am 20/01/17 um 14:34 schrieb Dominique Larchey-Wendling:
> 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
>>
>>
>>
>>
>>