The Coq mailing list

[Victor Porton <porton AT narod.ru>]

20.11.2011, 18:07, "Andrej Bauer" 
<andrej.bauer AT andrej.com>:
> 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.)

I don't say that Coq design decisions are bad. I understand that Coq is built 
on a set of highly orthogonal principles. Following orthogonal principles is 
good.

But excuse me to ask one more dumb question with suspicion that in the 
current version of Coq there are some deficiency. If I don't ask, I can't be 
100% sure.

Dear Andrej Bauer, I've read your code (below) and I somehow understand 
(honestly not 100%) its idea. I am going to put it into real use.

But the question arises: Should I repeat it every time I introduces a 
dependent structure?

Can it be put into a coherent way for every dependent record I declare, 
allowing to not repeat the same proof each time?

I don't thing anything is wrong, just I am confused with this question/

> What version of Coq are you using?

8.3pl2

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

I repeat (a little modified for simplicity) code by Andrej Bauer:

[[[[
Parameter A : Set.
Parameter B : A -> Prop.

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.

(*Print tran.*)

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.

-- 
Victor Porton - http://portonvictor.org