The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

Dear Victor,

I have sent you a message like this one privately, but it did not
work, so I am going to say this publicly.

You are flooding the list with trivialities. In addition, your
messages are arrogant because you keep saying things like "Coq can't
compare dependent records" where in reality the source of trouble is
(in most cases) your ignorance. There is nothing wrong with being
ignorant, and we're happy to help, but not if you keep implying that
everyone on this list, the designers of Coq included, are so dumb that
they can't even get the basic things right and that the design
decisions made in Coq are obviously bad. (This _is_ what you are
implying, even if you are not aware of it.)

There is another source of help for beginners which might work better
for you, namely the IRC #coq channel irc://irc.freenode.net/#coq where
you can get help immediately.

Now, regarding comparison of dependent records:

>Theorem ax2: @v A = @v B.
>Proof.
> auto.
>Qed.

Here I get:

   The term "@v B" has type "@x B = 0" while it is expected to have
type  "@x A = 0".

What version of Coq are you using?

Anyhow, you can of course compare dependent records, but you must
transport the dependent component of one record along the proof of
equality so that things typecheck, i.e.:

-----
Parameter A : Type.
Parameter B : A -> Type.

Structure Foo := mkFoo { a : A; b : B a }.

Definition tran {u v : Foo} (p : a u = a v) : B (a u) -> B (a v).
Proof.
  induction p.
  auto.
Defined.

Lemma equal_foo (u v : Foo) (p : a u = a v) : tran p (b u) = b v -> u = v.
Proof.
  intro H.
  destruct u as [x y].
  destruct v as [s t].
  simpl in * |- *.
  destruct p.
  simpl in H.
  rewrite H.
  reflexivity.
Qed.
------

Lemma equal_foo says that the dependent records u and v are equal,
provided that their first components are equal, and the second
component of u is equal to the second component of v, after we have
converted it from type B (a u) to type B (a v) via the proof p of
equality a u = a v.

With kind regards,

Andrej