test-claude.why 3.48 KB
Newer Older
1 2 3 4 5 6 7
(*

Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.


*)
MARCHE Claude's avatar
MARCHE Claude committed
8

9 10
theory TestProp

MARCHE Claude's avatar
MARCHE Claude committed
11 12 13 14
  goal Test0 : true

  goal Test0_5 : true -> false

15
  predicate a
16

17
  predicate b
18

19
  goal Test1: a /\ b -> a
20 21 22

end

MARCHE Claude's avatar
MARCHE Claude committed
23
theory TestInt
24

25
   use int.Int
26

27
   goal Test1: 2+2 = 4
28

29 30
   goal Test2: forall x:int. x*x >= 0

MARCHE Claude's avatar
MARCHE Claude committed
31
   goal Test3: 1<>0
32

MARCHE Claude's avatar
MARCHE Claude committed
33
   goal Test4: 1=2 -> 3=4
34 35 36

   goal Test5: forall x:int. x <> 0 -> x*x > 0

37
   goal Test6: 2+3 = 5 /\ (forall x:int. x*x >= 0)
38

39
   goal Test7: 0 = 2 /\ 2 = 3 /\ 4 = 5 /\ 6 = 7
MARCHE Claude's avatar
MARCHE Claude committed
40

41
   goal Test8: 2+2=4 /\ 3+3=6
42

43 44
   axiom A : 1 = 2

45
   goal Test9: 2+2=5 /\ 3+3=8
46

MARCHE Claude's avatar
MARCHE Claude committed
47 48
end

49 50
theory TestSplit

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 58

  goal G2 : ("stop_split" aa 0 && bb 1) && ("stop_split" aa 1 && bb 2)

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
MARCHE Claude's avatar
MARCHE Claude committed
64 65 66

  goal Glet : (let x = 1 in x+1 = 2) /\ (let y = 3 in y+2 = 4)

67 68
end

69 70
theory TestMinMax

71 72
  use int.Int
  use int.MinMax
73 74 75 76 77

  goal G1: min 1 2 = 1

end

MARCHE Claude's avatar
MARCHE Claude committed
78 79
theory TestDiv

80
   use int.Int
MARCHE Claude's avatar
MARCHE Claude committed
81 82 83 84 85 86 87 88 89 90 91 92
   use int.EuclideanDivision

   goal EDiv1: EuclideanDivision.div 1 2 = 0

   goal EDiv2: EuclideanDivision.div (-1) 2 = -1

   use int.ComputerDivision

   goal CDiv1: ComputerDivision.div 1 2 = 0

   goal CDiv2: ComputerDivision.div (-1) 2 = 0

MARCHE Claude's avatar
MARCHE Claude committed
93 94
end

95 96
theory TestList

97 98
  use int.Int
  use list.List
99

100
  function x : list int
101

102 103
  goal Test1:
     match x with
104 105
     | Nil -> 1 = 0 /\ 2 = 3
     | Cons _ Nil -> 4 = 5 /\ 6 = 7
106
     | Cons _ _ -> 8 = 9 /\ 10 = 11
107
     end
108

109
end
110

MARCHE Claude's avatar
MARCHE Claude committed
111

MARCHE Claude's avatar
MARCHE Claude committed
112 113
theory TestReal

114
   use real.Real
MARCHE Claude's avatar
MARCHE Claude committed
115 116 117

   goal Real1: forall x:real. x <> 0.0 -> x*x <> 0.0

118
   use real.Abs
119

MARCHE Claude's avatar
MARCHE Claude committed
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
MARCHE Claude's avatar
MARCHE Claude committed
123

MARCHE Claude's avatar
MARCHE Claude committed
124 125 126 127
end

theory TestFloat

128
   use floating_point.Rounding
129 130 131 132
   use floating_point.Single

   lemma Round_single_01: Single.round NearestTiesToEven 0.1 = 0x0.199999Ap0

133 134
end

135 136
theory TestIntros

137
  use int.Int
138

MARCHE Claude's avatar
MARCHE Claude committed
139
  goal G :
140 141 142
    forall x y : int. x > 0 /\ y > 0 ->
      (exists z t:int. x + t = y + z) -> x > y

MARCHE Claude's avatar
MARCHE Claude committed
143
  goal G2 :
144 145 146
    forall x y : int. (x > 0 /\ y > 0) /\ (x < 10 /\ y < 10) ->
      (exists x' y':int. x + x' = y + y') -> x > y

147 148 149 150 151 152

  type t 'a 'b

  goal G3 :
    forall x y: t 'a 'b, z z': t int 'c. z = z' -> x = y

153 154 155 156 157

  axiom A: exists x. x * 6 = 42

  goal g: false

158
end
MARCHE Claude's avatar
MARCHE Claude committed
159

MARCHE Claude's avatar
MARCHE Claude committed
160

161 162 163 164
theory TestRealize

  type t

165
  predicate p t t
166

167 168
  axiom P_arefl: forall x:t. not (p x x)

169
  axiom P_total: forall x y:t. p x y \/ p y x \/ x=y
170

171
  function f t : t
172

173 174
  axiom A : forall x:t. p (f x) x

175 176 177 178 179 180
  lemma B : forall x:t. not (p x (f x))

end

theory TestRealizeUse

181
  use TestRealize
182

183
  function q t : t
184

185
  axiom C : forall x:t. p (q x) x
186 187 188

end

189 190
theory TestRealizeUseInt

191
  use int.Int
192 193 194 195 196 197 198

  function q int : int

  axiom C : forall x:int. q x + x >= 0

end

199
theory TestInline
200

201
  use int.Int
202

203 204
  goal T : 1 = 2

205
  predicate p (x:int) (y:int) = x <= 3 /\ y <= 7
206 207

  goal G : p 4 4
208

209
end
210 211 212

theory TestInductive

213
use int.Int
214 215 216 217 218 219 220 221 222 223 224

inductive p (x:int) =

  | C0 : forall x:int. p x -> p x
(* NonPositiveIndDecl
  | C1 : forall x:int.
     (if p x then true else false) -> p x
*)
  | C2 : let x=0 in p x
end

225
theory TestWarnings
226

227 228 229 230 231 232 233
  type t

  lemma L1 : forall x:t. true

  lemma L2 : exists x:t. x=x -> false

end
MARCHE Claude's avatar
MARCHE Claude committed
234 235 236

theory TestPVSRealAbs

237 238
  use int.Abs
  use real.RealInfix
MARCHE Claude's avatar
MARCHE Claude committed
239 240 241 242
  use import real.Abs as A

  lemma l: A.abs (-. 1.0) = 1.0

243 244 245 246 247 248 249 250 251 252
end

theory TestTransform

 predicate a int
 predicate b int

 lemma L: a 1 /\ b 2

end