coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Andreas Abel <andreas.abel AT ifi.lmu.de>
- To: AUGER Cédric <sedrikov AT gmail.com>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] proj1 and proj2 opaque
- Date: Wed, 05 Dec 2012 18:44:59 -0500
On 05.12.12 4:32 AM, AUGER Cédric wrote:
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
+1
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).
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
- [Coq-Club] proj1 and proj2 opaque, AUGER Cédric, 12/05/2012
- Re: [Coq-Club] proj1 and proj2 opaque, Andreas Abel, 12/06/2012
Archive powered by MHonArc 2.6.18.