test_compute.why 5.52 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1

2 3
theory Lambda

4
use int.Int
5 6 7 8 9 10 11

constant f : int -> int = (\x:int.x+1)

constant a : int

goal g1: f 42 = a

12
constant compose : ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c) =
13 14 15 16
         (\f:'b->'c.(\g:'a->'b.(\x:'a.f (g x))))

goal g2: compose f f 42 = a

17 18 19 20 21 22 23 24
constant h : int -> int

axiom a1 : h 42 = 56

meta "rewrite" prop a1

goal g3: h 42 = 4

25 26
end

MARCHE Claude's avatar
MARCHE Claude committed
27 28 29 30 31 32 33 34 35
theory A

  predicate p
  predicate q

  goal G1 : p /\ q
  goal G2 : p -> q
  goal G3 : p && q

36
  use bool.Bool
37 38 39 40

  type t

  function f t : bool
41
  predicate r t
42 43 44 45 46 47 48 49 50

  axiom a : forall x:t. f x = True <-> r x

  constant c : t

  meta "rewrite" prop a

  goal g : f c <-> r c

MARCHE Claude's avatar
MARCHE Claude committed
51 52
end

MARCHE Claude's avatar
MARCHE Claude committed
53
theory Test
MARCHE Claude's avatar
MARCHE Claude committed
54 55 56 57 58 59 60

  goal g1: true

  goal g2: true /\ false

  goal g3: true /\ true

61
  goal g10: if true then 1=1 else 3=4
MARCHE Claude's avatar
MARCHE Claude committed
62

63
  goal g11: let x=1 in x=1
MARCHE Claude's avatar
MARCHE Claude committed
64

MARCHE Claude's avatar
MARCHE Claude committed
65 66 67 68
end

theory TestArith

69
  use int.Int
MARCHE Claude's avatar
MARCHE Claude committed
70 71 72

  goal h1: 2+2=4

73 74
  goal h2: 2+(-2)=0

MARCHE Claude's avatar
MARCHE Claude committed
75
  goal h3: 10 = 0xA
76 77 78

  function g int : int

MARCHE Claude's avatar
MARCHE Claude committed
79
  axiom g4: g 4 = 7
80 81 82

  meta "rewrite" prop g4

MARCHE Claude's avatar
MARCHE Claude committed
83 84
  goal j1: g (2+2) = 7

85
  use int.Power
MARCHE Claude's avatar
MARCHE Claude committed
86 87 88 89 90 91 92

  meta "rewrite" prop Power_0
(* not a rule: conditional
  meta "rewrite" prop Power_s
*)
  goal k1: power 4 3 = 64

93 94 95 96 97 98 99 100 101 102 103 104
  constant n : int

  goal l1: n+0 = n
  goal l2: 0+n = n
  goal l3: n+1 = n
  goal l4: n*0 = n
  goal l5: 0*n = n
  goal l6: n*1 = n
  goal l7: 1*n = n
  goal l8: n-0 = n
  goal l9: 0-n = n

105
  use int.ComputerDivision
106 107 108 109 110 111

  goal m1: div 0 1 = 42
  goal m2: div n 1 = 42
  goal m3: div 0 n = 42
  goal m4: div n n = 42

112
  use int.MinMax
113 114 115 116 117 118

  goal n1: max 3 4 = n
  goal n2: max n n = 42
  goal n3: min n n = 42
  goal n4: min 3 4 = n

119 120

  function f int : int
121

122 123 124 125 126 127
  axiom a42 : f 42 + 43 = 56

  meta rewrite prop a42

  goal o1 : f (6*7) + (42 + 1) = n

MARCHE Claude's avatar
MARCHE Claude committed
128 129
end

MARCHE Claude's avatar
MARCHE Claude committed
130 131
theory TestRecord

132
  use int.Int
MARCHE Claude's avatar
MARCHE Claude committed
133 134 135 136 137 138 139 140 141 142 143

  type t = { f : int }

  goal i1: let x = { f = 4 } in x.f < 5

  goal i2: let  x = { f = 4 } in
    match x with { f = y } -> y + 1 > 3 end

end


MARCHE Claude's avatar
MARCHE Claude committed
144 145 146

theory TestList

147
  use int.Int
MARCHE Claude's avatar
MARCHE Claude committed
148

149
  use list.List
MARCHE Claude's avatar
MARCHE Claude committed
150 151 152

  constant l1 : list int = Cons 12 (Cons 34 (Cons 56 Nil))

153
  goal g1: match l1 with Nil -> 0 | Cons x _ -> x end = 12
MARCHE Claude's avatar
MARCHE Claude committed
154

155
  use list.Length
MARCHE Claude's avatar
MARCHE Claude committed
156 157 158

  goal g2: length l1 = 3

159
  use list.HdTlNoOpt
MARCHE Claude's avatar
MARCHE Claude committed
160 161 162 163 164 165

  meta "rewrite" prop hd_cons
  meta "rewrite" prop tl_cons

  goal g3: hd l1 = 12

166
  use list.Append
MARCHE Claude's avatar
MARCHE Claude committed
167 168 169 170 171 172 173 174

  constant l2 : list int =
    Cons 12 (Cons 34 (Cons 56 Nil)) ++ Cons 78 (Cons 90 Nil)

  goal h1: l2 = l1

  goal h2: length l2 = 5

175
  goal h3: forall x y:int. Cons x Nil = Cons y Nil
MARCHE Claude's avatar
MARCHE Claude committed
176

177 178 179 180 181 182 183 184
  constant l3 : list int

  axiom dangerous: Cons 12 Nil = l3

  meta rewrite prop dangerous

  goal i1: l3 = Nil ++ Nil

MARCHE Claude's avatar
MARCHE Claude committed
185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236
end




theory Rstandard

   type t

   constant u : t

   constant a : t

   function f t t : t

   function g t : t

   axiom a1 : g a = a

   meta "rewrite" prop a1



   constant b : t

   axiom a2 : f b b = g b

   meta "rewrite" prop a2


   function h t : t

   axiom a3 : forall x:t. f (h x) a = g x

   meta "rewrite" prop a3

   function i t t : t

   axiom a4 : forall x y:t. i x y = f x y

   meta "rewrite" prop a4

   function j t t : t

   axiom a5 : forall x:t. j x x = x

   meta "rewrite" prop a5

end

theory TestStandard

237
   use Rstandard
MARCHE Claude's avatar
MARCHE Claude committed
238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294

   goal g00 : u = g a

   goal g01 : f (g (g a)) u = f a (g a)

   goal g02 : u = f b b

   goal g03 : f (f b b) (g b) = f u (f b b)

   goal g04 : f (h u) a = f (h a) a

   goal g05 : i a b = u

   goal g06 : j a b = u

   goal g07 : j a a = u

end


theory Rgroup

  type t

  function ( * ) t t : t

  function e : t

  function i t : t

  axiom assoc : forall x y z:t. (x * y) * z = x * (y * z)

  meta "rewrite" prop assoc

  axiom id_left : forall x:t. e * x = x

  meta "rewrite" prop id_left

  axiom inv_left : forall x:t. i x * x = e

  meta "rewrite" prop inv_left

  constant a:t
  constant b:t
  constant c:t

  goal g0: (a * b) * c = e

  goal g01: (a * e) * c = a * c

  goal g1: (b * i a) * a = b

  goal g2: ((b * i a) * a) * a = b * a

end


295 296 297 298 299 300 301 302 303 304 305 306 307 308
theory NonTerm

  type t

  constant c : t

  function f t : t

  axiom a: f c = f (f c)

  meta "rewrite" prop a

  goal g: f c = f c

309
  use int.Int
310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332

  type nat = O | S nat

  function plus (n m:nat) : nat =
    match n with
    | O -> m
    | S k -> S (plus k m)
    end

  function fib (n:nat) : nat =
    match n with
    | O -> O
    | S O -> S O
    | S (S n as m) -> plus (fib n) (fib m)
    end

  constant x : nat

  goal g3 : fib (S (S (S O))) = x
  goal g4 : fib (S (S (S (S O)))) = x
  goal g5 : fib (S (S (S (S (S O))))) = x
  goal g6 : fib (S (S (S (S (S (S O)))))) = x
  goal g7 : fib (S (S (S (S (S (S (S O))))))) = x
333 334 335

  meta "compute_max_steps" 100000

336 337 338 339 340 341
  goal g8 : fib (S (S (S (S (S (S (S (S O)))))))) = x
  goal g9 : fib (S (S (S (S (S (S (S (S (S O))))))))) = x
  goal g10 : fib (S (S (S (S (S (S (S (S (S (S O)))))))))) = x

end

MARCHE Claude's avatar
MARCHE Claude committed
342 343 344 345
theory Rinteger

   use export int.Int

MARCHE Claude's avatar
MARCHE Claude committed
346 347 348 349
   goal g1 : forall y. 2+2 = y

   goal g2 : forall y.  0 + y + 0 + y - y = y

350 351 352 353 354
   lemma l1 : forall x y z:int. (x + y) + z = z + (y + x)

   function f int : int

   goal g3 : (f 1 + f 2) + f 3 = f 4
355

MARCHE Claude's avatar
MARCHE Claude committed
356 357 358 359
end

theory TestInteger

360
   use Rinteger
MARCHE Claude's avatar
MARCHE Claude committed
361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390

   predicate f1 (y:int) = y > 0 /\ true

   goal g1 : true /\ false

   predicate f2 (y:int) = y + 0 >= 1

   function f3 (y:int) : int = y + 0

   goal g2 : 1 + 0 = 1

   goal g3 : 1 + 0 >= 1

end


theory MoreSets

use export set.Set

meta "rewrite" prop mem_empty

meta "rewrite" prop add_def1

meta "rewrite" prop union_def1

end

theory TestSets

391
use MoreSets
MARCHE Claude's avatar
MARCHE Claude committed
392 393 394 395 396 397 398 399 400 401 402 403 404 405

type t = A | B | C | D

goal g00 : mem A empty


goal g01 : mem A (add B empty)

goal g015 : mem A (singleton B)


goal g02 : mem A (union (add B empty) (add C empty))

goal g025 : mem A (union (singleton B) (singleton C))
406

MARCHE Claude's avatar
MARCHE Claude committed
407
end
408 409 410 411 412 413 414 415 416 417 418 419 420 421 422


theory Wrong

type t

constant a : t
constant b : t

axiom A : forall x:t. a = x

meta "rewrite" prop A

goal test : a = b

423
end