test-bobot.why 2.84 KB
Newer Older
1 2 3

(* test file *)

4 5 6
theory Test_inline_trivial
  type t
  logic c : t
7 8
  logic eq (x y :'a) = x=y
  goal G : eq c c
9 10
end

11 12 13 14 15 16
theory Test_ind
  use graph.Path

  goal G : true
end

17
(*
18 19 20 21 22 23 24 25 26 27 28 29
theory Test_encoding
  use import int.Int
  logic id(x: int) : int = x
  logic id2(x: int) : int = id(x)
  logic succ(x:int) : int = id(x+1)

  type myt
  logic f (int) : myt
  clone transform.encoding_decorate.Kept with type t = myt

  goal G : (forall x:int.f(x)=f(x)) or
    (forall x:int. x=x+1)
30
  goal G2 : forall x:int. let x = 0 + 1 in x = let y = 0 + 1 + 0 in y
31
end
32
*)
33 34

theory Test_simplify_array
35
  use import array.ArrayPoly
36
  goal G : forall x y:int. forall m: t int int. 
37
    get (set m y x) y = x
38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53
end 

theory Test_conjunction
  use import int.Int
  goal G : 
    forall x:int. x*x=4 -> ((x*x*x=8 or x*x*x = -8) and x*x*2 = 8)
  goal G2 : 
    forall x:int. 
    (x+x=4 or x*x=4) -> ((x*x*x=8 or x*x*x = -8) and x*x*2 = 8)
end

theory Split_conj
  logic p(x:int)
    (*goal G : forall x,y,z:int. ((p(x) -> p(y)) and ((not p(x)) -> p(z))) -> ((p(x) and p(y)) or ((not p(x)) and p(z)))*)
    (*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) <-> ((p(x) and p(y)) or ((not p(x)) and p(z)))*)
    (*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) -> (if p(x) then p(y) else p(z))*)
54
  goal G : forall x y z:int. (p(x) <-> p(z)) -> (p(x) <-> p(z))
55 56 57 58 59 60 61 62 63
    (*goal G : forall x,y,z:int. (p(z) <-> p(x)) -> (((not p(z)) and (not p(x))  or  ((p(z)) and (p(x))))) *)
    (*goal G : forall x,y,z:int. (p(x) or p(y)) -> p(z)*)
end




theory TestEnco
  use import int.Int
64
  meta "encoding_decorate : kept" type int
65
  type mytype 'a
66 67 68 69 70 71
  logic id(x: int) : int = x
  logic id2(x: int) : int = id(x)
  logic succ(x:int) : int = id(x+1)

  goal G : (forall x:int. x=x) or
    (forall x:int. x=x+1)
72 73
  logic p('a ) : mytype 'a
  logic p2(mytype 'a) : 'a
74
  type toto
75
  logic f (toto) : mytype toto
76
  axiom A0 : forall x : toto. f(x) = p(x)
77
  logic g (mytype int) : toto
78 79
  logic h (int) : toto
  axiom A05 : forall x : int. g(p(x)) = h(x)
80
  axiom A1 : forall x : mytype 'a. p(p2(x)) = x
81
  goal G2 : forall x:mytype toto. f(p2(x)) = x
82 83
end

84 85
theory TestIte
  use import int.Int
86 87
  use list.Length
  use list.Mem
88 89 90 91
  logic abs(x:int) : int = if x >= 0 then x else -x 
  goal G : forall x:int. abs(x) >= 0
  goal G2 : forall x:int. if x>=0 then x >= 0 else -x>=0 
end
92

93 94 95 96 97 98 99 100 101
theory TestBuiltin_real
  use import real.Real
  goal G1 : 5.5 * 10. = 55. 
  goal G2 : 9. / 3. = 3. 
  goal G3 : inv(5.) = 0.2
end

theory TestBuiltin_bool
  use import bool.Bool
102
  goal G : xorb True False = True 
103
  goal G_false : xorb True False = False
104 105
end

106 107 108 109 110 111 112
theory TestEncodingEnumerate
  type t = A | B | C
  goal G : forall x : t. (x = A or x = B) ->  x<>C
  goal G1 : forall x : t. B <> A
  goal G2 : forall x : t. x = A or x = B or x=C
  goal G3 : forall x : t. x = A or x = B or x <> C
end
113

114 115 116 117 118 119
(*
Local Variables: 
compile-command: "make -C .. test"
End: 
*)