1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
---------------------------------
-- Section 2.2                 --
-- isModule is in fact has_sub --
---------------------------------
-----------------
-- Section 2.3 --
-----------------
universe u
variables {α μ μ' β β' ν ν' η η' : Type u}
variables [has_sub μ] [has_sub μ']

class isNaiveNormSpace (ν : Type u) extends has_sub ν :=
  (norm : ν -> nat)
  (normP : ∀ x : ν, norm (x - x) = 0)

variables [isNaiveNormSpace ν] [isNaiveNormSpace ν']

def naive_norm (x : ν) := isNaiveNormSpace.norm x
notation |x| := naive_norm x
def naive_normP (x : ν) : |x - x| = 0 := isNaiveNormSpace.normP x

#check ∀ x y : ν, x - y = x - y

instance ℤ_isNaiveNormSpace : isNaiveNormSpace ℤ :=
  ⟨int.nat_abs, λ n, begin rw sub_self, apply int.nat_abs_zero end⟩

-----------------
-- Section 3.1 --
-----------------

class isBallSpace (β : Type u) :=
 (ball : β -> β -> Prop) (ballP : ∀ x : β, ball x x)

variables [isBallSpace β] [isBallSpace β']
def ball  (x y : β) : Prop := isBallSpace.ball x y
def ballP (x : β) := isBallSpace.ballP x
infix ~ := ball

instance nnorm_isBallSpace : isBallSpace ν := ⟨
  λ x y : ν, |x - y| ≤ 1, λ x,
  begin simp [naive_normP, nat.le_succ] end⟩

instance prod_has_sub : has_sub (μ × μ') :=
  ⟨λ ⟨x1, x2⟩ ⟨y1, y2⟩, (x1 - y1, x2 - y2)⟩

#check ∀ (x y : nat × nat), x - y = x - y

instance prod_isBallSpace : isBallSpace (β × β') := ⟨
  λ ⟨x1, x2⟩ ⟨y1, y2⟩, x1 ~ y1 ∧ x2 ~ y2,
  λ ⟨x1, x2⟩, begin split; apply ballP end⟩

instance prod_isNaiveNormSpace : isNaiveNormSpace (ν × ν') := ⟨
  λ ⟨x1, x2⟩, max ( |x1| ) ( |x2| ),
  λ ⟨x1, x2⟩, begin
    have: max ( |x1 - x1| ) ( |x2 - x2| ) = 0,
    {simp [naive_normP]}, {apply this}
  end⟩

variable P : ∀ {α : Type u}, (α → Prop) → Prop
-- failure 1
example
 (Pball : ∀ {α : Type u} [isNaiveNormSpace α] (v : α), P (ball v))
 (w : ν × ν) : P (ball w) := by apply Pball

lemma ball_is_norm_ball (x y : ℤ) : x ~ y = ( |x - y| ≤ 1 ) := rfl

example (x : ν) : |x - x| ≤ 1 := by apply (ballP x)

instance ℤ_isBallSpace : isBallSpace ℤ :=
  ⟨λ m n, m = n ∨ m = n + 1 ∨ m = n - 1, λ n, begin left, refl end⟩

-- failure 2
example (x y : ℤ) : x ~ y = ( |x - y| < 1 ) :=
  by apply ball_is_norm_ball

-----------------
-- Section 3.2 --
-----------------
-- INHERITANCE BY INCLUSION --
-- The mixin for normedspaces contains the compatibility with ballspaces --)
class isNormSpace (η : Type u) extends has_sub η, isBallSpace η :=
  (norm :  η -> ℕ)
  (normP : ∀ x : η, norm (x - x) = 0)
  (norm_ballP : forall x y, x ~ y ↔ norm (x - y) ≤ 1)

variables [isNormSpace η] [isNormSpace η']

def norm (x : η) := isNormSpace.norm x
notation |x| := norm x
def normP (x : η) : |x - x| = 0 := isNormSpace.normP x
def norm_ballP (x y : η) : x ~ y ↔ norm (x - y) ≤ 1 :=
  isNormSpace.norm_ballP x y

instance prod_isNormSpace : isNormSpace (η × η') := ⟨
  λ ⟨x1, x2⟩, max ( |x1| ) ( |x2| ),
  λ ⟨x1, x2⟩, begin
    have: max ( |x1 - x1| ) ( |x2 - x2| ) = 0,
      {simp [normP]}, {apply this}
  end,
  λ ⟨x1, x2⟩ ⟨y1, y2⟩, begin
    have: x1 ~ y1 ∧ x2 ~ y2 ↔ max ( |x1 - y1| ) ( |x2 - y2| ) ≤ 1,
      {simp [norm_ballP], split,
        {intro H; cases H; apply max_le; assumption},
        {intro H, split; apply (le_trans _ H),
          {apply le_max_left}, {apply le_max_right}}
      }, {apply this}
  end⟩

-- success 1
example
 (Pball : ∀ {α : Type u} [isNormSpace α] (v : α), P (ball v))
 (w : η × η) : P (ball w) := by apply Pball

instance ℤ_isNormSpace : isNormSpace ℤ := ⟨
  int.nat_abs,
  λ n, begin rw sub_self, apply int.nat_abs_zero end,
  λ m n, begin
    calc m ~ n ↔ m = n ∨ m = n + 1 ∨ m = n - 1 : by refl
           ... ↔ m - n = 0 ∨ m - n = 1 ∨ m - n = - 1 : sorry
           ... ↔ int.nat_abs (m - n) ≤ 1 : sorry
  end⟩

-- success 2
example (x y : ℤ) : x ~ y ↔ ( norm (x - y) ) ≤ 1 :=
  by apply norm_ballP