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

(***************)
(* Section 2.1 *)
(***************)
Record flatNormSpace := FlatNormSpace {
  carrier : Type ;
  fminus : carrier -> carrier -> carrier;
  fnorm : carrier -> nat;
  fnormP : forall x : carrier, fnorm (fminus x x) = 0}.

Check fminus.
(* fminus : forall f : flatNormSpace,                         *)
(*   carrier f -> carrier f -> carrier f        *)
Check fnormP.
(* fnormP : forall (f : flatNormSpace) (x : carrier f), *)
(*   fnorm f (fminus f x x) = 0                           *)

Lemma Z_normP (n : Z) : Z.abs_nat (Z.sub n n) = 0.
Proof. by rewrite Z.sub_diag. Qed.
Definition Z_flatNormSpace := FlatNormSpace Z Z.sub Z.abs_nat Z_normP.

(***************)
(* Section 2.2 *)
(***************)
Record isModule T := IsModule {minus_op : T -> T -> T}.
Structure module := Module {
  module_carrier : Type ;
  module_isModule : isModule module_carrier}.

Definition minus {M : module} := minus_op _ (module_isModule M).
Notation "x - y" := (minus x y).

Definition Z_isModule : isModule Z := IsModule Z Z.sub.
Definition Z_module := Module Z Z_isModule.

Fail Check forall x y : Z, x - y = x - y.

Canonical Z_module.
Check forall x y : Z, x - y = x - y.
Print Canonical Projections.
(* the line Z <- module_carrier (Z_module) tries to solve *)
(* the equation `module_carrier ?M =?= Z`                 *)

(* begin omitted from the paper *)
Coercion module_carrier : module >-> Sortclass.
(* end omitted from the paper   *)

(***************)
(* Section 2.3 *)
(***************)
Record naiveNormMixin (T : module) := NaiveNormMixin {
  naive_norm_op  : T -> nat ;
  naive_norm_opP : forall x : T, naive_norm_op (x - x) = 0}.
Record isNaiveNormSpace (T : Type) := IsNaiveNormSpace {
  nbase : isModule T ;
  nmix  : naiveNormMixin (Module _ nbase)}.
Structure naiveNormSpace := NaiveNormSpace {
  naive_norm_carrier          :> Type;
  naive_normSpace_isNormSpace : isNaiveNormSpace naive_norm_carrier}.
Definition naive_norm {N : naiveNormSpace} :=
  naive_norm_op _ (nmix _ (naive_normSpace_isNormSpace N)).
Notation "| x |" := (naive_norm x).

Fail Check forall (N : naiveNormSpace) (x y : N), x - y = x - y.

(* With similar techniques as before,
  one can make automatic the search for a substructure *)
Canonical naiveNorm_isModule (N : naiveNormSpace) :=
  Module N (nbase _ (naive_normSpace_isNormSpace N)).
Check forall (N : naiveNormSpace) (x y : N), x - y = x - y.

(* begin omitted from the paper *)
Arguments IsNaiveNormSpace {_ _}.

Definition naive_normP (N : naiveNormSpace) (x : N) : |x - x| = 0.
Proof. exact: naive_norm_opP. Qed.
(* end omitted from the paper   *)

(***************)
(* Section 3.1 *)
(***************)
Record isBallSpace T     := IsBallSpace {
  ball_op  : T -> T -> Prop;
  ball_opP : forall x : T, ball_op x x}.
Structure ballSpace    := BallSpace {
  ball_carrier          :> Type;
  ballSpace_isBallSpace : isBallSpace ball_carrier}.
Definition ball {N : ballSpace} := ball_op _ (ballSpace_isBallSpace N).
Notation "x ~~ y" := (ball x y).

(* begin omitted from the paper *)
Definition ballP (B : ballSpace) (x : B) : x ~~ x.
Proof. exact: ball_opP. Qed.
(* end omitted from the paper *)

Section NaiveNormSpace_BallSpace.
Variable (N : naiveNormSpace).

(* The norm_ball definition should come with proofs of the axioms of
   the ball space structure in real life *)
Definition norm_ball (x : N) := fun y : N => |x - y| <= 1.

(* begin omitted from the paper *)
Lemma nnorm_ballP (x : N) : norm_ball x x.
Proof. by rewrite /norm_ball naive_normP; constructor. Qed.
Definition naiveNormSpace_isBallSpace :=
  IsBallSpace N norm_ball nnorm_ballP.
(* end omitted from the paper   *)
(* details about naiveNormSpace_isBallSpaceball omitted from the paper *)
Canonical nnorm_ballSpace := BallSpace N naiveNormSpace_isBallSpace.

End NaiveNormSpace_BallSpace.

(* begin omitted from the paper *)
Coercion nnorm_ballSpace :  naiveNormSpace >-> ballSpace.
(* end omitted from the paper *)

(**************************************************)
(* Paragraph "Problem with generic constructions" *)
(**************************************************)
(* Stability of module, ball space and norm space structures by product *)
Section ProdModule.
Variables (M M' : module).
Definition prod_minus (x y : M * M') := (fst x - fst y, snd x - snd y).
Definition prod_isModule             := IsModule (M * M') prod_minus.
Canonical  prod_Module               := Module   (M * M') prod_isModule.
End ProdModule.

Section ProdBallAndNorm.
Variables (B B' : ballSpace) (N N' : naiveNormSpace).

Definition prod_ball (x y : B * B') := fst x ~~ fst y /\ snd x ~~ snd y.
(* begin omitted from the paper *)
Lemma prod_ballP (x : B * B') : prod_ball x x.
Proof. by split; apply: ballP. Qed.
Definition prod_isBallSpace := IsBallSpace (B * B') prod_ball prod_ballP.
(* end omitted from the paper *)
(* definition of prod_isBallSpace omitted from the paper *)
Canonical prod_ballSpace := BallSpace (B * B') prod_isBallSpace.

Definition prod_nnorm (x : N * N') := max (|fst x|) (|snd x|).
(* begin omitted from the paper *)
Lemma prod_nnormP x : prod_nnorm (x - x) = 0.
Proof. by case: x => x x'; rewrite /prod_nnorm/= !naive_normP. Qed.
Definition prod_naiveNormMixin := NaiveNormMixin _ prod_nnorm prod_nnormP.
Definition prod_isNNSpace := IsNaiveNormSpace prod_naiveNormMixin.
(* end omitted from the paper *)
(* definition of prod_isNaiveNormSpace omitted from the paper *)
Canonical prod_naiveNormSpace := NaiveNormSpace (N * N') prod_isNNSpace.
End ProdBallAndNorm.

Variable P : forall {T}, (T -> Prop) -> Prop.
Example failure (Pball : forall V : naiveNormSpace, forall v : V, P (ball v))
  (W : naiveNormSpace) (w : W * W): P (ball w).
(* begin omitted from the paper *)
Fail have _ : exists (V : naiveNormSpace),
    nnorm_ballSpace V = prod_ballSpace (nnorm_ballSpace W) (nnorm_ballSpace W)
  by exists (prod_naiveNormSpace W W); reflexivity.
(* end omitted from the paper *)
Proof. Fail apply Pball. Abort.

(**********************************************************)
(* Paragraph "Problem with inference of ground instances" *)
(**********************************************************)
Lemma ball_is_nball (N : naiveNormSpace) (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.
(* begin omitted from the paper *)
Lemma Z_ballP n : Z_ball n n. Proof. by left. Qed.
Definition Z_isBallSpace := IsBallSpace _ Z_ball Z_ballP.
(* end omitted from the paper *)
(* definition of Z_isBallSpace omitted from the paper *)
Canonical Z_ballSpace := BallSpace Z Z_isBallSpace.

Definition Z_naiveNormMixin := NaiveNormMixin Z_module Z.abs_nat Z_normP.
Canonical Z_naiveNormSpace :=
   NaiveNormSpace Z (IsNaiveNormSpace Z_naiveNormMixin).

(* 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.
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 *)
Record normMixin (T : module) (m : isBallSpace T) := NormMixin {
  norm_op       : T -> nat;
  norm_opP      : forall x,   norm_op (x - x) = 0;
  norm_ball_opP : forall x y, ball_op _ m x y <-> (norm_op (x - y) <= 1)}.
Record isNormSpace (T : Type) := IsNormSpace {
  base : isModule T;
  bmix : isBallSpace T;
  mix  : normMixin (Module _ base) bmix }.
Structure normSpace := NormSpace {
  norm_carrier          :> Type;
  normSpace_isNormSpace : isNormSpace norm_carrier}.
Definition norm {N : normSpace} :=
  norm_op _ _ (mix _ (normSpace_isNormSpace N)).
Notation "| x |" := (norm x).

(* begin omitted from the paper *)
(* Inheritance of module structure, same as naiveNormSpace *)
Arguments IsNormSpace {_ _ _}.

Canonical module_of_normSpace (N : normSpace) :=
  Module _ (base _ (normSpace_isNormSpace N)).
Coercion module_of_normSpace : normSpace >-> module.

Definition normP (N : normSpace) (x : N) : |x - x| = 0.
Proof. exact: norm_opP. Qed.
(* end omitted from the paper *)

Canonical norm_ballSpace (N : normSpace) :=
  BallSpace N (bmix _ (normSpace_isNormSpace N)).

(************************************************************)
(* Begin omitted from the paper,                            *)
(* we redo all the examples of section 2.3 on product and Z *)
(* but now the diagrams commute.                            *)
(************************************************************)
Coercion norm_ballSpace : normSpace >-> ballSpace.

Lemma norm_ballP  (N : normSpace) (x y : N) : (x ~~ y) <-> |x - y| <= 1.
Proof. exact: norm_ball_opP. Qed.

(* Stability of norm space structure by product *)
Section ProdNorm.
Variables (N N' : normSpace).
Definition prod_norm (x : N * N') := max (|fst x|) (|snd x|).
Lemma prod_normP x : prod_norm (x - x) = 0.
Proof. by case: x => x x'; rewrite /prod_norm/= !normP. Qed.
Lemma prod_norm_ballP (x y : N * N') : x ~~ y <-> prod_norm (x - y) <= 1.
Proof.
by split => [[/= xy1 xy2]|/Nat.max_lub_iff[xy1 xy2]];
   [apply: Nat.max_lub|split]; apply/norm_ballP.
Qed.
Definition prod_normMixin :=
  NormMixin _ (prod_isBallSpace N N') prod_norm prod_normP prod_norm_ballP.
Definition prod_isNormSpace := IsNormSpace prod_normMixin.
Canonical prod_normSpace := NormSpace (N * N') prod_isNormSpace.
End ProdNorm.

Lemma Z_norm_ballP (m n : Z) : Z_ball m n <-> Z.abs_nat (m - n) <= 1.
Proof.
rewrite /Z_ball -Nat.leb_le -[m = n]Z.sub_move_0_r Z.add_comm -Z.sub_move_r.
rewrite -[(n - 1)%Z]Z.add_opp_l -Z.sub_move_r; split => [[->|[->|->]]|]//.
case: (m - n)%Z => [|p|p]//=; do ?tauto;
  by rewrite -[p in X in _ -> X]Pos2Nat.id; case: Pos.to_nat => [|[]]//; tauto.
Qed.

Definition Z_normMixin := NormMixin _ Z_isBallSpace
  Z.abs_nat Z_normP Z_norm_ballP.
Definition Z_isNormSpace := IsNormSpace Z_normMixin.
Canonical Z_normSpace : normSpace := NormSpace Z Z_isNormSpace.

(*The previous failures does not happen again *)
(* `x ~ y` and `|x - y| < 1` are not definitionally equal in general *)
Example success (x y : Z) : x ~~ y <-> |x - y| <= 1.
Proof.
now apply norm_ballP.
Restart.
rewrite -norm_ballP.
reflexivity.
Qed.

Example success' (Pball : forall V : normSpace, forall v : V, P (ball v))
   (W : normSpace) (w : W * W) : P (ball w).
Proof.
have _ : exists (V : normSpace),
    norm_ballSpace V =  prod_ballSpace (norm_ballSpace W) (norm_ballSpace W)
  by exists (prod_normSpace W W); reflexivity.
by apply Pball.
Qed.
(* End omitted from the paper *)

(*************************)
(* Paragraph "Factories" *)
(*************************)
Section NaiveNormFactory.
Variable (T : module) (m : naiveNormMixin T).

Definition fact_ball (x y : T) := naive_norm_op T m (x - y) <= 1.

Lemma fact_ballP (x : T) : fact_ball x x.
Proof. by rewrite /fact_ball (naive_norm_opP _ m); constructor. Qed.

Definition nNormMixin_isBallSpace := IsBallSpace T fact_ball fact_ballP.

(* begin omitted from the paper *)
Lemma fact_normP (x : T) : naive_norm_op T m (x - x) = 0.
Proof. by rewrite (naive_norm_opP _ m); constructor. Qed.

Lemma fact_norm_ballP x y : fact_ball x y <-> naive_norm_op T m (x - y) <= 1.
Proof. by []. Qed.
(* end omitted from the paper *)
(* details for fact_normP and fact_norm_ballP omitted from the paper *)
Definition nNormMixin_normMixin :=
  NormMixin T nNormMixin_isBallSpace (naive_norm_op T m)
            fact_normP fact_norm_ballP.

End NaiveNormFactory.
Coercion nNormMixin_isBallSpace : naiveNormMixin >-> isBallSpace.
Coercion nNormMixin_normMixin : naiveNormMixin >-> normMixin.

Canonical alt_Z_ballSpace := BallSpace Z Z_naiveNormMixin.
Canonical alt_Z_normSpace := NormSpace Z (IsNormSpace Z_naiveNormMixin).