Как иметь несколько обозначений "0" в Coq - PullRequest
Новая
       17

Как иметь несколько обозначений "0" в Coq

3 голосов
/ 19 мая 2019

Я определил аксиомы поля в Coq и использовал их для доказательства простых свойств, подобных описанным здесь . Затем я добавил аксиомы векторного пространства и доказал простые свойства там. Поскольку нотация 0 уже используется моим полем: 

(*******************)
(* Field notations *)
(*******************)
Notation "0" := zero.
Notation "1" :=  one.
Infix    "+" :=  add.
Infix    "*" :=  mul.

Я использовал несколько более уродливые обозначения для своего векторного пространства: 

(**************************)
(* Vector space notations *)
(**************************)
Notation "00" := zerov.
Notation "11" := onev.
Infix    "+_v" :=  addv (at level 50, no associativity).
Infix    "*_v" :=  mulv (at level 60, no associativity).

Что позволило доказать следующую простую лемму: 

Lemma mul_0_l: forall (v : V), (eqv (mulv 0 v) 00).

Когда я изменил "00" на "0V" (что красивее), все перестало работать, и я получил следующую ошибку: 

In environment
v : V
The term "0" has type "F" while it is expected to have type "V".

Есть ли способ использовать "0V"? или я застрял с "00"?

1 Ответ

2 голосов
/ 20 мая 2019

Мне удивительно, что токен, начинающийся с цифры, не распознается; Я открыл проблему с GitHub .Между тем, я полагаю, что ближайшая вещь, с которой вы можете работать, - это обозначение области видимости (хотя это на один символ длиннее): 

Section test.
  Variable T : Type.
  Variable zero : T.
  Notation "0" := zero.

  Variable V : Type.
  Variable zeroV : V.

  Notation "0" := zeroV : V_scope.
  Delimit Scope V_scope with V.
  Check 0.   (* 0 : T *)
  Check 0%V. (* 0%V : V *)

Редактировать

Как @JasonGross предлагает в комментарии,Вы можете Bind Scope использовать одну и ту же запись 0 для обоих типов T и V.Это может повлиять на читабельность в некоторых случаях. 

Section test.
  Variable T : Type.
  Variable zero : T.
  Notation "0" := zero.

  Variable V : Type.
  Variable zeroV : V.

  Notation "0" := zeroV : V_scope.
  Delimit Scope V_scope with V.
  Bind Scope V_scope with V.
  Check 0.   (* 0 : T *)
  Check 0%V. (* 0%V : V *)

  Variable mult : T -> V -> V.
  Check mult 0 0.   (* mult 0 0 : V *)
  Check mult 0 0%V. (* mult 0 0 : V *)
...