Not pretty-printing a field of a record

user_3780931 0
Viewed 58

Suppose I have such record type:

Record myRec : Type := {
  myNat : nat;
  myProof : myNat > 0
}.

How can I tell Coq to parse but not pretty-print (i.e., hide) the field myProof of a value of type myRec?

Can it be set while declaring the record type?

Or should it be done using the Notation command and the only printing syntax modifier?

coq
1 Answers

The way I would do it is indeed with notations.

Record myRec : Type := myRecBuild {
  myNat : nat ;
  myProof : myNat > 0
}.

Notation "⟪ x ⟫" := (myRecBuild x _).

Now if you have a value of myRec it will only print the relevant part.

Lemma foo :
  forall (x y : myRec),
    x.(myNat) = y.(myNat) ->
    x = x.
Proof.
  intros [x hx] [y hy] e.
  simpl in e. (* replaces myNat ⟪ x ⟫ with x *)
  (* Goal is now ⟪ x ⟫ = ⟪ x ⟫, hiding hx and hy *)
Abort.

I would argue that you don't need the only printing option. In fact, this can be handy if you want to easily provide the relevant part and leave the rest to automation / tactics.

Lemma bar :
  exists (x : myRec), x.(myNat) = 1.
Proof.
  unshelve eexists ⟪ 1 ⟫.
  - auto.
  - reflexivity.
Qed.

This can become particularly handy when using Program or Equations.

user_12759750
Related