test_compute.why 5.52 KB
 MARCHE Claude committed Aug 18, 2014 1 `````` `````` MARCHE Claude committed Sep 08, 2014 2 3 ``````theory Lambda `````` Andrei Paskevich committed Jun 15, 2018 4 ``````use int.Int `````` MARCHE Claude committed Sep 08, 2014 5 6 7 8 9 10 11 `````` constant f : int -> int = (\x:int.x+1) constant a : int goal g1: f 42 = a `````` MARCHE Claude committed May 13, 2016 12 ``````constant compose : ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c) = `````` MARCHE Claude committed Sep 08, 2014 13 14 15 16 `````` (\f:'b->'c.(\g:'a->'b.(\x:'a.f (g x)))) goal g2: compose f f 42 = a `````` MARCHE Claude committed Sep 09, 2014 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 `````` MARCHE Claude committed Sep 08, 2014 25 26 ``````end `````` MARCHE Claude committed Sep 04, 2014 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 `````` Andrei Paskevich committed Jun 15, 2018 36 `````` use bool.Bool `````` MARCHE Claude committed Sep 05, 2014 37 38 39 40 `````` type t function f t : bool `````` MARCHE Claude committed May 13, 2016 41 `````` predicate r t `````` MARCHE Claude committed Sep 05, 2014 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 committed Sep 04, 2014 51 52 ``````end `````` MARCHE Claude committed Aug 20, 2014 53 ``````theory Test `````` MARCHE Claude committed Aug 18, 2014 54 55 56 57 58 59 60 `````` goal g1: true goal g2: true /\ false goal g3: true /\ true `````` MARCHE Claude committed Aug 19, 2014 61 `````` goal g10: if true then 1=1 else 3=4 `````` MARCHE Claude committed Aug 18, 2014 62 `````` `````` MARCHE Claude committed Aug 19, 2014 63 `````` goal g11: let x=1 in x=1 `````` MARCHE Claude committed Aug 18, 2014 64 `````` `````` MARCHE Claude committed Aug 20, 2014 65 66 67 68 ``````end theory TestArith `````` Andrei Paskevich committed Jun 15, 2018 69 `````` use int.Int `````` MARCHE Claude committed Aug 18, 2014 70 71 72 `````` goal h1: 2+2=4 `````` MARCHE Claude committed Aug 20, 2014 73 74 `````` goal h2: 2+(-2)=0 `````` MARCHE Claude committed Aug 20, 2014 75 `````` goal h3: 10 = 0xA `````` MARCHE Claude committed Aug 19, 2014 76 77 78 `````` function g int : int `````` MARCHE Claude committed Aug 19, 2014 79 `````` axiom g4: g 4 = 7 `````` MARCHE Claude committed Aug 19, 2014 80 81 82 `````` meta "rewrite" prop g4 `````` MARCHE Claude committed Aug 19, 2014 83 84 `````` goal j1: g (2+2) = 7 `````` Andrei Paskevich committed Jun 15, 2018 85 `````` use int.Power `````` MARCHE Claude committed Aug 20, 2014 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 `````` MARCHE Claude committed Sep 05, 2014 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 `````` Andrei Paskevich committed Jun 15, 2018 105 `````` use int.ComputerDivision `````` MARCHE Claude committed Sep 05, 2014 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 `````` Andrei Paskevich committed Jun 15, 2018 112 `````` use int.MinMax `````` MARCHE Claude committed Sep 05, 2014 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 `````` MARCHE Claude committed Sep 09, 2014 119 120 `````` function f int : int `````` MARCHE Claude committed May 13, 2016 121 `````` `````` MARCHE Claude committed Sep 09, 2014 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 committed Aug 19, 2014 128 129 ``````end `````` MARCHE Claude committed Aug 20, 2014 130 131 ``````theory TestRecord `````` Andrei Paskevich committed Jun 15, 2018 132 `````` use int.Int `````` MARCHE Claude committed Aug 20, 2014 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 committed Aug 19, 2014 144 145 146 `````` theory TestList `````` Andrei Paskevich committed Jun 15, 2018 147 `````` use int.Int `````` MARCHE Claude committed Aug 19, 2014 148 `````` `````` Andrei Paskevich committed Jun 15, 2018 149 `````` use list.List `````` MARCHE Claude committed Aug 19, 2014 150 151 152 `````` constant l1 : list int = Cons 12 (Cons 34 (Cons 56 Nil)) `````` MARCHE Claude committed Aug 19, 2014 153 `````` goal g1: match l1 with Nil -> 0 | Cons x _ -> x end = 12 `````` MARCHE Claude committed Aug 19, 2014 154 `````` `````` Andrei Paskevich committed Jun 15, 2018 155 `````` use list.Length `````` MARCHE Claude committed Aug 19, 2014 156 157 158 `````` goal g2: length l1 = 3 `````` Andrei Paskevich committed Jun 15, 2018 159 `````` use list.HdTlNoOpt `````` MARCHE Claude committed Aug 19, 2014 160 161 162 163 164 165 `````` meta "rewrite" prop hd_cons meta "rewrite" prop tl_cons goal g3: hd l1 = 12 `````` Andrei Paskevich committed Jun 15, 2018 166 `````` use list.Append `````` MARCHE Claude committed Aug 19, 2014 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 `````` MARCHE Claude committed Aug 20, 2014 175 `````` goal h3: forall x y:int. Cons x Nil = Cons y Nil `````` MARCHE Claude committed Aug 19, 2014 176 `````` `````` MARCHE Claude committed Sep 09, 2014 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 committed Aug 19, 2014 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 `````` Andrei Paskevich committed Jun 15, 2018 237 `````` use Rstandard `````` MARCHE Claude committed Aug 19, 2014 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 `````` MARCHE Claude committed Aug 20, 2014 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 `````` Andrei Paskevich committed Jun 15, 2018 309 `````` use int.Int `````` MARCHE Claude committed Aug 20, 2014 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 `````` MARCHE Claude committed Sep 09, 2014 333 334 335 `````` meta "compute_max_steps" 100000 `````` MARCHE Claude committed Aug 20, 2014 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 committed Aug 19, 2014 342 343 344 345 ``````theory Rinteger use export int.Int `````` MARCHE Claude committed Aug 20, 2014 346 347 348 349 `````` goal g1 : forall y. 2+2 = y goal g2 : forall y. 0 + y + 0 + y - y = y `````` MARCHE Claude committed Sep 12, 2014 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 `````` MARCHE Claude committed May 13, 2016 355 `````` `````` MARCHE Claude committed Aug 19, 2014 356 357 358 359 ``````end theory TestInteger `````` Andrei Paskevich committed Jun 15, 2018 360 `````` use Rinteger `````` MARCHE Claude committed Aug 19, 2014 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 `````` Andrei Paskevich committed Jun 15, 2018 391 ``````use MoreSets `````` MARCHE Claude committed Aug 19, 2014 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)) `````` MARCHE Claude committed Aug 19, 2014 406 `````` `````` MARCHE Claude committed Aug 18, 2014 407 ``````end `````` MARCHE Claude committed May 13, 2016 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 `````` Andrei Paskevich committed Jun 15, 2018 423 ``end``