tests/test-bobot.why

   1
   2 (* test file *)
   3
   4 theory Test_inline_trivial
   5   type t
   6   function c : t
   7   predicate eq (x y :'a) = x=y
   8   goal G : eq c c
   9 end
  10
  11 theory Test_ind
  12   use graph.Path
  13
  14   goal G : true
  15 end
  16
  17 (*
  18 theory Test_encoding
  19   use int.Int
  20   function id(x: int) : int = x
  21   function id2(x: int) : int = id(x)
  22   function succ(x:int) : int = id(x+1)
  23
  24   type myt
  25   function f (int) : myt
  26   clone transform.encoding_decorate.Kept with type t = myt
  27
  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   use int.Int
  36   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   goal G3 : forall x y:int. forall m: map int int.
  42     get (const x) y = x
  43 end
  44
  45 theory Test_simplify_array2
  46   use int.Int
  47   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
  51 end
  52
  53 theory Test_guard
  54   type t
  55   function f t : t
  56   function a : t
  57   function b : t
  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   goal G2 :
  67     forall x:int.
  68     (x+x=4 \/ x*x=4) -> ((x*x*x=8 \/ x*x*x = -8) /\ x*x*2 = 8)
  69 end
  70
  71 theory Split_conj
  72   predicate p(x:int)
  73     (*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)))*)
  74     (*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     (*goal G : forall x,y,z:int. (p(z) <-> p(x)) -> (((not p(z)) /\ (not p(x))  \/  ((p(z)) /\ (p(x))))) *)
  78     (*goal G : forall x,y,z:int. (p(x) \/ p(y)) -> p(z)*)
  79 end
  80
  81
  82
  83
  84 theory TestEnco
  85   use int.Int
  86   meta "encoding : kept" type int
  87   type mytype 'a
  88   function id(x: int) : int = x
  89   function id2(x: int) : int = id(x)
  90   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   function p('a ) : mytype 'a
  95   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   function g (mytype int) : toto
 100   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 end
 105
 106 theory TestIte
 107   use int.Int
 108   use list.Length
 109   use list.Mem
 110   function abs(x:int) : int = if x >= 0 then x else -x
 111   goal G : forall x:int. abs(x) >= 0
 112   goal G2 : forall x:int. if x>=0 then x >= 0 else -x>=0
 113 end
 114
 115 theory TestBuiltin_real
 116   use real.Real
 117   goal G1 : 5.5 * 10. = 55.
 118   goal G2 : 9. / 3. = 3.
 119   goal G3 : inv(5.) = 0.2
 120 end
 121
 122 theory TestBuiltin_bool
 123   use bool.Bool
 124   goal G : xorb True False = True
 125   goal G_false : xorb True False = False
 126 end
 127
 128 theory TestEncodingEnumerate
 129   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   goal G2 : forall x : t. x = A \/ x = B \/ x=C
 133   goal G3 : forall x : t. x = A \/ x = B \/ x <> C
 134 end
 135
 136 (*
 137 Local Variables:
 138 compile-command: "make -C .. test"
 139 End:
 140 *)
 141