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

(* test file *)

4 5
theory Test_inline_trivial
  type t
6 7
  function c : t
  predicate eq (x y :'a) = x=y
8
  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
theory Test_encoding
19
  use int.Int
20 21 22
  function id(x: int) : int = x
  function id2(x: int) : int = id(x)
  function succ(x:int) : int = id(x+1)
23 24

  type myt
25
  function f (int) : myt
26 27
  clone transform.encoding_decorate.Kept with type t = myt

28
  goal G : (forall x:int.f(x)=f(x)) \/
29
    (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 36
  use int.Int
  use map.Map
37
  goal G1 : forall x y:int. forall m: map int int.
38
    get (set m y x) y = x
39
  goal G2 : forall x y:int. forall m: map int int.
40
    get (set m y x) y = y
41 42
  goal G3 : forall x y:int. forall m: map int int.
    get (const x) y = x
43 44 45
end

theory Test_simplify_array2
46 47
  use int.Int
  use map.Map
48
  type t2 'a
49
  goal G1 : forall y:int. forall x:t2 int. forall m: map int (t2 int).
50
    get (set m y x) y = x
François Bobot's avatar
François Bobot committed
51
end
52

François Bobot's avatar
François Bobot committed
53 54
theory Test_guard
  type t
55 56 57
  function f t : t
  function a : t
  function b : t
François Bobot's avatar
François Bobot committed
58
  goal G : forall x:t. f a = x
59
end
60 61

theory Test_conjunction
62
  use int.Int
63
  axiom Trivial : 2 * 2 = 4 /\ 4 * 2 = 8
64
  goal G : 
65
    forall x:int. x*x=4 -> ((x*x*x=8 \/ x*x*x = -8) /\ x*x*2 = 8)
66 67
  goal G2 : 
    forall x:int. 
68
    (x+x=4 \/ x*x=4) -> ((x*x*x=8 \/ x*x*x = -8) /\ x*x*2 = 8)
69 70 71
end

theory Split_conj
72 73 74
  predicate p(x:int)
    (*goal G : forall x,y,z:int. ((p(x) -> p(y)) /\ ((not p(x)) -> p(z))) -> ((p(x) /\ p(y)) \/ ((not p(x)) /\ p(z)))*)
    (*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) <-> ((p(x) /\ p(y)) \/ ((not p(x)) /\ p(z)))*)
75
    (*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))*)
76
  goal G : forall x y z:int. (p(x) <-> p(z)) -> (p(x) <-> p(z))
77 78
    (*goal G : forall x,y,z:int. (p(z) <-> p(x)) -> (((not p(z)) /\ (not p(x))  \/  ((p(z)) /\ (p(x))))) *)
    (*goal G : forall x,y,z:int. (p(x) \/ p(y)) -> p(z)*)
79 80 81 82 83 84
end




theory TestEnco
85
  use int.Int
86
  meta "encoding : kept" type int
87
  type mytype 'a
88 89 90
  function id(x: int) : int = x
  function id2(x: int) : int = id(x)
  function succ(x:int) : int = id(x+1)
91

92
  goal G : (forall x:int. x=x) \/
93
    (forall x:int. x=x+1)
94 95
  function p('a ) : mytype 'a
  function p2(mytype 'a) : 'a
96
  type toto
97
  function f (toto) : mytype toto
98
  axiom A0 : forall x : toto. f(x) = p(x)
99 100
  function g (mytype int) : toto
  function h (int) : toto
101
  axiom A05 : forall x : int. g(p(x)) = h(x)
102
  axiom A1 : forall x : mytype 'a. p(p2(x)) = x
103
  goal G2 : forall x:mytype toto. f(p2(x)) = x
104 105
end

106
theory TestIte
107
  use int.Int
108 109
  use list.Length
  use list.Mem
110
  function abs(x:int) : int = if x >= 0 then x else -x 
111 112 113
  goal G : forall x:int. abs(x) >= 0
  goal G2 : forall x:int. if x>=0 then x >= 0 else -x>=0 
end
114

115
theory TestBuiltin_real
116
  use real.Real
117 118 119 120 121 122
  goal G1 : 5.5 * 10. = 55. 
  goal G2 : 9. / 3. = 3. 
  goal G3 : inv(5.) = 0.2
end

theory TestBuiltin_bool
123
  use bool.Bool
124
  goal G : xorb True False = True 
125
  goal G_false : xorb True False = False
126 127
end

128 129
theory TestEncodingEnumerate
  type t = A | B | C
130
  goal G : forall x : t. (x = A \/ x = B) ->  x<>C
131
  goal G1 : forall x : t. B <> A
132 133
  goal G2 : forall x : t. x = A \/ x = B \/ x=C
  goal G3 : forall x : t. x = A \/ x = B \/ x <> C
134
end
135

136 137 138 139 140 141
(*
Local Variables: 
compile-command: "make -C .. test"
End: 
*)