The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Sorry, I may have misunderstood your question. Here are some observations that may be relevant:

Note that in the proof of the lemma "example" in my email, simpl won't  unfold the notation "0". To do that, you need to unfold

the definition canonical_names.zero, just as you would unfold any other definition. 

You can also control which definitions simpl unfolds:

https://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic143

In your style, Z0 was an abbreviation. I don't know how simpl's behavior on abbreviations can be customized.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Thu, Feb 9, 2017 at 9:44 AM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

An alternative is to have just one notation and to use the typeclass resolution machinery to resolve it to the appropriate instance, based on types.

MathClasses already defines typeclasses for the kind of notations you want.

http://www.cs.cornell.edu/~aa755/ROSCoq/coqdoc/MathClasses.interfaces.canonical_names.html#Zero

Here is your example rewritten in that style:

Require Import Utf8_core.

Require Import MathClasses.interfaces.canonical_names.

Open Scope mc_scope.

Notation "〈 a , b 〉" := (pair a b)

(no associativity).

Inductive ℕ := Zero : ℕ | Suc : ℕ → ℕ.

Global Instance ZeroN : canonical_names.Zero ℕ := Zero.

Global Instance OneN : canonical_names.One ℕ := (Suc 0).

(* 0, which is a notation for canonical_names.zero, is resolved to the 

latest typeclass

Instance of Zero in scope. If that is not the instance you want,

you need to help the typeclass resolution by providing casts (see below), 

or implicit arguments *)

Check 0.

Check Zero.

Check Suc Zero.

Notation ℤ := (ℕ * ℕ)%type.

Check (〈0,1〉).

Check (〈Zero, Suc Zero〉).

Notation "ℤ-1" := (〈0, 1〉 : ℤ).

Global Instance ZeroZ : canonical_names.Zero ℤ := 〈0, 0〉.

Global Instance OneZ : canonical_names.One ℤ := 〈1, 0〉.

Check 0.

Check (0:ℕ).

Global Instance EquivN ℕ : Equiv ℕ := (Coq.Init.Logic.eq).

Lemma example : ℤ-1 = ℤ-1 ∧ (0 = (0:ℤ)) ∧ 1 = (1:ℤ).

split;[|split]; reflexivity.

Admitted.

If you are new to typeclasses, you may want to first walk through some tutorial, e.g.

http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Thu, Feb 9, 2017 at 8:57 AM, Sebastian Böhne <boehne AT uni-potsdam.de> wrote:

Dear Coq-community!

We, Tim Richter and Sebastian Böhne, have problems with some notations we introduced for numbers in Coq. Sometimes an already introduced notation is ignored by Coq and -- even worse -- when processing in a proof our notations are replaced by their original versions. This is a big problem, since even simple contents become very confusing.

You find a minimal example below and attached.

Thank you very much for your help!

Best regards

Tim Richter and Sebastian Böhne

PS: We use CoqIde 8.4pl3.

----------------------------------

Require Import Utf8_core.

Notation "〈 a , b 〉" := (pair a b)
(no associativity).

Inductive ℕ := Zero : ℕ | Suc : ℕ → ℕ.

Notation ℕ0 := (Zero).
Notation ℕ1 := (Suc ℕ0).

Check ℕ0.
Check Zero.
Check Suc Zero.
(* Here Coq sticks correctly to notations and
furthermore retranslates objects, which can be
displayed as Notations *)

Notation ℤ := (ℕ * ℕ)%type.

Check (〈ℕ0,ℕ1〉).
Check (〈Zero, Suc Zero〉).
(* So Coq does not seem to have problems with
the pair notation *)

Notation ℤ0 := (〈ℕ0, ℕ0〉 : ℤ).
Notation ℤ1 := (〈ℕ1, ℕ0〉 : ℤ).
Notation "ℤ-1" := (〈ℕ0, ℕ1〉 : ℤ).

Check ℤ1.
(* Still like expected *)

Check (〈ℕ1, ℕ0〉).
(* Here Coq does not retranslate anymore *)

Check (〈ℕ1, ℕ0〉 : ℤ).
(* However, with some little help it still
 works *)

Lemma example : ℤ-1 = ℤ-1 ∧ ℤ0 = ℤ0 ∧ ℤ1 = ℤ1.
Proof.
simpl.
(* We did not even do anything but Coq
replaces our abbreviations with the longer
original versions. Why? *)
admit.
Admitted.

----------------------------------