The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Matthieu,

 

I see. I thought they are primitive in the sense that they can just be beta reduced to the record field value, but not delta reduced to a let term. Let me see if Set Printing Projections and/or more careful evaluation solves the readability issues I have in proofs with larger records.

 

Thanks & best regards,

 

Michael

 

From: matthieu.sozeau AT gmail.com [mailto:matthieu.sozeau AT gmail.com] On Behalf Of Matthieu Sozeau
Sent: Friday, January 30, 2015 1:16 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Question on 8.5 primitive projections

 

Hi Michael,

 

   Primitive projections still obey the same reduction rules: delta to unfold it and beta/iota to reduce it, hence they have the unfolded form you witness. However simpl/cbn can recognize them easily and shouldn't ever expose this unfolded form unless you specifically do a delta reduction. Internally though, the projections are different terms and what you're seeing at the user level just hides the internal representation for compatibility. Also, you may want to Set Printing Projections.
Best,

-- Matthieu

Le vendredi 30 janvier 2015, Soegtrop, Michael <michael.soegtrop AT intel.com> a écrit :

Dear Coq users,

I really like the primitive projections feature, because the let terms to which projections expand sometimes make proof contexts with large records hard to understand. Just it doesn't work as I expected.

In the below sample:

        Set Primitive Projections.

        Record Test :=
        {
          a : unit;
          b : bool;
          c : nat
        }.

        Print a.

I get

        a = fun t : Test => let (a, _, _) := t in a : Test -> unit

I expected that the let term would go away and be replaced by the new primitive projection term. Also if I try

        Definition test := Build_Test tt false 0.
        Definition testa := test.(a).
        Eval cbv delta beta in testa.

I get

     = let (a, _, _) := {| a := tt; b := false; c := 0 |} in a
     : unit

I used the 8.5beta1 windows version.

Best regards,

Michael

--