The Coq mailing list

[Carlos Simpson <Carlos.Simpson AT unice.fr>]

Dear Victor,
  As I think people have been saying for a while, you can only prove
that if you assume ``proof irrelevance'' which is an axiom stating
that for P:Prop, and any p,q:P, we have p=q. 
This of course corresponds to the way mathematicians usually think of 
propositions as being truth values; however, it isn't necessarily true in
Coq and indeed Voevodsky et.al.'s new interpretation of type theory 
uses exactly the idea that there could be many proofs of a proposition.

Your question about dependent records isn't such a bad question in and of
itself. In fact, in earlier versions of Coq say 10 years ago, the 
statements eq_rect were missing and you couldn't prove this property of
equality of dependent records; luckily that is an integral part of the system
now. Unfortunately, it's really a textbook case of ``the boy who cried wolf'':
you asked so many annoying questions before then without even trying to read 
the documentation or tutorials or the numerous books available on the 
subject, 
that nobody felt like explaining this carefully. 

---Carlos




Selon Victor Porton 
<porton AT narod.ru>:

> One more novice question:
> 
> Can we prove the following theorem as a consequence of equal_foo?
> 
> Theorem thm (u v : Foo): (a u = a v -> u = v).
> 
> 22.11.2011, 23:11, "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
> 
> -- 
> Victor Porton - http://portonvictor.org
>