CODEWITHSUNDEEP
coq
OrenIshShalom
OrenIshShalom

Reputation: 7102

How to have multiple notations of "0" in Coq

I have defined field axioms in Coq, and used them to prove simple properties like described here. Then, I added vector space axioms and proved simple properties there. Since the 0 notation has already been used by my field:

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

I used the somewhat uglier notations for my vector space:

(**************************)
(* 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).

Which allowed to prove the following simple lemma:

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

When I changed "00" to "0V" (which is prettier) everything stopped working, and I got the following error:

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

Is there anyway to use "0V"? or am I stuck with "00"?

Upvotes: 3

Views: 319

Answers (1)

Bubbler
Bubbler

Reputation: 982

2021 update: The linked issue has been fixed in the meantime, and you should be able to use "0V" (or any notation with leading digits) without problems.

It's surprising to me that a token starting with a numeral is not recognized; I opened a GitHub issue on it. Meanwhile, I believe the closest thing you can work with is a scope notation (though it's one character longer):

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 *)

Edit

As @JasonGross suggested in the comment, you can Bind Scope to use the same notation 0 for both types T and V. This might impact readability in some cases though.

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 *)

Upvotes: 2

Related Questions