The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

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/