Remove the [ _ ] notations

They weren't extensively used and conflicted with too many things like primitive arrays or list notations. For instance, the following code was failing: ```Coq Require Import PArray Uint63. Check [|true; true | false|]. From Bignums Require Import BigN. Fail Check [|true; true | false|]. (* Error: Syntax error: [term level 200] expected after '[' (in [term]). *) ```
coq-community · Mar 15, 2023 · a410391 · a410391
1 parent def90f1
commit a410391
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 10 deletions.
diff --git a/BigN/BigN.v b/BigN/BigN.v
@@ -67,7 +67,6 @@ Notation "x < y < z" := (x<y /\ y<z) : bigN_scope.
 Notation "x < y <= z" := (x<y /\ y<=z) : bigN_scope.
 Notation "x <= y < z" := (x<=y /\ y<z) : bigN_scope.
 Notation "x <= y <= z" := (x<=y /\ y<=z) : bigN_scope.
-Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
 Infix "mod" := BigN.modulo (at level 40, no associativity) : bigN_scope.
 
 (** Example of reasoning about [BigN] *)
@@ -110,7 +109,7 @@ case Z.eqb_spec.
 BigN.zify. auto with zarith.
 intros NEQ.
 generalize (BigN.spec_div_eucl a b).
-generalize (Z_div_mod_full [a] [b] NEQ).
+generalize (Z_div_mod_full (BigN.to_Z a) (BigN.to_Z b) NEQ).
 destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r').
 intros (EQ,_). injection 1 as EQr EQq.
 BigN.zify. rewrite EQr, EQq; auto.

diff --git a/BigQ/BigQ.v b/BigQ/BigQ.v
@@ -73,7 +73,6 @@ Notation "x < y < z" := (x<y /\ y<z) : bigQ_scope.
 Notation "x < y <= z" := (x<y /\ y<=z) : bigQ_scope.
 Notation "x <= y < z" := (x<=y /\ y<z) : bigQ_scope.
 Notation "x <= y <= z" := (x<=y /\ y<=z) : bigQ_scope.
-Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope.
 
 (** [BigQ] is a ring *)
 
@@ -106,7 +105,7 @@ Lemma BigQpowerth :
  power_theory 1 BigQ.mul BigQ.eq Z.of_N BigQ.power.
 Proof.
 constructor. intros. BigQ.qify.
-replace ([r] ^ Z.of_N n)%Q with (pow_N 1 Qmult [r] n)%Q by (now destruct n).
+replace (BigQ.to_Q r ^ Z.of_N n)%Q with (pow_N 1 Qmult (BigQ.to_Q r) n)%Q by (now destruct n).
 destruct n. reflexivity.
 induction p; simpl; auto; rewrite ?BigQ.spec_mul, ?IHp; reflexivity.
 Qed.

diff --git a/BigZ/BigZ.v b/BigZ/BigZ.v
@@ -70,14 +70,13 @@ Notation "x < y < z" := (x<y /\ y<z) : bigZ_scope.
 Notation "x < y <= z" := (x<y /\ y<=z) : bigZ_scope.
 Notation "x <= y < z" := (x<=y /\ y<z) : bigZ_scope.
 Notation "x <= y <= z" := (x<=y /\ y<=z) : bigZ_scope.
-Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
 Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigZ_scope.
 Infix "÷" := BigZ.quot (at level 40, left associativity) : bigZ_scope.
 
 (** Some additional results about [BigZ] *)
 
 Theorem spec_to_Z: forall n : bigZ,
-  BigN.to_Z (BigZ.to_N n) = ((Z.sgn [n]) * [n])%Z.
+  BigN.to_Z (BigZ.to_N n) = (Z.sgn (BigZ.to_Z n) * BigZ.to_Z n)%Z.
 Proof.
 intros n; case n; simpl; intros p;
   generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
@@ -86,16 +85,16 @@ intros p1 H1; case H1; auto.
 Qed.
 
 Theorem spec_to_N n:
- ([n] = Z.sgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z.
+ (BigZ.to_Z n = Z.sgn (BigZ.to_Z n) * (BigN.to_Z (BigZ.to_N n)))%Z.
 Proof.
 case n; simpl; intros p;
   generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
 intros p1 H1; case H1; auto.
 intros p1 H1; case H1; auto.
 Qed.
 
-Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z ->
-  BigN.to_Z (BigZ.to_N n) = [n].
+Theorem spec_to_Z_pos: forall n, (0 <= BigZ.to_Z n)%Z ->
+  BigN.to_Z (BigZ.to_N n) = BigZ.to_Z n.
 Proof.
 intros n; case n; simpl; intros p;
   generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
@@ -139,7 +138,7 @@ case Z.eqb_spec.
 BigZ.zify. auto with zarith.
 intros NEQ.
 generalize (BigZ.spec_div_eucl a b).
-generalize (Z_div_mod_full [a] [b] NEQ).
+generalize (Z_div_mod_full (BigZ.to_Z a) (BigZ.to_Z b) NEQ).
 destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r').
 intros (EQ,_). injection 1 as EQr EQq.
 BigZ.zify. rewrite EQr, EQq; auto.