tests/demo-itp.mlw

   1 module Naming
   2   use int.Int
   3   constant x : int
   4   goal G : forall x:int. x >= 0 -> x = 0
   5 end
   6
   7 module ApplyRewrite
   8
   9   use int.Int
  10
  11   function f int int : int
  12
  13   axiom H: forall x. (fun (z: int) -> x + z) =  f x
  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   goal g3: (fun toto -> 42 + toto) 2 = 2
  20
  21   goal g2: (fun y -> y + y) = f 24
  22 end
  23
  24 module A
  25
  26   use int.Int
  27
  28   function f int: int
  29
  30   axiom H: forall y. exists x. f x = x + y
  31
  32   goal g1: exists x. f x = x + 42
  33
  34   goal g: (fun y -> f y) 0 = 3
  35
  36   constant b: bool
  37
  38   axiom Ha: forall y. if b = true then let x = 3 in f x = x + y else false
  39
  40   goal ga: if b = true then let z = 3 in f z = z + 42 else false
  41
  42   goal gb: if b  = true then let z = 453 in f z = z + 42 else false
  43
  44 end
  45
  46 module Soundness
  47
  48   use int.Int
  49
  50   function f0 (x y z:int) : int = x * y + z
  51
  52   predicate p (f:int -> int) =
  53     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
  61   lemma Absurd : false
  62
  63 end
  64
  65 module TestCEX
  66
  67   use int.Int
  68
  69   goal g: forall x. x=0
  70
  71 end
  72
  73 module TestCopyPaste
  74
  75  use int.Int
  76
  77  goal g1: 1=2 /\ 3=4
  78
  79  goal g2: 5=6 /\ 7=8 /\ 9=10
  80
  81 end
  82
  83 module M
  84   use int.Int
  85
  86   function (++) (x:int) (y:int) : int  = x * y
  87
  88 end
  89
  90 module TestWarnings
  91
  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   goal g1: forall z:int. 42 > 0
  99
 100   goal g2: let z=1 in 42 > 0
 101
 102 end
 103
 104 module TestTaskPrinting
 105
 106   use int.Int
 107
 108   function averyveryveryveryveryverylongname int : int
 109
 110   goal g1: averyveryveryveryveryverylongname 1 + averyveryveryveryveryverylongname 2 +
 111            averyveryveryveryveryverylongname 3 + averyveryveryveryveryverylongname 4 >= 0
 112
 113   goal g2: let x = 1 in x + 1 >= 0
 114
 115   goal g3: let x = 1 in averyveryveryveryveryverylongname x + averyveryveryveryveryverylongname 1 >= 0
 116
 117   goal g4: let x = averyveryveryveryveryverylongname 1 in averyveryveryveryveryverylongname x + 1 >= 0
 118
 119   goal g5: let x = averyveryveryveryveryverylongname 1 + averyveryveryveryveryverylongname 2
 120            in averyveryveryveryveryverylongname x + 1 >= 0
 121
 122   goal g6: let x = averyveryveryveryveryverylongname 1 + averyveryveryveryveryverylongname 2
 123            in averyveryveryveryveryverylongname x + averyveryveryveryveryverylongname 1 >= 0
 124
 125   function (+) (x:int) (y:int) : int  = x * y
 126
 127   goal g7: 2 + 3 = Int.(+) 3 3
 128
 129   use M
 130
 131   function (++) (x:int) (y:int) : int  = x * y
 132
 133   goal g8: 2 ++ 3 = M.(++) 3 3
 134
 135 end
 136
 137 module TestAutomaticIntro
 138
 139
 140   use int.Int
 141
 142   goal g : forall x:int. x > 0 -> forall y z:int. y = z -> x=y
 143
 144 end
 145
 146 module TestInduction
 147
 148   use int.Int
 149
 150   predicate p int
 151
 152   goal g : forall n. p n
 153
 154 end
 155
 156 module TestInfixSymbols
 157
 158 function (+) int int : int
 159
 160 goal g : false
 161
 162 end
 163
 164 module TestAutoFocus
 165
 166   use int.Int
 167
 168
 169   goal g0: 0=0 /\ 1=1
 170   (* "split" should mode you to the first subgoal
 171      "compute" should then move you to the second goal
 172      "compute" should then move you to the next goal
 173    *)
 174
 175   goal g1: 2+2 = 4
 176   (* "compute" should move you to the next goal *)
 177
 178   goal g2: 2+3 = 4
 179   (* "compute" should move you to the subgoal 5=4 *)
 180
 181
 182 end
 183
 184 module TestRewritePoly
 185
 186   use int.Int
 187   use list.List
 188   use list.Append
 189
 190   goal g : (Cons 1 Nil) ++ ((Cons 2 Nil) ++ Nil) = Cons 1 (Cons 2 Nil)
 191
 192 end
 193
 194
 195 module Power
 196
 197   use int.Int
 198
 199   function power int int : int
 200   axiom power_0 : forall x:int. power x 0 = 1
 201   axiom power_s : forall x n:int. n >= 0 ->
 202     power x (n+1) = x * power x n
 203
 204   lemma power_1 : forall x:int. power x 1 = x
 205
 206   lemma sqrt4_256 : exists x:int. power x 4 = 256
 207
 208   lemma power_sum : forall x n m: int.
 209     0 <= n /\ 0 <= m ->
 210     power x (n+m) = power x n * power x m
 211
 212 (* Fermat's little theorem for n = 3 *)
 213
 214   lemma power_0_left : forall n. n >= 1 -> power 0 n = 0
 215
 216 (*
 217   lemma power_3 : forall x. x >= 1 ->
 218     power (x-1) 3 = power x 3 - 3 * x * x + 3 * x - 1
 219 *)
 220
 221   lemma little_fermat_3 :
 222     forall x : int. x >= 0 -> exists y : int. power x 3 - x = 3 * y
 223
 224 end
 225
 226
 227 (*
 228 Local Variables:
 229 compile-command: "why3 ide demo-itp.mlw"
 230 End:
 231 *)