不漂亮地打印记录的字段

Question

假设我有这样的记录类型：

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

我如何告诉 Coq 解析但不漂亮打印（即隐藏）myRec 类型值的字段 myProof？

可以在声明记录类型的时候设置吗？

还是应该使用 Notation 命令和 only printing 语法修饰符来完成？

Answer 1

我的做法确实是用符号。

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

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

现在，如果您的值为 myRec，它只会打印相关部分。

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.

我认为您不需要 only printing 选项。事实上，如果您想轻松提供相关部分并将其余部分留给自动化/策略，这会很方便。

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

这在使用 Program 或 Equations 时会变得特别方便。

不漂亮地打印记录的字段

Not pretty-printing a field of a record

coq