module Naming use int.Int constant x : int goal G : forall x:int. x >= 0 -> x = 0 end module ApplyRewrite use int.Int function f int int : int axiom H: forall x. (fun (z: int) -> x + z) = f x goal g1: (fun toto -> 42 + toto) = f 42 axiom Ha: forall x. (fun (z: int) -> x + z) 2 = 2 goal g3: (fun toto -> 42 + toto) 2 = 2 goal g2: (fun y -> y + y) = f 24 end module A use int.Int function f int: int axiom H: forall y. exists x. f x = x + y goal g1: exists x. f x = x + 42 goal g: (fun y -> f y) 0 = 3 constant b: bool axiom Ha: forall y. if b = true then let x = 3 in f x = x + y else false 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 end module Soundness use int.Int function f0 (x y z:int) : int = x * y + z predicate p (f:int -> int) = f (-1) = 0 && forall n:int. f n = f 0 + (f 1 - f 0) * n lemma A : forall y z:int. p (fun x -> f0 x y z) <-> y = z meta rewrite lemma A lemma Fail : 0 = 0 /\ p (fun x -> f0 x x x) lemma Absurd : false end module TestCEX use int.Int goal g: forall x. x=0 end module TestCopyPaste use int.Int goal g1: 1=2 /\ 3=4 goal g2: 5=6 /\ 7=8 /\ 9=10 end module M use int.Int function (++) (x:int) (y:int) : int = x * y end module TestWarnings use int.Int function f (x y : int) :int = x axiom a : forall x:int. x*x >= 0 goal g1: forall z:int. 42 > 0 goal g2: let z=1 in 42 > 0 end module TestTaskPrinting use int.Int function averyveryveryveryveryverylongname int : int goal g1: averyveryveryveryveryverylongname 1 + averyveryveryveryveryverylongname 2 + averyveryveryveryveryverylongname 3 + averyveryveryveryveryverylongname 4 >= 0 goal g2: let x = 1 in x + 1 >= 0 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 function (+) (x:int) (y:int) : int = x * y goal g7: 2 + 3 = Int.(+) 3 3 use M function (++) (x:int) (y:int) : int = x * y goal g8: 2 ++ 3 = M.(++) 3 3 end module TestAutomaticIntro use int.Int goal g : forall x:int. x > 0 -> forall y z:int. y = z -> x=y end module TestInduction use int.Int predicate p int goal g : forall n. p n end module TestInfixSymbols function (+) int int : int goal g : false end module TestAutoFocus use int.Int 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 module TestRewritePoly use int.Int use list.List use list.Append goal g : (Cons 1 Nil) ++ ((Cons 2 Nil) ++ Nil) = Cons 1 (Cons 2 Nil) end module Power use int.Int 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 lemma power_sum : forall x n m: int. 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 (* lemma power_3 : forall x. x >= 1 -> power (x-1) 3 = power x 3 - 3 * x * x + 3 * x - 1 *) lemma little_fermat_3 : forall x : int. x >= 0 -> exists y : int. power x 3 - x = 3 * y end (* Local Variables: compile-command: "why3 ide demo-itp.mlw" End: *)