examples/kleene_algebra.mlw

   1 (** {1 Kleene Algebra Definition and Relational Kleene Algebra }
   2
   3 Author: Quentin Garchery (Université Paris-Saclay)
   4 *)
   5
   6 module SemiRing
   7
   8   use int.Int
   9
  10   type t
  11   constant zero : t
  12   constant one : t
  13   function (+) t t : t
  14   function (*) t t : t
  15
  16   clone export algebra.CommutativeMonoid with type t = t, constant unit = zero,
  17   function op = (+), axiom .
  18
  19   clone algebra.Monoid with type t = t, constant unit = one,
  20   function op = (*), axiom .
  21
  22   axiom Mul_zero_l : forall x. zero * x = zero
  23   axiom Mul_zero_r : forall x. x * zero = zero
  24
  25   axiom Mul_distr_l : forall x y z : t. x * (y + z) = x * y + x * z
  26   axiom Mul_distr_r : forall x y z : t. (y + z) * x = y * x + z * x
  27
  28   let rec ghost function (^) (x : t) (n : int) : t
  29     requires { n >= 0 }
  30     variant { n }
  31   =
  32     if n = 0 then pure{one} else let r = x ^ (n-1) in pure {x * r}
  33
  34   clone int.Exponentiation with type t = t, constant one = one,
  35   function (*) = (*), function power = (^), lemma .
  36 end
  37
  38
  39 module Dioid
  40
  41   clone export SemiRing with axiom .
  42
  43   axiom Idem : forall x : t. x + x = x
  44
  45   predicate (<=) (x : t) (y : t) = x + y = y
  46
  47   lemma le_refl : forall x. x <= x
  48
  49   lemma le_antisym : forall x y. x <= y -> y <= x -> x = y
  50
  51   lemma le_trans : forall x y z. x <= y -> y <= z -> x <= z
  52
  53   lemma zero_le : forall x. zero <= x
  54
  55   lemma le_compat_add : forall x y z. x <= y -> x + z <= y + z
  56
  57   lemma le_add : forall x y. x <= x + y
  58
  59   lemma le_add_le : forall x y z. x <= z -> y <= z -> x + y <= z
  60
  61   lemma add_le : forall x y z. x + y <= z -> x <= z
  62
  63   lemma le_compat_add_left : forall x y z. x <= y -> z * x <= z * y
  64
  65   lemma le_compat_add_right : forall x y z. x <= y -> x * z <= y * z
  66 end
  67
  68
  69 module KleeneAlgebra
  70
  71   use int.Int
  72
  73   clone export Dioid with axiom .
  74
  75   (* We denote x^* as !x *)
  76   function (!_) t : t
  77
  78   axiom Star_unfold_left : forall x. one + x * !x <= !x
  79
  80   axiom Star_unfold_right : forall x. one + !x * x <= !x
  81
  82   axiom Star_induct_left : forall x y z. z + x * y <= y -> !x * z <= y
  83
  84   axiom Star_induct_right : forall x y z. z + y * x <= y -> z * !x <= y
  85
  86   lemma one_le_star : forall x. one <= !x
  87
  88   lemma mul_var_le_star : forall x. x * !x <= !x
  89
  90   lemma var_mul_le_star : forall x. !x * x <= !x
  91
  92   lemma power_le_star : forall i x. i >= 0 -> x ^ i <= !x
  93
  94   lemma star_mul_star : forall x. !x * !x = !x
  95   by !x + x * !x <= ! x
  96
  97   lemma star_star : forall x. !(!x) = !x
  98
  99   lemma star_unfold_left : forall x. one + x * !x = !x
 100   by one + x * (one + x * !x) <= one + x * !x
 101
 102   lemma star_unfold_right : forall x. one + !x * x = !x
 103   by one + (one + !x * x) * x <= one + !x * x
 104
 105   lemma star_le : forall x y. x <= y -> !x <= !y
 106   by one + x * !y <= !y
 107
 108   lemma le_star_left_right : forall x y z. z * x <= y * z -> z * !x <= !y * z
 109   by z + (!y * z) * x <= !y * z
 110
 111   lemma le_star_right_left : forall x y z. x * z <= z * y -> !x * z <= z * !y
 112   by z + x * (z * !y) <= z * !y
 113
 114   lemma slide_left : forall x y. !(x + y) = !x * !(y * !x)
 115   by !x <= !(x + y)
 116   so y * !x <= !(x + y)
 117   so !(y * !x) <= !(!(x + y)) <= !(x + y)
 118   so !x * !(y * !x) <= !(x + y)
 119   so one + (x + y) * (!x * !(y * !x)) <= !x * !(y * !x)
 120   so !(x + y) <= !x * !(y * !x)
 121
 122   lemma slide_right : forall x y. !(x + y) = !(!x * y) * !x
 123   by !x <= !(x + y)
 124   so !x * y <= !(x + y)
 125   so !(!x * y) <= !(!(x + y)) <= !(x + y)
 126   so !(!x * y) * !x <= !(x + y)
 127   so one + (!(!x * y) * !x) * (x + y) <= !(!x * y) * !x
 128   so !(x + y) <= !(!x * y) * !x
 129
 130   (** Conway's equality: a way to cut x^* in slices of size x^n *)
 131
 132   let rec ghost function sum_pow (x : t) (a b: int) : t
 133     requires { b >= a >= 0 }
 134     variant { b - a }
 135   = if b = a then pure{zero} else
 136     let m1 = sum_pow x a (b - 1) in
 137     let m2 = x ^ (b - 1) in
 138     pure {m1 + m2}
 139
 140   lemma sum_pow_left: forall x a b.
 141     b > a >= 0 ->
 142     sum_pow x a b = x^a + sum_pow x (Int.(+) a 1) b
 143
 144   lemma mul_sum_pow: forall x a b.
 145     b >= a >= 0 ->
 146     sum_pow x a b * x = sum_pow x (Int.(+) a 1) (Int.(+) b 1)
 147
 148   lemma sum_pow_le_star: forall x a b.
 149     b >= a >= 0 ->
 150     sum_pow x a b <= !x
 151
 152   lemma Conway_equality: forall x n.
 153     n >= 1 ->
 154     !x = !(x^n) * sum_pow x 0 n
 155   by !(x^n) * sum_pow x 0 n <= !x
 156   so !(x^n) * sum_pow x 0 n * x = !(x^n) * sum_pow x 1 n + !(x^n) * x ^ n
 157                                 <= !(x^n) * sum_pow x 0 n
 158   so one + !(x^n) * sum_pow x 0 n * x <= !(x^n) * sum_pow x 0 n
 159 end
 160
 161
 162 module RelAlgebra
 163
 164   use int.Int
 165
 166   use set.Set
 167
 168   (* Relational Algebra: sets of pairs of the same type *)
 169
 170   type a
 171
 172   type t = set (a, a)
 173
 174   (** Specify zero, one, +, * and ! in terms of membership *)
 175
 176   constant zero : t = empty
 177   lemma zero_def : forall x. not mem x zero
 178
 179   constant one : t = map (fun a -> (a, a)) all
 180   lemma one_def : forall x : a. mem (x, x) one
 181
 182   let ghost function post (s : t) (x : a)
 183     ensures { forall y. mem y result <-> mem (x, y) s }
 184   =
 185     map (fun p -> let (_, a2) = p in a2)
 186     (filter s (fun p -> let (a1, _) = p in pure{a1 = x}))
 187
 188   let ghost function pre (s : t) (y : a)
 189     ensures { forall x. mem x result <-> mem (x, y) s }
 190   =
 191     map (fun p -> let (a1, _) = p in a1)
 192     (filter s (fun p -> let (_, a2) = p in pure {a2 = y}))
 193
 194   let ghost function (+) (s1 s2 : t)
 195     ensures { forall x. mem x result <-> mem x s1 \/ mem x s2 }
 196   =
 197     union s1 s2
 198
 199   let ghost function (*) (s1 s2 : t)
 200     ensures { forall a1 a2. mem (a1, a2) result <->
 201                             exists x. mem (a1, x) s1 /\ mem (x, a2) s2 }
 202   =
 203     filter all
 204     (fun p -> let (a1, a2) = p in
 205     not (disjoint (post s1 a1) (pre s2 a2)))
 206
 207   lemma unit_l : forall x. one * x = x
 208   (*by one * x == x*)
 209
 210   lemma unit_r : forall x. x * one = x
 211   (*by x * one == x*)
 212
 213   lemma assoc_mul : forall x y z. x * y * z = x * (y * z)
 214   by forall e. (mem e (x * y * z) -> mem e (x * (y * z))) /\
 215                (mem e (x * (y * z)) -> mem e (x * y * z))
 216
 217   clone Dioid with type t = t, constant zero = zero,
 218   constant one = one, function (+) = (+), function (*) = (*), lemma .
 219
 220   lemma le_mem : forall x y. x <= y <-> forall u. mem u x -> mem u y
 221
 222   inductive in_star t (a, a) =
 223    | Star_0 : forall x s. in_star s (x, x)
 224    | Star_s : forall x y z s. in_star s (x, y) -> mem (y, z) s -> in_star s (x, z)
 225
 226   let ghost function (!_) (s : t) =
 227       filter all (in_star s)
 228
 229   lemma power_in_star : forall s : t, i, p : (a, a).
 230         i >= 0 -> mem p (s ^ i) -> mem p !s
 231         by i > 0 -> let (x, z) = p in
 232            exists y. (in_star s (x, y) by mem (x, y) (s ^ (i-1)))  /\ mem (y, z) s
 233
 234   lemma star_in_power : forall s x y.
 235         in_star s (x, y) -> (exists i. i >= 0 /\ mem (x, y) (s ^ i))
 236
 237   lemma star_spec : forall s : t, p : (a, a).
 238         mem p !s <-> exists i. i >= 0 /\ mem p (s ^ i)
 239
 240   lemma star_unfold_l : forall x u. mem u (one + x * !x) -> mem u !x
 241   by mem u (x * !x) -> (exists i. i >= 0 /\ mem u (x * x ^ i))
 242      by let (u1, u2) = u in
 243         exists v. mem (u1, v) x /\ mem (v, u2) !x
 244                   so exists i. i >= 0 /\ mem u (x * x ^ i)
 245
 246   lemma star_unfold_r : forall x u. mem u (one + !x * x) -> mem u !x
 247   by mem u (!x * x) -> (exists i. i >= 0 /\ mem u (x ^ i * x))
 248      by let (u1, u2) = u in
 249      exists v. mem (u1, v) !x /\ mem (v, u2) x
 250             so exists i. i >= 0 /\ mem u (x ^ i * x)
 251
 252   lemma star_induct_left_ind : forall x y z i. i >= 0 ->
 253     z + x * y <= y -> x^i * z <= y
 254
 255   lemma star_induct_left_lem : forall x y z i. i >= 0 ->
 256     z + x * y <= y -> forall u. mem u (x^i * z) -> mem u y
 257
 258   lemma star_induct_left : forall x y z.
 259     z + x * y <= y -> !x * z <= y
 260   by forall u. mem u (!x * z) -> (exists i. i >= 0 /\ mem u (x^i * z))
 261      by let (u1, u2) = u in
 262         exists v. mem (u1, v) !x /\ mem (v, u2) z
 263                   so exists i. i >= 0 /\ mem u (x^i * z)
 264
 265   lemma star_induct_right_ind : forall x y z i. i >= 0 ->
 266     z + y * x <= y -> z * x^i <= y
 267
 268   lemma star_induct_right_lem : forall x y z i. i >= 0 ->
 269     z + y * x <= y -> forall u. mem u (z * x^i) -> mem u y
 270
 271   lemma star_induct_right : forall x y z.
 272     z + y * x <= y -> z * !x <= y
 273   by forall u. mem u (z * !x) -> (exists i. i >= 0 /\ mem u (z * x^i))
 274      by let (u1, u2) = u in
 275         exists v. mem (u1, v) z /\ mem (v, u2) !x
 276                   so exists i. i >= 0 /\ mem u (z * x^i)
 277
 278   (** Prove that this forms a Kleene Algebra *)
 279
 280   clone KleeneAlgebra with type t = t, constant zero = zero,
 281   constant one = one, function (+) = (+), function (*) = (*),
 282   function (!_) = (!_), lemma .
 283 end