examples/logic/lagrange_inequality.why

   1
   2 (** {1 Lagrange Identity, Cauchy-Schwarz and Triangle Inequalities} *)
   3
   4 theory LagrangeInequality
   5
   6 (*
   7
   8 sum_squares a  \times sum_squares b = (scalar product a.b)^2 +
   9
  10 sum {1 <= i <j <=n} (a_i b_j - a_j b_i)^2
  11 *)
  12
  13   use real.Real
  14   use real.Square
  15
  16   (** dot product, a.k.a. scalar product, of two vectors *)
  17   function dot (x1:real) (x2:real) (y1:real) (y2:real) : real =
  18      x1*y1 + x2*y2
  19
  20   (** square of the norm of a vector *)
  21   function norm2 (x1:real) (x2:real) : real =
  22      sqr x1 + sqr x2
  23
  24   (** square of the norm is non-negative *)
  25   lemma norm2_pos :
  26      forall x1 x2:real. norm2 x1 x2 >= 0.0
  27
  28
  29   lemma Lagrange :
  30     forall a1 a2 b1 b2 : real .
  31        norm2 a1 a2 * norm2 b1 b2 = sqr (dot a1 a2 b1 b2) + sqr (a1 * b2 - a2 * b1)
  32
  33 end
  34
  35
  36 theory CauchySchwarzInequality
  37
  38
  39   use real.Real
  40   use real.Square
  41   use LagrangeInequality
  42
  43   lemma CauchySchwarz_aux:
  44      forall x1 x2 y1 y2 : real.
  45         sqr (dot x1 x2 y1 y2) <= norm2 x1 x2 * norm2 y1 y2
  46
  47   (** norm of a vector *)
  48   function norm (x1:real) (x2:real) : real = sqrt (norm2 x1 x2)
  49
  50   (** norm is non-negative *)
  51   lemma norm_pos :
  52      forall x1 x2:real. norm x1 x2 >= 0.0
  53
  54   (** 2 lemmas to help the next one *)
  55   lemma sqr_le_sqrt :
  56     forall x y:real. sqr x <= y -> x <= sqrt y
  57
  58   lemma CauchySchwarz:
  59      forall x1 x2 y1 y2 : real.
  60         dot x1 x2 y1 y2 <= norm x1 x2 * norm y1 y2
  61
  62 end
  63
  64
  65 theory TriangleInequality
  66
  67   use real.Real
  68   use real.Square
  69   use LagrangeInequality
  70   use CauchySchwarzInequality
  71
  72 (** Triangle inequality, proved thanks to
  73   ||x+y||² = ||x||² + 2<x,y> + ||y||²
  74            <= ||x||² + 2||x||*||y|| + ||y||²
  75            = (||x|| + ||y||)²
  76 *)
  77
  78   lemma triangle_aux :
  79     forall x1 x2 y1 y2 : real.
  80       norm2 (x1+y1) (x2+y2) <= sqr (norm x1 x2 + norm y1 y2)
  81       by norm2 (x1+y1) (x2+y2) = norm2 x1 x2 + 2.0 * dot x1 x2 y1 y2 + norm2 y1 y2
  82         <= norm2 x1 x2 + 2.0 * norm x1 x2 * norm y1 y2 + norm2 y1 y2
  83         = sqr (norm x1 x2 + norm y1 y2)
  84
  85   (* lemma to help the next one *)
  86   lemma sqr_sqrt_le :
  87     forall x y:real. 0.0 <= y /\ 0.0 <= x <= sqr y -> sqrt x <= y
  88
  89   lemma triangle :
  90     forall x1 x2 y1 y2 : real.
  91       norm (x1+y1) (x2+y2) <= norm x1 x2 + norm y1 y2
  92
  93 end