demo-itp.mlw 4.01 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
module Naming
2
  use int.Int
MARCHE Claude's avatar
MARCHE Claude committed
3 4 5
  constant x : int
  goal G : forall x:int. x >= 0 -> x = 0
end
6

7 8
module ApplyRewrite

9
  use int.Int
10

Sylvain Dailler's avatar
Sylvain Dailler committed
11
  function f int int : int
12

13
  axiom H: forall x. (fun (z: int) -> x + z) =  f x
Sylvain Dailler's avatar
Sylvain Dailler committed
14

15
  goal g1: (fun toto -> 42 + toto) = f 42
16

17
  axiom Ha: forall x. (fun (z: int) -> x + z) 2 = 2
18 19 20

  goal g3: (fun toto -> 42 + toto) 2 = 2

21
  goal g2: (fun y -> y + y) = f 24
Sylvain Dailler's avatar
Sylvain Dailler committed
22 23 24
end

module A
25 26

  use int.Int
Sylvain Dailler's avatar
Sylvain Dailler committed
27 28 29 30

  function f int: int

  axiom H: forall y. exists x. f x = x + y
31

Sylvain Dailler's avatar
Sylvain Dailler committed
32
  goal g1: exists x. f x = x + 42
33

34
  goal g: (fun y -> f y) 0 = 3
Sylvain Dailler's avatar
Sylvain Dailler committed
35 36 37 38

  constant b: bool

  axiom Ha: forall y. if b = true then let x = 3 in f x = x + y else false
39

Sylvain Dailler's avatar
Sylvain Dailler committed
40 41 42
  goal ga: if b = true then let z = 3 in f z = z + 42 else false

  goal gb: if b  = true then let z = 453 in f z = z + 42 else false
43 44 45

end

Sylvain Dailler's avatar
Sylvain Dailler committed
46
module Soundness
47 48 49

  use int.Int

Sylvain Dailler's avatar
Sylvain Dailler committed
50
  function f0 (x y z:int) : int = x * y + z
51

Sylvain Dailler's avatar
Sylvain Dailler committed
52 53
  predicate p (f:int -> int) =
    f (-1) = 0 && forall n:int. f n = f 0 + (f 1 - f 0) * n
54

55
  lemma A : forall y z:int. p (fun x -> f0 x y z) <-> y = z
56

57
  meta rewrite lemma A
58

59
  lemma Fail : 0 = 0 /\ p (fun x -> f0 x x x)
60

Sylvain Dailler's avatar
Sylvain Dailler committed
61
  lemma Absurd : false
62

Sylvain Dailler's avatar
Sylvain Dailler committed
63
end
64

65 66
module TestCEX

67 68
  use int.Int

69
  goal g: forall x. x=0
70

71
end
72

73 74
module TestCopyPaste

75
 use int.Int
76 77 78 79 80 81 82

 goal g1: 1=2 /\ 3=4

 goal g2: 5=6 /\ 7=8 /\ 9=10

end

83
module M
84
  use int.Int
85 86 87 88 89

  function (++) (x:int) (y:int) : int  = x * y

end

90 91
module TestWarnings

92
  use int.Int
93

94
  function f (x y : int) :int = x
95

96
  axiom a : forall x:int. x*x >= 0
97

98 99 100 101 102 103
  goal g1: forall z:int. 42 > 0

  goal g2: let z=1 in 42 > 0

end

104 105
module TestTaskPrinting

106
  use int.Int
107 108 109 110 111 112

  function averyveryveryveryveryverylongname int : int

  goal g1: averyveryveryveryveryverylongname 1 + averyveryveryveryveryverylongname 2 +
           averyveryveryveryveryverylongname 3 + averyveryveryveryveryverylongname 4 >= 0

113
  goal g2: let x = 1 in x + 1 >= 0
114 115 116 117 118 119 120 121 122 123 124

  goal g3: let x = 1 in averyveryveryveryveryverylongname x + averyveryveryveryveryverylongname 1 >= 0

  goal g4: let x = averyveryveryveryveryverylongname 1 in averyveryveryveryveryverylongname x + 1 >= 0

  goal g5: let x = averyveryveryveryveryverylongname 1 + averyveryveryveryveryverylongname 2
           in averyveryveryveryveryverylongname x + 1 >= 0

  goal g6: let x = averyveryveryveryveryverylongname 1 + averyveryveryveryveryverylongname 2
           in averyveryveryveryveryverylongname x + averyveryveryveryveryverylongname 1 >= 0

125 126 127 128
  function (+) (x:int) (y:int) : int  = x * y

  goal g7: 2 + 3 = Int.(+) 3 3

129
  use M
130 131 132 133 134

  function (++) (x:int) (y:int) : int  = x * y

  goal g8: 2 ++ 3 = M.(++) 3 3

135
end
136

137 138 139
module TestAutomaticIntro


140
  use int.Int
141 142 143 144 145

  goal g : forall x:int. x > 0 -> forall y z:int. y = z -> x=y

end

146 147
module TestInduction

148
  use int.Int
149

150
  predicate p int
151

152
  goal g : forall n. p n
153

154
end
155 156 157 158 159 160 161 162 163

module TestInfixSymbols

function (+) int int : int

goal g : false

end

164 165
module TestAutoFocus

166
  use int.Int
167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183


  goal g0: 0=0 /\ 1=1
  (* "split" should mode you to the first subgoal
     "compute" should then move you to the second goal
     "compute" should then move you to the next goal
   *)

  goal g1: 2+2 = 4
  (* "compute" should move you to the next goal *)

  goal g2: 2+3 = 4
  (* "compute" should move you to the subgoal 5=4 *)


end

184 185
module TestRewritePoly

186 187 188
  use int.Int
  use list.List
  use list.Append
189

190
  goal g : (Cons 1 Nil) ++ ((Cons 2 Nil) ++ Nil) = Cons 1 (Cons 2 Nil)
191

192 193
end

194

195 196
module Power

197
  use int.Int
198 199 200 201 202 203 204 205 206 207

  function power int int : int
  axiom power_0 : forall x:int. power x 0 = 1
  axiom power_s : forall x n:int. n >= 0 ->
    power x (n+1) = x * power x n

  lemma power_1 : forall x:int. power x 1 = x

  lemma sqrt4_256 : exists x:int. power x 4 = 256

MARCHE Claude's avatar
MARCHE Claude committed
208
  lemma power_sum : forall x n m: int.
209 210 211 212 213 214 215
    0 <= n /\ 0 <= m ->
    power x (n+m) = power x n * power x m

(* Fermat's little theorem for n = 3 *)

  lemma power_0_left : forall n. n >= 1 -> power 0 n = 0

MARCHE Claude's avatar
MARCHE Claude committed
216
(*
217 218
  lemma power_3 : forall x. x >= 1 ->
    power (x-1) 3 = power x 3 - 3 * x * x + 3 * x - 1
MARCHE Claude's avatar
MARCHE Claude committed
219
*)
220

MARCHE Claude's avatar
MARCHE Claude committed
221 222
  lemma little_fermat_3 :
    forall x : int. x >= 0 -> exists y : int. power x 3 - x = 3 * y
223 224 225 226 227 228

end


(*
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
229
compile-command: "why3 ide demo-itp.mlw"
230 231
End:
*)