Блог

Главная - Вопросы по программированию - Некрасиво-печатать поле записи

Некрасиво-печатать поле записи

#coq

Вопрос:

Предположим, у меня есть такой тип записи:

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

Как я могу сказать Coq, чтобы он проанализировал, но не напечатал (т. Е. Не скрыл) поле myProof значения типа myRec ?

Можно ли его установить при объявлении типа записи?

Или это следует сделать с помощью Notation команды и модификатора only printing синтаксиса?

Ответ №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 .

Комментарии:

1. Но с вашим подходом, если у меня есть другие типы записей с полями для скрытия, мне нужно будет ввести разные обозначения для каждого типа записей. Я хотел бы использовать встроенную нотацию {| myNat := 1 |} .

2. Я не знаю, как это можно было бы сделать. В любом случае, вы должны указать его для каждой записи, так как теперь Coq сможет угадать, какие аргументы вы хотите видеть.

Метки: