tests/test-claude.why

   1 (*
   2
   3 Require Import Why3.
   4 Ltac ae := why3 "alt-ergo" timelimit 3.
   5
   6
   7 *)
   8
   9 theory TestProp
  10
  11   goal Test0 : true
  12
  13   goal Test0_5 : true -> false
  14
  15   predicate a
  16
  17   predicate b
  18
  19   goal Test1: a /\ b -> a
  20
  21 end
  22
  23 theory TestInt
  24
  25    use int.Int
  26
  27    goal Test1: 2+2 = 4
  28
  29    goal Test2: forall x:int. x*x >= 0
  30
  31    goal Test3: 1<>0
  32
  33    goal Test4: 1=2 -> 3=4
  34
  35    goal Test5: forall x:int. x <> 0 -> x*x > 0
  36
  37    goal Test6: 2+3 = 5 /\ (forall x:int. x*x >= 0)
  38
  39    goal Test7: 0 = 2 /\ 2 = 3 /\ 4 = 5 /\ 6 = 7
  40
  41    goal Test8: 2+2=4 /\ 3+3=6
  42
  43    axiom A : 1 = 2
  44
  45    goal Test9: 2+2=5 /\ 3+3=8
  46
  47 end
  48
  49 theory TestSplit
  50
  51   predicate aa int
  52
  53   predicate bb int
  54
  55   goal G1 : (aa 5) /\ ("stop_split" aa 0 /\ bb 6) /\ ("stop_split" aa 1 /\ bb 2)
  56
  57   goal G2 : ("stop_split" aa 0 && bb 1) && ("stop_split" aa 1 && bb 2)
  58
  59   goal G3 : forall x:int. ("stop_split" aa x /\ bb 1) /\ ("stop_split" aa 1 /\ bb 2)
  60
  61   goal G4 : forall x:int. ("stop_split" aa x && bb 1) && ("stop_split" aa 1 && bb 2)
  62
  63   use int.Int
  64
  65   goal Glet : (let x = 1 in x+1 = 2) /\ (let y = 3 in y+2 = 4)
  66
  67 end
  68
  69 theory TestMinMax
  70
  71   use int.Int
  72   use int.MinMax
  73
  74   goal G1: min 1 2 = 1
  75
  76 end
  77
  78 theory TestDiv
  79
  80    use int.Int
  81    use int.EuclideanDivision
  82
  83    goal EDiv1: EuclideanDivision.div 1 2 = 0
  84
  85    goal EDiv2: EuclideanDivision.div (-1) 2 = -1
  86
  87    use int.ComputerDivision
  88
  89    goal CDiv1: ComputerDivision.div 1 2 = 0
  90
  91    goal CDiv2: ComputerDivision.div (-1) 2 = 0
  92
  93 end
  94
  95 theory TestList
  96
  97   use int.Int
  98   use list.List
  99
 100   function x : list int
 101
 102   goal Test1:
 103      match x with
 104      | Nil -> 1 = 0 /\ 2 = 3
 105      | Cons _ Nil -> 4 = 5 /\ 6 = 7
 106      | Cons _ _ -> 8 = 9 /\ 10 = 11
 107      end
 108
 109 end
 110
 111
 112 theory TestReal
 113
 114    use real.Real
 115
 116    goal Real1: forall x:real. x <> 0.0 -> x*x <> 0.0
 117
 118    use real.Abs
 119
 120    goal RealAbs1: forall x:real. 100.0 >= abs x >= 1.0 -> x*x >= 1.0
 121
 122    goal T: forall x y:real. abs x <= 1.0 /\ abs y <= 1.0 -> x - y <= 2.0
 123
 124 end
 125
 126 theory TestFloat
 127
 128    use floating_point.Rounding
 129    use floating_point.Single
 130
 131    lemma Round_single_01: Single.round NearestTiesToEven 0.1 = 0x0.199999Ap0
 132
 133 end
 134
 135 theory TestIntros
 136
 137   use int.Int
 138
 139   goal G :
 140     forall x y : int. x > 0 /\ y > 0 ->
 141       (exists z t:int. x + t = y + z) -> x > y
 142
 143   goal G2 :
 144     forall x y : int. (x > 0 /\ y > 0) /\ (x < 10 /\ y < 10) ->
 145       (exists x' y':int. x + x' = y + y') -> x > y
 146
 147
 148   type t 'a 'b
 149
 150   goal G3 :
 151     forall x y: t 'a 'b, z z': t int 'c. z = z' -> x = y
 152
 153
 154   axiom A: exists x. x * 6 = 42
 155
 156   goal g: false
 157
 158 end
 159
 160
 161 theory TestRealize
 162
 163   type t
 164
 165   predicate p t t
 166
 167   axiom P_arefl: forall x:t. not (p x x)
 168
 169   axiom P_total: forall x y:t. p x y \/ p y x \/ x=y
 170
 171   function f t : t
 172
 173   axiom A : forall x:t. p (f x) x
 174
 175   lemma B : forall x:t. not (p x (f x))
 176
 177 end
 178
 179 theory TestRealizeUse
 180
 181   use TestRealize
 182
 183   function q t : t
 184
 185   axiom C : forall x:t. p (q x) x
 186
 187 end
 188
 189 theory TestRealizeUseInt
 190
 191   use int.Int
 192
 193   function q int : int
 194
 195   axiom C : forall x:int. q x + x >= 0
 196
 197 end
 198
 199 theory TestInline
 200
 201   use int.Int
 202
 203   goal T : 1 = 2
 204
 205   predicate p (x:int) (y:int) = x <= 3 /\ y <= 7
 206
 207   goal G : p 4 4
 208
 209 end
 210
 211 theory TestInductive
 212
 213 use int.Int
 214
 215 inductive p (x:int) =
 216
 217   | C0 : forall x:int. p x -> p x
 218 (* NonPositiveIndDecl
 219   | C1 : forall x:int.
 220      (if p x then true else false) -> p x
 221 *)
 222   | C2 : let x=0 in p x
 223 end
 224
 225 theory TestWarnings
 226
 227   type t
 228
 229   lemma L1 : forall x:t. true
 230
 231   lemma L2 : exists x:t. x=x -> false
 232
 233 end
 234
 235 theory TestPVSRealAbs
 236
 237   use int.Abs
 238   use real.RealInfix
 239   use import real.Abs as A
 240
 241   lemma l: A.abs (-. 1.0) = 1.0
 242
 243 end
 244
 245 theory TestTransform
 246
 247  predicate a int
 248  predicate b int
 249
 250  lemma L: a 1 /\ b 2
 251
 252 end