(* Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. *) theory TestProp goal Test0 : true goal Test0_5 : true -> false predicate a predicate b goal Test1: a /\ b -> a end theory TestInt use int.Int goal Test1: 2+2 = 4 goal Test2: forall x:int. x*x >= 0 goal Test3: 1<>0 goal Test4: 1=2 -> 3=4 goal Test5: forall x:int. x <> 0 -> x*x > 0 goal Test6: 2+3 = 5 /\ (forall x:int. x*x >= 0) goal Test7: 0 = 2 /\ 2 = 3 /\ 4 = 5 /\ 6 = 7 goal Test8: 2+2=4 /\ 3+3=6 axiom A : 1 = 2 goal Test9: 2+2=5 /\ 3+3=8 end theory TestSplit predicate aa int predicate bb int goal G1 : (aa 5) /\ ("stop_split" aa 0 /\ bb 6) /\ ("stop_split" aa 1 /\ bb 2) goal G2 : ("stop_split" aa 0 && bb 1) && ("stop_split" aa 1 && bb 2) goal G3 : forall x:int. ("stop_split" aa x /\ bb 1) /\ ("stop_split" aa 1 /\ bb 2) goal G4 : forall x:int. ("stop_split" aa x && bb 1) && ("stop_split" aa 1 && bb 2) use int.Int goal Glet : (let x = 1 in x+1 = 2) /\ (let y = 3 in y+2 = 4) end theory TestMinMax use int.Int use int.MinMax goal G1: min 1 2 = 1 end theory TestDiv use int.Int 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 end theory TestList use int.Int use list.List function x : list int goal Test1: match x with | Nil -> 1 = 0 /\ 2 = 3 | Cons _ Nil -> 4 = 5 /\ 6 = 7 | Cons _ _ -> 8 = 9 /\ 10 = 11 end end theory TestReal use real.Real goal Real1: forall x:real. x <> 0.0 -> x*x <> 0.0 use real.Abs goal RealAbs1: forall x:real. 100.0 >= abs x >= 1.0 -> x*x >= 1.0 goal T: forall x y:real. abs x <= 1.0 /\ abs y <= 1.0 -> x - y <= 2.0 end theory TestFloat use floating_point.Rounding use floating_point.Single lemma Round_single_01: Single.round NearestTiesToEven 0.1 = 0x0.199999Ap0 end theory TestIntros use int.Int goal G : forall x y : int. x > 0 /\ y > 0 -> (exists z t:int. x + t = y + z) -> x > y goal G2 : forall x y : int. (x > 0 /\ y > 0) /\ (x < 10 /\ y < 10) -> (exists x' y':int. x + x' = y + y') -> x > y type t 'a 'b goal G3 : forall x y: t 'a 'b, z z': t int 'c. z = z' -> x = y axiom A: exists x. x * 6 = 42 goal g: false end theory TestRealize type t predicate p t t axiom P_arefl: forall x:t. not (p x x) axiom P_total: forall x y:t. p x y \/ p y x \/ x=y function f t : t axiom A : forall x:t. p (f x) x lemma B : forall x:t. not (p x (f x)) end theory TestRealizeUse use TestRealize function q t : t axiom C : forall x:t. p (q x) x end theory TestRealizeUseInt use int.Int function q int : int axiom C : forall x:int. q x + x >= 0 end theory TestInline use int.Int goal T : 1 = 2 predicate p (x:int) (y:int) = x <= 3 /\ y <= 7 goal G : p 4 4 end theory TestInductive use int.Int 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 theory TestWarnings type t lemma L1 : forall x:t. true lemma L2 : exists x:t. x=x -> false end theory TestPVSRealAbs use int.Abs use real.RealInfix use import real.Abs as A lemma l: A.abs (-. 1.0) = 1.0 end theory TestTransform predicate a int predicate b int lemma L: a 1 /\ b 2 end