tests/test_compute.why

   1
   2 theory Lambda
   3
   4 use int.Int
   5
   6 constant f : int -> int = (\x:int.x+1)
   7
   8 constant a : int
   9
  10 goal g1: f 42 = a
  11
  12 constant compose : ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c) =
  13          (\f:'b->'c.(\g:'a->'b.(\x:'a.f (g x))))
  14
  15 goal g2: compose f f 42 = a
  16
  17 constant h : int -> int
  18
  19 axiom a1 : h 42 = 56
  20
  21 meta "rewrite" prop a1
  22
  23 goal g3: h 42 = 4
  24
  25 end
  26
  27 theory A
  28
  29   predicate p
  30   predicate q
  31
  32   goal G1 : p /\ q
  33   goal G2 : p -> q
  34   goal G3 : p && q
  35
  36   use bool.Bool
  37
  38   type t
  39
  40   function f t : bool
  41   predicate r t
  42
  43   axiom a : forall x:t. f x = True <-> r x
  44
  45   constant c : t
  46
  47   meta "rewrite" prop a
  48
  49   goal g : f c <-> r c
  50
  51 end
  52
  53 theory Test
  54
  55   goal g1: true
  56
  57   goal g2: true /\ false
  58
  59   goal g3: true /\ true
  60
  61   goal g10: if true then 1=1 else 3=4
  62
  63   goal g11: let x=1 in x=1
  64
  65 end
  66
  67 theory TestArith
  68
  69   use int.Int
  70
  71   goal h1: 2+2=4
  72
  73   goal h2: 2+(-2)=0
  74
  75   goal h3: 10 = 0xA
  76
  77   function g int : int
  78
  79   axiom g4: g 4 = 7
  80
  81   meta "rewrite" prop g4
  82
  83   goal j1: g (2+2) = 7
  84
  85   use int.Power
  86
  87   meta "rewrite" prop Power_0
  88 (* not a rule: conditional
  89   meta "rewrite" prop Power_s
  90 *)
  91   goal k1: power 4 3 = 64
  92
  93   constant n : int
  94
  95   goal l1: n+0 = n
  96   goal l2: 0+n = n
  97   goal l3: n+1 = n
  98   goal l4: n*0 = n
  99   goal l5: 0*n = n
 100   goal l6: n*1 = n
 101   goal l7: 1*n = n
 102   goal l8: n-0 = n
 103   goal l9: 0-n = n
 104
 105   use int.ComputerDivision
 106
 107   goal m1: div 0 1 = 42
 108   goal m2: div n 1 = 42
 109   goal m3: div 0 n = 42
 110   goal m4: div n n = 42
 111
 112   use int.MinMax
 113
 114   goal n1: max 3 4 = n
 115   goal n2: max n n = 42
 116   goal n3: min n n = 42
 117   goal n4: min 3 4 = n
 118
 119
 120   function f int : int
 121
 122   axiom a42 : f 42 + 43 = 56
 123
 124   meta rewrite prop a42
 125
 126   goal o1 : f (6*7) + (42 + 1) = n
 127
 128 end
 129
 130 theory TestRecord
 131
 132   use int.Int
 133
 134   type t = { f : int }
 135
 136   goal i1: let x = { f = 4 } in x.f < 5
 137
 138   goal i2: let  x = { f = 4 } in
 139     match x with { f = y } -> y + 1 > 3 end
 140
 141 end
 142
 143
 144
 145 theory TestList
 146
 147   use int.Int
 148
 149   use list.List
 150
 151   constant l1 : list int = Cons 12 (Cons 34 (Cons 56 Nil))
 152
 153   goal g1: match l1 with Nil -> 0 | Cons x _ -> x end = 12
 154
 155   use list.Length
 156
 157   goal g2: length l1 = 3
 158
 159   use list.HdTlNoOpt
 160
 161   meta "rewrite" prop hd_cons
 162   meta "rewrite" prop tl_cons
 163
 164   goal g3: hd l1 = 12
 165
 166   use list.Append
 167
 168   constant l2 : list int =
 169     Cons 12 (Cons 34 (Cons 56 Nil)) ++ Cons 78 (Cons 90 Nil)
 170
 171   goal h1: l2 = l1
 172
 173   goal h2: length l2 = 5
 174
 175   goal h3: forall x y:int. Cons x Nil = Cons y Nil
 176
 177   constant l3 : list int
 178
 179   axiom dangerous: Cons 12 Nil = l3
 180
 181   meta rewrite prop dangerous
 182
 183   goal i1: l3 = Nil ++ Nil
 184
 185 end
 186
 187
 188
 189
 190 theory Rstandard
 191
 192    type t
 193
 194    constant u : t
 195
 196    constant a : t
 197
 198    function f t t : t
 199
 200    function g t : t
 201
 202    axiom a1 : g a = a
 203
 204    meta "rewrite" prop a1
 205
 206
 207
 208    constant b : t
 209
 210    axiom a2 : f b b = g b
 211
 212    meta "rewrite" prop a2
 213
 214
 215    function h t : t
 216
 217    axiom a3 : forall x:t. f (h x) a = g x
 218
 219    meta "rewrite" prop a3
 220
 221    function i t t : t
 222
 223    axiom a4 : forall x y:t. i x y = f x y
 224
 225    meta "rewrite" prop a4
 226
 227    function j t t : t
 228
 229    axiom a5 : forall x:t. j x x = x
 230
 231    meta "rewrite" prop a5
 232
 233 end
 234
 235 theory TestStandard
 236
 237    use Rstandard
 238
 239    goal g00 : u = g a
 240
 241    goal g01 : f (g (g a)) u = f a (g a)
 242
 243    goal g02 : u = f b b
 244
 245    goal g03 : f (f b b) (g b) = f u (f b b)
 246
 247    goal g04 : f (h u) a = f (h a) a
 248
 249    goal g05 : i a b = u
 250
 251    goal g06 : j a b = u
 252
 253    goal g07 : j a a = u
 254
 255 end
 256
 257
 258 theory Rgroup
 259
 260   type t
 261
 262   function ( * ) t t : t
 263
 264   function e : t
 265
 266   function i t : t
 267
 268   axiom assoc : forall x y z:t. (x * y) * z = x * (y * z)
 269
 270   meta "rewrite" prop assoc
 271
 272   axiom id_left : forall x:t. e * x = x
 273
 274   meta "rewrite" prop id_left
 275
 276   axiom inv_left : forall x:t. i x * x = e
 277
 278   meta "rewrite" prop inv_left
 279
 280   constant a:t
 281   constant b:t
 282   constant c:t
 283
 284   goal g0: (a * b) * c = e
 285
 286   goal g01: (a * e) * c = a * c
 287
 288   goal g1: (b * i a) * a = b
 289
 290   goal g2: ((b * i a) * a) * a = b * a
 291
 292 end
 293
 294
 295 theory NonTerm
 296
 297   type t
 298
 299   constant c : t
 300
 301   function f t : t
 302
 303   axiom a: f c = f (f c)
 304
 305   meta "rewrite" prop a
 306
 307   goal g: f c = f c
 308
 309   use int.Int
 310
 311   type nat = O | S nat
 312
 313   function plus (n m:nat) : nat =
 314     match n with
 315     | O -> m
 316     | S k -> S (plus k m)
 317     end
 318
 319   function fib (n:nat) : nat =
 320     match n with
 321     | O -> O
 322     | S O -> S O
 323     | S (S n as m) -> plus (fib n) (fib m)
 324     end
 325
 326   constant x : nat
 327
 328   goal g3 : fib (S (S (S O))) = x
 329   goal g4 : fib (S (S (S (S O)))) = x
 330   goal g5 : fib (S (S (S (S (S O))))) = x
 331   goal g6 : fib (S (S (S (S (S (S O)))))) = x
 332   goal g7 : fib (S (S (S (S (S (S (S O))))))) = x
 333
 334   meta "compute_max_steps" 100000
 335
 336   goal g8 : fib (S (S (S (S (S (S (S (S O)))))))) = x
 337   goal g9 : fib (S (S (S (S (S (S (S (S (S O))))))))) = x
 338   goal g10 : fib (S (S (S (S (S (S (S (S (S (S O)))))))))) = x
 339
 340 end
 341
 342 theory Rinteger
 343
 344    use export int.Int
 345
 346    goal g1 : forall y. 2+2 = y
 347
 348    goal g2 : forall y.  0 + y + 0 + y - y = y
 349
 350    lemma l1 : forall x y z:int. (x + y) + z = z + (y + x)
 351
 352    function f int : int
 353
 354    goal g3 : (f 1 + f 2) + f 3 = f 4
 355
 356 end
 357
 358 theory TestInteger
 359
 360    use Rinteger
 361
 362    predicate f1 (y:int) = y > 0 /\ true
 363
 364    goal g1 : true /\ false
 365
 366    predicate f2 (y:int) = y + 0 >= 1
 367
 368    function f3 (y:int) : int = y + 0
 369
 370    goal g2 : 1 + 0 = 1
 371
 372    goal g3 : 1 + 0 >= 1
 373
 374 end
 375
 376
 377 theory MoreSets
 378
 379 use export set.Set
 380
 381 meta "rewrite" prop mem_empty
 382
 383 meta "rewrite" prop add_def1
 384
 385 meta "rewrite" prop union_def1
 386
 387 end
 388
 389 theory TestSets
 390
 391 use MoreSets
 392
 393 type t = A | B | C | D
 394
 395 goal g00 : mem A empty
 396
 397
 398 goal g01 : mem A (add B empty)
 399
 400 goal g015 : mem A (singleton B)
 401
 402
 403 goal g02 : mem A (union (add B empty) (add C empty))
 404
 405 goal g025 : mem A (union (singleton B) (singleton C))
 406
 407 end
 408
 409
 410 theory Wrong
 411
 412 type t
 413
 414 constant a : t
 415 constant b : t
 416
 417 axiom A : forall x:t. a = x
 418
 419 meta "rewrite" prop A
 420
 421 goal test : a = b
 422
 423 end