The Coq mailing list

[Sebastian Böhne <boehne AT uni-potsdam.de>]

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.

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

Attachment: Minimal_example.v
Description: application/verilog