Skip to Content.
Sympa Menu

coq-club - [Coq-Club] proj1 and proj2 opaque

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] proj1 and proj2 opaque


Chronological Thread 
  • From: AUGER Cédric <sedrikov AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] proj1 and proj2 opaque
  • Date: Wed, 5 Dec 2012 10:32:54 +0100

Hi all, is there any reason to have proj1 and proj2 opaque?

I do not really see the point in doing so.
Making them transparent wouldn't break proof-irrelevance, and would
allow simplifications where conj is involved.

Maybe I shouldn't do some computation inside of Prop, but really I do
not understand why forbiding "proj1 (conj a b)" to reduce to "a".

Plus, in the source code,

Theorem proj1 : A /\ B -> A.
Proof.
destruct 1; trivial.
Qed.

use of tactics here could be considered as obfuscation, it is longer to
write than direct access and less evident.

Record and (A B : Prop) : Prop := conj { proj1 : A; proj2 : B }.

Would be a lot more compact.

I was pretty sure, that "proj1 (conj a b)" used to reduce to "a" (with
a transparent definition of proj1 of course).



Archive powered by MHonArc 2.6.18.

Top of Page