From Coq Require Import ssreflect ZArith.
Reserved Notation "| x |"   (at level 30).
Reserved Notation  "x ~~ y" (at level 30).

(***************)
(* Section 2.2 *)
(***************)
Class isModule (T : Type) := IsModule {minus : T -> T -> T}.
Hint Mode isModule ! : typeclass_instances.
Arguments IsModule {_}.
Arguments minus {_ _}.
Notation "x - y" := (minus x y).

Definition Z_isModule : isModule Z := IsModule Z.sub.
Fail Goal forall x y : Z, x - y = x - y.

Existing Instance Z_isModule.
Goal forall x y : Z, x - y = x - y. Abort.

Print HintDb typeclass_instances.
(* For isModule (modes !) ->   exact Z_isModule(level 0, pattern isModule Z, id 0) *)

(***************)
(* Section 2.3 *)
(***************)
Class isNaiveNormSpace (T : Type) := IsNaiveNormSpace {
  normSpace_isModule :> isModule T;
  naive_norm         : T -> nat;
  naive_normP        : forall x : T, naive_norm (x - x) = 0}.
Hint Mode isNaiveNormSpace ! : typeclass_instances.
Arguments IsNaiveNormSpace {_ _}.
Arguments naive_norm {_ _}.
Arguments naive_normP {_ _}.
Notation "| x |":= (naive_norm x).

Check forall N `{isNaiveNormSpace N} (x y : N), x - y = x - y.

Lemma Z_normP (n : Z) : Z.abs_nat (Z.sub n n) = 0.
Proof. by rewrite Z.sub_diag. Qed.
Instance Z_isNaiveNormSpace : isNaiveNormSpace Z :=
  IsNaiveNormSpace Z.abs_nat Z_normP.

(***************)
(* Section 3.1 *)
(***************)
Class isBallSpace (T : Type) := IsBallSpace {
  ball  : T -> T -> Prop;
  ballP : forall x : T, ball x x}.
Hint Mode isBallSpace ! : typeclass_instances.
Arguments IsBallSpace {_}.
Arguments ball {_ _}.
Arguments ballP {_ _}.
Notation "x ~~ y" := (ball x y).

Definition nnorm_ball {N} `{isNaiveNormSpace N} (x : N) :=
   fun y : N => |x - y| <= 1.
Program Instance nnorm_isBallSpace {N} `{isNaiveNormSpace N} : isBallSpace N :=
  IsBallSpace nnorm_ball _.
Next Obligation. by rewrite /nnorm_ball naive_normP; constructor. Qed.

(**************************************************)
(* Paragraph "Problem with generic constructions" *)
(**************************************************)
(* Stability of module, ball space and norm space structures by product *)
Definition prod_minus {M M'} `{isModule M, isModule M'} (x y : M * M') :=
   (fst x - fst y, snd x - snd y).
Program Instance prod_isModule {M M'} `{isModule M, isModule M'} :
   isModule (M * M') := IsModule prod_minus.

Definition prod_ball {B B'} `{isBallSpace B, isBallSpace B'} (x y : B * B') :=
   fst x ~~ fst y /\ snd x ~~ snd y.
Program Instance prod_isBallSpace {B B'} `{isBallSpace B, isBallSpace B'} :
  isBallSpace (B * B') := IsBallSpace prod_ball _.
Next Obligation. by split; apply: ballP. Qed.

Definition prod_nnorm {N N'} `{isNaiveNormSpace N, isNaiveNormSpace N'}
  (x : N * N') := max (|fst x|) (|snd x|).
Program Instance prod_isNNSpace {N N'}
  `{isNaiveNormSpace N, isNaiveNormSpace N'} :
  isNaiveNormSpace (N * N') := IsNaiveNormSpace prod_nnorm _.
Next Obligation. by rewrite /prod_nnorm/= !naive_normP. Qed.

(* This the same failure as with typeclasses *)
Variable P1 : forall {T : Type}, (T -> Prop) -> Prop.
Variable P2 : forall {T : Type}, (T -> Prop) -> Prop.
Set Typeclasses Debug.
Example failure
  (Pball1 : forall {V} `{isNaiveNormSpace V}, forall v : V, P1 (ball v))
  (Pball2 : forall {V} `{isBallSpace V}, forall v : V * V, P2 (ball v))
  {W} `{isNaiveNormSpace W} (w : W * W) :  P1 (ball w) /\ P2 (ball w).
Proof.
Set Typeclasses Debug.
Set Printing All.
split. (* only one of them can be true, and depends on typeclass priorities *)
- by apply Pball1.
- Fail by apply Pball2.
Unset Typeclasses Debug.
Unset Printing All.
Abort.

(**********************************************)
(* Paragraph "Problem inference of instances" *)
(**********************************************)
Lemma ball_is_nball N `{isNaiveNormSpace N} (x y : N) :
  ball x y <-> |x - y| <= 1.
Proof. reflexivity. Qed.

Definition Z_ball (m n : Z) := (m = n \/ m = n + 1 \/ m = n - 1)%Z.
Lemma Z_ballP n : Z_ball n n. Proof. by left. Qed.
Instance Z_isBallSpace : isBallSpace Z := IsBallSpace Z_ball Z_ballP.

(* Now two instances of ballSpace exist on Z:                   *)
(* the canonical ballSpace of a naiveNormSpace and Z_ballSpace. *)
(* As a consequence, even if Z is an an instance of normSpace,  *)
(* we cannot use ball_is_nball. *)
Example failure (x y : Z) : x ~~ y <-> |x - y| <= 1.
Proof.
Fail apply ball_is_nball. (* !!! *)
rewrite -ball_is_nball.
(* the goal is: x ~ y <-> x ~ y *)
Fail reflexivity. (* !!! *)
Abort.

(***************)
(* Section 3.2 *)
(***************)
(*INHERITANCE BY INCLUSION*)
(*The mixin for normedspaces contains the compatibility with ballspaces *)
Class isNormSpace (T : Type) := IsNormSpace {
  base :> isModule T;
  bmix :> isBallSpace T; (*New: inheritance of ball space by inclusion *)
  norm :  T -> nat;
  normP : forall x : T, norm (x - x) = 0;
  norm_ballP : forall x y, x ~~ y <-> norm (x - y) <= 1 (* New: compatibility condition *)
}.
Hint Mode isNormSpace ! : typeclass_instances.
Arguments IsNormSpace {T _ _}.
Arguments norm {_ _}.
Notation "| x |":= (norm x) (at level 30).

(* Stability of norm space structure by product *)
Definition prod_norm {N N'} `{isNormSpace N, isNormSpace N'} (x : N * N') :=
   max (|fst x|) (|snd x|).
Program Instance prod_isNormSpace {N N'} `{isNormSpace N, isNormSpace N'} :
  isNormSpace (N * N') := IsNormSpace prod_norm _ _.
Next Obligation. by rewrite /prod_norm/= !normP. Qed.
Next Obligation.
by split => [[/= xy1 xy2]|/Nat.max_lub_iff[xy1 xy2]];
   [apply: Nat.max_lub|split]; apply/norm_ballP.
Qed.

(* This the same failure as with typeclasses *)
Example success
  (Pball1 : forall {V} `{isNormSpace V}, forall v : V, P1 (ball v))
  (Pball2 : forall {V} `{isBallSpace V}, forall v : V * V, P2 (ball v))
  {W} `{isNormSpace W} (w : W * W) :  P1 (ball w) /\ P2 (ball w).
Proof.
Set Typeclasses Debug.
Set Printing All.
split.
- by apply Pball1.
- by apply Pball2.
Unset Typeclasses Debug.
Unset Printing All.
Abort.

Program Instance Z_isNormSpace : isNormSpace Z := IsNormSpace Z.abs_nat _ _.
Next Obligation. by rewrite Z.sub_diag. Qed.
Next Obligation.
rewrite /Z_ball -Nat.leb_le -[x = y]Z.sub_move_0_r Z.add_comm -Z.sub_move_r.
rewrite -[(y - 1)%Z]Z.add_opp_l -Z.sub_move_r; split => [[->|[->|->]]|]//.
case: (x - y)%Z => [|p|p]//=; do ?tauto;
  by rewrite -[p in X in _ -> X]Pos2Nat.id; case: Pos.to_nat => [|[]]//; tauto.
Qed.

(*The previous failures does not happen again *)
(* `x ~ y` and `|x - y| < 1` are not definitionally equal in general *)
Example semi_success (x y : Z) : x ~~ y <-> |x - y| <= 1.
Proof.
rewrite -norm_ballP. (* sucess *)
reflexivity.
Restart.
simpl.
Fail apply norm_ballP. (* unexpected failure *)
Fail rewrite norm_ballP. (* unexpected failure *)
Abort.