imandra-100-theorems/src/tri_ineq.iml at main · imandra-ai/imandra-100-theorems · GitHub

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
(* Triangle inequality in Imandra, over R^2.
   Theorem 91 of the 100 Theorems list.

   Grant Passmore, Imandra
 *)

module R2 = struct

  type vec = { x: real; y: real }

  let add (u:vec) (v:vec) : vec = Real.({ x = u.x + v.x; y = u.y + v.y })
  let dot (u:vec) (v:vec) : real = Real.(u.x * v.x + u.y * v.y)
  let norm (u:vec) : real = dot u u

end

lemma cauchy_schwarz_sq (u:R2.vec) (v:R2.vec) =
  let open Real in
  R2.(dot u v * dot u v <= norm u * norm v)
[@@by auto]

(* Expand ((a+b)^2 + (c+d)^2) into squares + 2(ab+cd). *)
lemma sumsq_expand_2x2 (a:real) (b:real) (c:real) (d:real) =
  ((a +. b) *. (a +. b) +. (c +. d) *. (c +. d))
  =
  ((a *. a +. c *. c) +. (b *. b +. d *. d))
  +. (2.0 *. (a *. b +. c *. d))
[@@by nonlin ()]

lemma regroup_square (a:real) (b:real) =
  (((a *. a) *. b) *. b) = ((a *. a) *. (b *. b))
[@@by auto]

(* (a^2)(b^2) = (ab)^2 *)
lemma sq_mul_sq (a:real) (b:real) =
  ((a *. a) *. (b *. b)) = ((a *. b) *. (a *. b))
[@@by auto]

(* a >= 0 /\ b >= 0 ==> a*b >= 0 *)
lemma prod_nonneg (a:real) (b:real) =
  a >=. 0.0 && b >=. 0.0 ==> a *. b >=. 0.0
[@@by auto]

lemma diff_of_squares (a:real) (b:real) =
  ((b +. (-1.0 *. a)) *. (b +. a)) = ((b *. b) +. (-1.0 *. (a *. a)))
[@@by auto]

lemma sum_nonneg_eq_zero_implies_both_zero (a:real) (b:real) =
  (a >=. 0.0 && b >=. 0.0 && a +. b = 0.0) ==> (a = 0.0 && b = 0.0)
[@@by auto]

(* a^2 <= b^2 /\ b >= 0 ==> a <= b. *)
lemma le_of_sq_le_nonneg_rhs (a:real) (b:real) =
  b >=. 0.0 && (a *. a) <=. (b *. b) ==> a <=. b
[@@by intros
   @> [%cases a <=. 0.0]
   @>| [auto;
        [%use prod_nonneg a a]
        @> [%use diff_of_squares a b]
        @> [%use sum_nonneg_eq_zero_implies_both_zero a b]
        @> nonlin ()]]

(* s^2 <= (nx^2)(ny^2) with nx,ny >= 0 ==> s <= nx*ny. *)
lemma cs_upper_from_sq (s:real) (nx:real) (ny:real) =
  nx >=. 0.0 && ny >=. 0.0 &&
  (s *. s) <=. ((nx *. nx) *. (ny *. ny))
  ==> s <=. nx *. ny
[@@by intros
  @> [%use regroup_square nx ny]
  @> [%use sq_mul_sq nx ny]
  @> simplify ()
  (* get nx*ny >= 0 from guards *)
  @> [%use prod_nonneg nx ny]
  (* unsquare: s^2 ≤ (nx*ny)^2 ∧ nx*ny >= 0 ==> s <= nx*ny *)
  @> [%use le_of_sq_le_nonneg_rhs s (nx *. ny)]
  @> auto]

(* S <= A·B ==> A^2 + B^2 + 2S <= (A+B)^2. *)
lemma add_bound_from_middle (a:real) (b:real) (s:real) =
  s <=. a *. b ==> (a *. a +. b *. b +. 2.0 *. s) <=. (a +. b) *. (a +. b)
[@@by auto]

lemma sum_nonneg (nx:real) (ny:real) =
  nx >=. 0.0 && ny >=. 0.0 ==> nx +. ny >=. 0.0
[@@by auto]

(* The Triangle Inequality over R^2! *)

theorem triangle_inequality (x:R2.vec) (y:R2.vec) (nx:real) (ny:real) (nxy:real) =
  let open Real in
  let open R2 in
  nx >= 0.0 && ny >= 0.0 && nxy >= 0.0 &&
  nx * nx = norm x && ny * ny = norm y && nxy * nxy = norm (add x y)
  ==> nxy <= nx + ny
[@@by
  [%simp_only R2.add, R2.dot, R2.norm]
  @>>|
    [%use cauchy_schwarz_sq x y]
    @> [%use sumsq_expand_2x2 x.x y.x x.y y.y]
    @> [%use cs_upper_from_sq ((x.x *. y.x) +. (x.y *. y.y)) nx ny]
    @> [%use add_bound_from_middle nx ny ((x.x *. y.x) +. (x.y *. y.y))]
    @> [%use sum_nonneg nx ny]
    @> [%use le_of_sq_le_nonneg_rhs nxy (nx +. ny)]
    @> simplify ()
    @> nonlin()
]