module M use import int.Int function (++) (x:int) (y:int) : int = x * y end module TestTaskPrinting use import 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 import M function (++) (x:int) (y:int) : int = x * y goal g8: 2 ++ 3 = M.(++) 3 3 end module TestAutomaticIntro use import int.Int goal g : forall x:int. x > 0 -> forall y z:int. y = z -> x=y end module TestInduction use import 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 import 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 import int.Int use import list.List use import list.Append goal g : (Cons 1 Nil) ++ ((Cons 2 Nil) ++ Nil) = Cons 1 (Cons 2 Nil) end module Power use import 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: *)