mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
844 lines
25 KiB
Plaintext
844 lines
25 KiB
Plaintext
Theory are:
|
|
theory Test
|
|
|
|
(* use why3.BuiltIn.BuiltIn *)
|
|
|
|
(* use why3.Bool.Bool *)
|
|
|
|
(* use why3.Unit.Unit *)
|
|
|
|
(* use int.Int *)
|
|
|
|
type a = <range 22 46>
|
|
|
|
function a'int a : int
|
|
|
|
constant a'maxInt : int = 46
|
|
|
|
constant a'minInt : int = 22
|
|
|
|
predicate a'eq (a:a) (b:a) = a'int a = a'int b
|
|
|
|
axiom a'inj : forall a:a, b:a. a'eq a b -> a = b
|
|
|
|
(* meta range_type type a, function a'int *)
|
|
|
|
(* meta model_projection function a'int *)
|
|
|
|
(* meta remove_unused:dependency prop a'inj, predicate a'eq *)
|
|
|
|
goal f2'vc : let result'unused = True in false
|
|
|
|
goal f3'vc : forall b:a. let _result'unused = b in a'int b = 42
|
|
|
|
goal f1'vc :
|
|
forall b:a. a'int b = 42 -> (let result'unused = (42:a) in 42 = a'int b)
|
|
|
|
end
|
|
|
|
theory Test1
|
|
|
|
(* use why3.BuiltIn.BuiltIn *)
|
|
|
|
(* use why3.Bool.Bool *)
|
|
|
|
(* use why3.Unit.Unit *)
|
|
|
|
(* use int.Int *)
|
|
|
|
type a1 = <range 22 46>
|
|
|
|
function a'int1 a1 : int
|
|
|
|
constant a'maxInt1 : int = 46
|
|
|
|
constant a'minInt1 : int = 22
|
|
|
|
predicate a'eq1 (a:a1) (b:a1) = a'int1 a = a'int1 b
|
|
|
|
axiom a'inj1 : forall a:a1, b:a1. a'eq1 a b -> a = b
|
|
|
|
(* meta range_type type a1, function a'int1 *)
|
|
|
|
(* meta model_projection function a'int1 *)
|
|
|
|
(* meta remove_unused:dependency prop a'inj1, predicate a'eq1 *)
|
|
|
|
(* clone Test with type a = a1, predicate a'eq = a'eq1,
|
|
constant a'minInt = a'minInt1, constant a'maxInt = a'maxInt1,
|
|
function a'int = a'int1, *)
|
|
|
|
end
|
|
|
|
Tasks are:
|
|
== Task 1 ==
|
|
|
|
theory Task
|
|
|
|
type int
|
|
|
|
type real
|
|
|
|
type string
|
|
|
|
predicate (=) 'a 'a
|
|
|
|
(* use why3.BuiltIn.BuiltIn *)
|
|
|
|
type bool =
|
|
| True
|
|
| False
|
|
|
|
(* use why3.Bool.Bool *)
|
|
|
|
type tuple0 =
|
|
| Tuple0
|
|
|
|
(* use why3.Tuple0.Tuple01 *)
|
|
|
|
type unit = unit
|
|
|
|
(* use why3.Unit.Unit *)
|
|
|
|
constant zero : int = 0
|
|
|
|
constant one : int = 1
|
|
|
|
function (-_) int : int
|
|
|
|
function (+) int int : int
|
|
|
|
function ( * ) int int : int
|
|
|
|
predicate (<) int int
|
|
|
|
function (-) (x:int) (y:int) : int = x + (- y)
|
|
|
|
predicate (>) (x:int) (y:int) = y < x
|
|
|
|
predicate (<=) (x:int) (y:int) = x < y \/ x = y
|
|
|
|
predicate (>=) (x:int) (y:int) = y <= x
|
|
|
|
axiom Assoc : forall x:int, y:int, z:int. ((x + y) + z) = (x + (y + z))
|
|
|
|
(* clone algebra.Assoc with type t = int, function op = (+),
|
|
prop Assoc1 = Assoc, *)
|
|
|
|
axiom Unit_def_l : forall x:int. (zero + x) = x
|
|
|
|
axiom Unit_def_r : forall x:int. (x + zero) = x
|
|
|
|
(* clone algebra.Monoid with type t1 = int, constant unit = zero,
|
|
function op1 = (+), prop Unit_def_r1 = Unit_def_r,
|
|
prop Unit_def_l1 = Unit_def_l, prop Assoc2 = Assoc, *)
|
|
|
|
axiom Inv_def_l : forall x:int. ((- x) + x) = zero
|
|
|
|
axiom Inv_def_r : forall x:int. (x + (- x)) = zero
|
|
|
|
(* clone algebra.Group with type t2 = int, function inv = (-_),
|
|
constant unit1 = zero, function op2 = (+), prop Inv_def_r1 = Inv_def_r,
|
|
prop Inv_def_l1 = Inv_def_l, prop Unit_def_r2 = Unit_def_r,
|
|
prop Unit_def_l2 = Unit_def_l, prop Assoc3 = Assoc, *)
|
|
|
|
axiom Comm : forall x:int, y:int. (x + y) = (y + x)
|
|
|
|
(* clone algebra.Comm with type t3 = int, function op3 = (+),
|
|
prop Comm1 = Comm, *)
|
|
|
|
(* meta AC function (+) *)
|
|
|
|
(* clone algebra.CommutativeGroup with type t4 = int, function inv1 = (-_),
|
|
constant unit2 = zero, function op4 = (+), prop Comm2 = Comm,
|
|
prop Inv_def_r2 = Inv_def_r, prop Inv_def_l2 = Inv_def_l,
|
|
prop Unit_def_r3 = Unit_def_r, prop Unit_def_l3 = Unit_def_l,
|
|
prop Assoc4 = Assoc, *)
|
|
|
|
axiom Assoc5 : forall x:int, y:int, z:int. ((x * y) * z) = (x * (y * z))
|
|
|
|
(* clone algebra.Assoc with type t = int, function op = ( * ),
|
|
prop Assoc1 = Assoc5, *)
|
|
|
|
axiom Mul_distr_l :
|
|
forall x:int, y:int, z:int. (x * (y + z)) = ((x * y) + (x * z))
|
|
|
|
axiom Mul_distr_r :
|
|
forall x:int, y:int, z:int. ((y + z) * x) = ((y * x) + (z * x))
|
|
|
|
(* clone algebra.Ring with type t5 = int, function ( *') = ( * ),
|
|
function (-'_) = (-_), function (+') = (+), constant zero1 = zero,
|
|
prop Mul_distr_r1 = Mul_distr_r, prop Mul_distr_l1 = Mul_distr_l,
|
|
prop Assoc6 = Assoc5, prop Comm3 = Comm, prop Inv_def_r3 = Inv_def_r,
|
|
prop Inv_def_l3 = Inv_def_l, prop Unit_def_r4 = Unit_def_r,
|
|
prop Unit_def_l4 = Unit_def_l, prop Assoc7 = Assoc, *)
|
|
|
|
axiom Comm4 : forall x:int, y:int. (x * y) = (y * x)
|
|
|
|
(* clone algebra.Comm with type t3 = int, function op3 = ( * ),
|
|
prop Comm1 = Comm4, *)
|
|
|
|
(* meta AC function ( * ) *)
|
|
|
|
(* clone algebra.CommutativeRing with type t6 = int,
|
|
function ( *'') = ( * ), function (-''_) = (-_), function (+'') = (+),
|
|
constant zero2 = zero, prop Comm5 = Comm4,
|
|
prop Mul_distr_r2 = Mul_distr_r, prop Mul_distr_l2 = Mul_distr_l,
|
|
prop Assoc8 = Assoc5, prop Comm6 = Comm, prop Inv_def_r4 = Inv_def_r,
|
|
prop Inv_def_l4 = Inv_def_l, prop Unit_def_r5 = Unit_def_r,
|
|
prop Unit_def_l5 = Unit_def_l, prop Assoc9 = Assoc, *)
|
|
|
|
axiom Unitary : forall x:int. (one * x) = x
|
|
|
|
axiom NonTrivialRing : not zero = one
|
|
|
|
(* clone algebra.UnitaryCommutativeRing with type t7 = int,
|
|
constant one1 = one, function ( *''') = ( * ), function (-'''_) = (-_),
|
|
function (+''') = (+), constant zero3 = zero,
|
|
prop NonTrivialRing1 = NonTrivialRing, prop Unitary1 = Unitary,
|
|
prop Comm7 = Comm4, prop Mul_distr_r3 = Mul_distr_r,
|
|
prop Mul_distr_l3 = Mul_distr_l, prop Assoc10 = Assoc5,
|
|
prop Comm8 = Comm, prop Inv_def_r5 = Inv_def_r,
|
|
prop Inv_def_l5 = Inv_def_l, prop Unit_def_r6 = Unit_def_r,
|
|
prop Unit_def_l6 = Unit_def_l, prop Assoc11 = Assoc, *)
|
|
|
|
(* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
|
|
*)
|
|
|
|
axiom Refl : forall x:int. x <= x
|
|
|
|
(* clone relations.Reflexive with type t9 = int, predicate rel1 = (<=),
|
|
prop Refl1 = Refl, *)
|
|
|
|
(* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
|
|
*)
|
|
|
|
axiom Trans : forall x:int, y:int, z:int. x <= y -> y <= z -> x <= z
|
|
|
|
(* clone relations.Transitive with type t10 = int, predicate rel2 = (<=),
|
|
prop Trans1 = Trans, *)
|
|
|
|
(* clone relations.PreOrder with type t11 = int, predicate rel3 = (<=),
|
|
prop Trans2 = Trans, prop Refl2 = Refl, *)
|
|
|
|
(* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
|
|
*)
|
|
|
|
axiom Antisymm : forall x:int, y:int. x <= y -> y <= x -> x = y
|
|
|
|
(* clone relations.Antisymmetric with type t12 = int,
|
|
predicate rel4 = (<=), prop Antisymm1 = Antisymm, *)
|
|
|
|
(* clone relations.PartialOrder with type t13 = int, predicate rel5 = (<=),
|
|
prop Antisymm2 = Antisymm, prop Trans3 = Trans, prop Refl3 = Refl, *)
|
|
|
|
(* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
|
|
*)
|
|
|
|
axiom Total : forall x:int, y:int. x <= y \/ y <= x
|
|
|
|
(* clone relations.Total with type t14 = int, predicate rel6 = (<=),
|
|
prop Total1 = Total, *)
|
|
|
|
(* clone relations.TotalOrder with type t15 = int, predicate rel7 = (<=),
|
|
prop Total2 = Total, prop Antisymm3 = Antisymm, prop Trans4 = Trans,
|
|
prop Refl4 = Refl, *)
|
|
|
|
axiom ZeroLessOne : zero <= one
|
|
|
|
axiom CompatOrderAdd :
|
|
forall x:int, y:int, z:int. x <= y -> (x + z) <= (y + z)
|
|
|
|
axiom CompatOrderMult :
|
|
forall x:int, y:int, z:int. x <= y -> zero <= z -> (x * z) <= (y * z)
|
|
|
|
(* meta remove_unused:dependency prop CompatOrderMult, function ( * ) *)
|
|
|
|
(* clone algebra.OrderedUnitaryCommutativeRing with type t16 = int,
|
|
predicate (<=') = (<=), constant one2 = one, function ( *'''') = ( * ),
|
|
function (-''''_) = (-_), function (+'''') = (+), constant zero4 = zero,
|
|
prop CompatOrderMult1 = CompatOrderMult,
|
|
prop CompatOrderAdd1 = CompatOrderAdd, prop ZeroLessOne1 = ZeroLessOne,
|
|
prop Total3 = Total, prop Antisymm4 = Antisymm, prop Trans5 = Trans,
|
|
prop Refl5 = Refl, prop NonTrivialRing2 = NonTrivialRing,
|
|
prop Unitary2 = Unitary, prop Comm9 = Comm4,
|
|
prop Mul_distr_r4 = Mul_distr_r, prop Mul_distr_l4 = Mul_distr_l,
|
|
prop Assoc12 = Assoc5, prop Comm10 = Comm, prop Inv_def_r6 = Inv_def_r,
|
|
prop Inv_def_l6 = Inv_def_l, prop Unit_def_r7 = Unit_def_r,
|
|
prop Unit_def_l7 = Unit_def_l, prop Assoc13 = Assoc, *)
|
|
|
|
(* meta remove_unused:keep function (+) *)
|
|
|
|
(* meta remove_unused:keep function (-) *)
|
|
|
|
(* meta remove_unused:keep function (-_) *)
|
|
|
|
(* meta remove_unused:keep predicate (<) *)
|
|
|
|
(* meta remove_unused:keep predicate (<=) *)
|
|
|
|
(* meta remove_unused:keep predicate (>) *)
|
|
|
|
(* meta remove_unused:keep predicate (>=) *)
|
|
|
|
(* use int.Int *)
|
|
|
|
type a = <range 22 46>
|
|
|
|
function a'int a : int
|
|
|
|
constant a'maxInt : int = 46
|
|
|
|
constant a'minInt : int = 22
|
|
|
|
predicate a'eq (a:a) (b:a) = a'int a = a'int b
|
|
|
|
axiom a'inj : forall a:a, b:a. a'eq a b -> a = b
|
|
|
|
(* meta range_type type a, function a'int *)
|
|
|
|
(* meta model_projection function a'int *)
|
|
|
|
(* meta remove_unused:dependency prop a'inj, predicate a'eq *)
|
|
|
|
(* clone Test with type a1 = a, predicate a'eq1 = a'eq,
|
|
constant a'minInt1 = a'minInt, constant a'maxInt1 = a'maxInt,
|
|
function a'int1 = a'int, prop a'inj1 = a'inj, *)
|
|
|
|
type a1 = <range 22 46>
|
|
|
|
function a'int1 a1 : int
|
|
|
|
constant a'maxInt1 : int = 46
|
|
|
|
constant a'minInt1 : int = 22
|
|
|
|
predicate a'eq1 (a:a1) (b:a1) = a'int1 a = a'int1 b
|
|
|
|
axiom a'inj1 : forall a:a1, b:a1. a'eq1 a b -> a = b
|
|
|
|
(* meta range_type type a1, function a'int1 *)
|
|
|
|
(* meta model_projection function a'int1 *)
|
|
|
|
(* meta remove_unused:dependency prop a'inj1, predicate a'eq1 *)
|
|
|
|
goal f2'vc : let result'unused = True in false
|
|
|
|
end
|
|
|
|
== Task 2 ==
|
|
|
|
theory Task
|
|
|
|
type int
|
|
|
|
type real
|
|
|
|
type string
|
|
|
|
predicate (=) 'a 'a
|
|
|
|
(* use why3.BuiltIn.BuiltIn *)
|
|
|
|
type bool =
|
|
| True
|
|
| False
|
|
|
|
(* use why3.Bool.Bool *)
|
|
|
|
type tuple0 =
|
|
| Tuple0
|
|
|
|
(* use why3.Tuple0.Tuple01 *)
|
|
|
|
type unit = unit
|
|
|
|
(* use why3.Unit.Unit *)
|
|
|
|
constant zero : int = 0
|
|
|
|
constant one : int = 1
|
|
|
|
function (-_) int : int
|
|
|
|
function (+) int int : int
|
|
|
|
function ( * ) int int : int
|
|
|
|
predicate (<) int int
|
|
|
|
function (-) (x:int) (y:int) : int = x + (- y)
|
|
|
|
predicate (>) (x:int) (y:int) = y < x
|
|
|
|
predicate (<=) (x:int) (y:int) = x < y \/ x = y
|
|
|
|
predicate (>=) (x:int) (y:int) = y <= x
|
|
|
|
axiom Assoc : forall x:int, y:int, z:int. ((x + y) + z) = (x + (y + z))
|
|
|
|
(* clone algebra.Assoc with type t = int, function op = (+),
|
|
prop Assoc1 = Assoc, *)
|
|
|
|
axiom Unit_def_l : forall x:int. (zero + x) = x
|
|
|
|
axiom Unit_def_r : forall x:int. (x + zero) = x
|
|
|
|
(* clone algebra.Monoid with type t1 = int, constant unit = zero,
|
|
function op1 = (+), prop Unit_def_r1 = Unit_def_r,
|
|
prop Unit_def_l1 = Unit_def_l, prop Assoc2 = Assoc, *)
|
|
|
|
axiom Inv_def_l : forall x:int. ((- x) + x) = zero
|
|
|
|
axiom Inv_def_r : forall x:int. (x + (- x)) = zero
|
|
|
|
(* clone algebra.Group with type t2 = int, function inv = (-_),
|
|
constant unit1 = zero, function op2 = (+), prop Inv_def_r1 = Inv_def_r,
|
|
prop Inv_def_l1 = Inv_def_l, prop Unit_def_r2 = Unit_def_r,
|
|
prop Unit_def_l2 = Unit_def_l, prop Assoc3 = Assoc, *)
|
|
|
|
axiom Comm : forall x:int, y:int. (x + y) = (y + x)
|
|
|
|
(* clone algebra.Comm with type t3 = int, function op3 = (+),
|
|
prop Comm1 = Comm, *)
|
|
|
|
(* meta AC function (+) *)
|
|
|
|
(* clone algebra.CommutativeGroup with type t4 = int, function inv1 = (-_),
|
|
constant unit2 = zero, function op4 = (+), prop Comm2 = Comm,
|
|
prop Inv_def_r2 = Inv_def_r, prop Inv_def_l2 = Inv_def_l,
|
|
prop Unit_def_r3 = Unit_def_r, prop Unit_def_l3 = Unit_def_l,
|
|
prop Assoc4 = Assoc, *)
|
|
|
|
axiom Assoc5 : forall x:int, y:int, z:int. ((x * y) * z) = (x * (y * z))
|
|
|
|
(* clone algebra.Assoc with type t = int, function op = ( * ),
|
|
prop Assoc1 = Assoc5, *)
|
|
|
|
axiom Mul_distr_l :
|
|
forall x:int, y:int, z:int. (x * (y + z)) = ((x * y) + (x * z))
|
|
|
|
axiom Mul_distr_r :
|
|
forall x:int, y:int, z:int. ((y + z) * x) = ((y * x) + (z * x))
|
|
|
|
(* clone algebra.Ring with type t5 = int, function ( *') = ( * ),
|
|
function (-'_) = (-_), function (+') = (+), constant zero1 = zero,
|
|
prop Mul_distr_r1 = Mul_distr_r, prop Mul_distr_l1 = Mul_distr_l,
|
|
prop Assoc6 = Assoc5, prop Comm3 = Comm, prop Inv_def_r3 = Inv_def_r,
|
|
prop Inv_def_l3 = Inv_def_l, prop Unit_def_r4 = Unit_def_r,
|
|
prop Unit_def_l4 = Unit_def_l, prop Assoc7 = Assoc, *)
|
|
|
|
axiom Comm4 : forall x:int, y:int. (x * y) = (y * x)
|
|
|
|
(* clone algebra.Comm with type t3 = int, function op3 = ( * ),
|
|
prop Comm1 = Comm4, *)
|
|
|
|
(* meta AC function ( * ) *)
|
|
|
|
(* clone algebra.CommutativeRing with type t6 = int,
|
|
function ( *'') = ( * ), function (-''_) = (-_), function (+'') = (+),
|
|
constant zero2 = zero, prop Comm5 = Comm4,
|
|
prop Mul_distr_r2 = Mul_distr_r, prop Mul_distr_l2 = Mul_distr_l,
|
|
prop Assoc8 = Assoc5, prop Comm6 = Comm, prop Inv_def_r4 = Inv_def_r,
|
|
prop Inv_def_l4 = Inv_def_l, prop Unit_def_r5 = Unit_def_r,
|
|
prop Unit_def_l5 = Unit_def_l, prop Assoc9 = Assoc, *)
|
|
|
|
axiom Unitary : forall x:int. (one * x) = x
|
|
|
|
axiom NonTrivialRing : not zero = one
|
|
|
|
(* clone algebra.UnitaryCommutativeRing with type t7 = int,
|
|
constant one1 = one, function ( *''') = ( * ), function (-'''_) = (-_),
|
|
function (+''') = (+), constant zero3 = zero,
|
|
prop NonTrivialRing1 = NonTrivialRing, prop Unitary1 = Unitary,
|
|
prop Comm7 = Comm4, prop Mul_distr_r3 = Mul_distr_r,
|
|
prop Mul_distr_l3 = Mul_distr_l, prop Assoc10 = Assoc5,
|
|
prop Comm8 = Comm, prop Inv_def_r5 = Inv_def_r,
|
|
prop Inv_def_l5 = Inv_def_l, prop Unit_def_r6 = Unit_def_r,
|
|
prop Unit_def_l6 = Unit_def_l, prop Assoc11 = Assoc, *)
|
|
|
|
(* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
|
|
*)
|
|
|
|
axiom Refl : forall x:int. x <= x
|
|
|
|
(* clone relations.Reflexive with type t9 = int, predicate rel1 = (<=),
|
|
prop Refl1 = Refl, *)
|
|
|
|
(* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
|
|
*)
|
|
|
|
axiom Trans : forall x:int, y:int, z:int. x <= y -> y <= z -> x <= z
|
|
|
|
(* clone relations.Transitive with type t10 = int, predicate rel2 = (<=),
|
|
prop Trans1 = Trans, *)
|
|
|
|
(* clone relations.PreOrder with type t11 = int, predicate rel3 = (<=),
|
|
prop Trans2 = Trans, prop Refl2 = Refl, *)
|
|
|
|
(* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
|
|
*)
|
|
|
|
axiom Antisymm : forall x:int, y:int. x <= y -> y <= x -> x = y
|
|
|
|
(* clone relations.Antisymmetric with type t12 = int,
|
|
predicate rel4 = (<=), prop Antisymm1 = Antisymm, *)
|
|
|
|
(* clone relations.PartialOrder with type t13 = int, predicate rel5 = (<=),
|
|
prop Antisymm2 = Antisymm, prop Trans3 = Trans, prop Refl3 = Refl, *)
|
|
|
|
(* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
|
|
*)
|
|
|
|
axiom Total : forall x:int, y:int. x <= y \/ y <= x
|
|
|
|
(* clone relations.Total with type t14 = int, predicate rel6 = (<=),
|
|
prop Total1 = Total, *)
|
|
|
|
(* clone relations.TotalOrder with type t15 = int, predicate rel7 = (<=),
|
|
prop Total2 = Total, prop Antisymm3 = Antisymm, prop Trans4 = Trans,
|
|
prop Refl4 = Refl, *)
|
|
|
|
axiom ZeroLessOne : zero <= one
|
|
|
|
axiom CompatOrderAdd :
|
|
forall x:int, y:int, z:int. x <= y -> (x + z) <= (y + z)
|
|
|
|
axiom CompatOrderMult :
|
|
forall x:int, y:int, z:int. x <= y -> zero <= z -> (x * z) <= (y * z)
|
|
|
|
(* meta remove_unused:dependency prop CompatOrderMult, function ( * ) *)
|
|
|
|
(* clone algebra.OrderedUnitaryCommutativeRing with type t16 = int,
|
|
predicate (<=') = (<=), constant one2 = one, function ( *'''') = ( * ),
|
|
function (-''''_) = (-_), function (+'''') = (+), constant zero4 = zero,
|
|
prop CompatOrderMult1 = CompatOrderMult,
|
|
prop CompatOrderAdd1 = CompatOrderAdd, prop ZeroLessOne1 = ZeroLessOne,
|
|
prop Total3 = Total, prop Antisymm4 = Antisymm, prop Trans5 = Trans,
|
|
prop Refl5 = Refl, prop NonTrivialRing2 = NonTrivialRing,
|
|
prop Unitary2 = Unitary, prop Comm9 = Comm4,
|
|
prop Mul_distr_r4 = Mul_distr_r, prop Mul_distr_l4 = Mul_distr_l,
|
|
prop Assoc12 = Assoc5, prop Comm10 = Comm, prop Inv_def_r6 = Inv_def_r,
|
|
prop Inv_def_l6 = Inv_def_l, prop Unit_def_r7 = Unit_def_r,
|
|
prop Unit_def_l7 = Unit_def_l, prop Assoc13 = Assoc, *)
|
|
|
|
(* meta remove_unused:keep function (+) *)
|
|
|
|
(* meta remove_unused:keep function (-) *)
|
|
|
|
(* meta remove_unused:keep function (-_) *)
|
|
|
|
(* meta remove_unused:keep predicate (<) *)
|
|
|
|
(* meta remove_unused:keep predicate (<=) *)
|
|
|
|
(* meta remove_unused:keep predicate (>) *)
|
|
|
|
(* meta remove_unused:keep predicate (>=) *)
|
|
|
|
(* use int.Int *)
|
|
|
|
type a = <range 22 46>
|
|
|
|
function a'int a : int
|
|
|
|
constant a'maxInt : int = 46
|
|
|
|
constant a'minInt : int = 22
|
|
|
|
predicate a'eq (a:a) (b:a) = a'int a = a'int b
|
|
|
|
axiom a'inj : forall a:a, b:a. a'eq a b -> a = b
|
|
|
|
(* meta range_type type a, function a'int *)
|
|
|
|
(* meta model_projection function a'int *)
|
|
|
|
(* meta remove_unused:dependency prop a'inj, predicate a'eq *)
|
|
|
|
(* clone Test with type a1 = a, predicate a'eq1 = a'eq,
|
|
constant a'minInt1 = a'minInt, constant a'maxInt1 = a'maxInt,
|
|
function a'int1 = a'int, prop a'inj1 = a'inj, *)
|
|
|
|
type a1 = <range 22 46>
|
|
|
|
function a'int1 a1 : int
|
|
|
|
constant a'maxInt1 : int = 46
|
|
|
|
constant a'minInt1 : int = 22
|
|
|
|
predicate a'eq1 (a:a1) (b:a1) = a'int1 a = a'int1 b
|
|
|
|
axiom a'inj1 : forall a:a1, b:a1. a'eq1 a b -> a = b
|
|
|
|
(* meta range_type type a1, function a'int1 *)
|
|
|
|
(* meta model_projection function a'int1 *)
|
|
|
|
(* meta remove_unused:dependency prop a'inj1, predicate a'eq1 *)
|
|
|
|
goal f3'vc : forall b:a1. let _result'unused = b in a'int1 b = 42
|
|
|
|
end
|
|
|
|
== Task 3 ==
|
|
|
|
theory Task
|
|
|
|
type int
|
|
|
|
type real
|
|
|
|
type string
|
|
|
|
predicate (=) 'a 'a
|
|
|
|
(* use why3.BuiltIn.BuiltIn *)
|
|
|
|
type bool =
|
|
| True
|
|
| False
|
|
|
|
(* use why3.Bool.Bool *)
|
|
|
|
type tuple0 =
|
|
| Tuple0
|
|
|
|
(* use why3.Tuple0.Tuple01 *)
|
|
|
|
type unit = unit
|
|
|
|
(* use why3.Unit.Unit *)
|
|
|
|
constant zero : int = 0
|
|
|
|
constant one : int = 1
|
|
|
|
function (-_) int : int
|
|
|
|
function (+) int int : int
|
|
|
|
function ( * ) int int : int
|
|
|
|
predicate (<) int int
|
|
|
|
function (-) (x:int) (y:int) : int = x + (- y)
|
|
|
|
predicate (>) (x:int) (y:int) = y < x
|
|
|
|
predicate (<=) (x:int) (y:int) = x < y \/ x = y
|
|
|
|
predicate (>=) (x:int) (y:int) = y <= x
|
|
|
|
axiom Assoc : forall x:int, y:int, z:int. ((x + y) + z) = (x + (y + z))
|
|
|
|
(* clone algebra.Assoc with type t = int, function op = (+),
|
|
prop Assoc1 = Assoc, *)
|
|
|
|
axiom Unit_def_l : forall x:int. (zero + x) = x
|
|
|
|
axiom Unit_def_r : forall x:int. (x + zero) = x
|
|
|
|
(* clone algebra.Monoid with type t1 = int, constant unit = zero,
|
|
function op1 = (+), prop Unit_def_r1 = Unit_def_r,
|
|
prop Unit_def_l1 = Unit_def_l, prop Assoc2 = Assoc, *)
|
|
|
|
axiom Inv_def_l : forall x:int. ((- x) + x) = zero
|
|
|
|
axiom Inv_def_r : forall x:int. (x + (- x)) = zero
|
|
|
|
(* clone algebra.Group with type t2 = int, function inv = (-_),
|
|
constant unit1 = zero, function op2 = (+), prop Inv_def_r1 = Inv_def_r,
|
|
prop Inv_def_l1 = Inv_def_l, prop Unit_def_r2 = Unit_def_r,
|
|
prop Unit_def_l2 = Unit_def_l, prop Assoc3 = Assoc, *)
|
|
|
|
axiom Comm : forall x:int, y:int. (x + y) = (y + x)
|
|
|
|
(* clone algebra.Comm with type t3 = int, function op3 = (+),
|
|
prop Comm1 = Comm, *)
|
|
|
|
(* meta AC function (+) *)
|
|
|
|
(* clone algebra.CommutativeGroup with type t4 = int, function inv1 = (-_),
|
|
constant unit2 = zero, function op4 = (+), prop Comm2 = Comm,
|
|
prop Inv_def_r2 = Inv_def_r, prop Inv_def_l2 = Inv_def_l,
|
|
prop Unit_def_r3 = Unit_def_r, prop Unit_def_l3 = Unit_def_l,
|
|
prop Assoc4 = Assoc, *)
|
|
|
|
axiom Assoc5 : forall x:int, y:int, z:int. ((x * y) * z) = (x * (y * z))
|
|
|
|
(* clone algebra.Assoc with type t = int, function op = ( * ),
|
|
prop Assoc1 = Assoc5, *)
|
|
|
|
axiom Mul_distr_l :
|
|
forall x:int, y:int, z:int. (x * (y + z)) = ((x * y) + (x * z))
|
|
|
|
axiom Mul_distr_r :
|
|
forall x:int, y:int, z:int. ((y + z) * x) = ((y * x) + (z * x))
|
|
|
|
(* clone algebra.Ring with type t5 = int, function ( *') = ( * ),
|
|
function (-'_) = (-_), function (+') = (+), constant zero1 = zero,
|
|
prop Mul_distr_r1 = Mul_distr_r, prop Mul_distr_l1 = Mul_distr_l,
|
|
prop Assoc6 = Assoc5, prop Comm3 = Comm, prop Inv_def_r3 = Inv_def_r,
|
|
prop Inv_def_l3 = Inv_def_l, prop Unit_def_r4 = Unit_def_r,
|
|
prop Unit_def_l4 = Unit_def_l, prop Assoc7 = Assoc, *)
|
|
|
|
axiom Comm4 : forall x:int, y:int. (x * y) = (y * x)
|
|
|
|
(* clone algebra.Comm with type t3 = int, function op3 = ( * ),
|
|
prop Comm1 = Comm4, *)
|
|
|
|
(* meta AC function ( * ) *)
|
|
|
|
(* clone algebra.CommutativeRing with type t6 = int,
|
|
function ( *'') = ( * ), function (-''_) = (-_), function (+'') = (+),
|
|
constant zero2 = zero, prop Comm5 = Comm4,
|
|
prop Mul_distr_r2 = Mul_distr_r, prop Mul_distr_l2 = Mul_distr_l,
|
|
prop Assoc8 = Assoc5, prop Comm6 = Comm, prop Inv_def_r4 = Inv_def_r,
|
|
prop Inv_def_l4 = Inv_def_l, prop Unit_def_r5 = Unit_def_r,
|
|
prop Unit_def_l5 = Unit_def_l, prop Assoc9 = Assoc, *)
|
|
|
|
axiom Unitary : forall x:int. (one * x) = x
|
|
|
|
axiom NonTrivialRing : not zero = one
|
|
|
|
(* clone algebra.UnitaryCommutativeRing with type t7 = int,
|
|
constant one1 = one, function ( *''') = ( * ), function (-'''_) = (-_),
|
|
function (+''') = (+), constant zero3 = zero,
|
|
prop NonTrivialRing1 = NonTrivialRing, prop Unitary1 = Unitary,
|
|
prop Comm7 = Comm4, prop Mul_distr_r3 = Mul_distr_r,
|
|
prop Mul_distr_l3 = Mul_distr_l, prop Assoc10 = Assoc5,
|
|
prop Comm8 = Comm, prop Inv_def_r5 = Inv_def_r,
|
|
prop Inv_def_l5 = Inv_def_l, prop Unit_def_r6 = Unit_def_r,
|
|
prop Unit_def_l6 = Unit_def_l, prop Assoc11 = Assoc, *)
|
|
|
|
(* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
|
|
*)
|
|
|
|
axiom Refl : forall x:int. x <= x
|
|
|
|
(* clone relations.Reflexive with type t9 = int, predicate rel1 = (<=),
|
|
prop Refl1 = Refl, *)
|
|
|
|
(* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
|
|
*)
|
|
|
|
axiom Trans : forall x:int, y:int, z:int. x <= y -> y <= z -> x <= z
|
|
|
|
(* clone relations.Transitive with type t10 = int, predicate rel2 = (<=),
|
|
prop Trans1 = Trans, *)
|
|
|
|
(* clone relations.PreOrder with type t11 = int, predicate rel3 = (<=),
|
|
prop Trans2 = Trans, prop Refl2 = Refl, *)
|
|
|
|
(* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
|
|
*)
|
|
|
|
axiom Antisymm : forall x:int, y:int. x <= y -> y <= x -> x = y
|
|
|
|
(* clone relations.Antisymmetric with type t12 = int,
|
|
predicate rel4 = (<=), prop Antisymm1 = Antisymm, *)
|
|
|
|
(* clone relations.PartialOrder with type t13 = int, predicate rel5 = (<=),
|
|
prop Antisymm2 = Antisymm, prop Trans3 = Trans, prop Refl3 = Refl, *)
|
|
|
|
(* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
|
|
*)
|
|
|
|
axiom Total : forall x:int, y:int. x <= y \/ y <= x
|
|
|
|
(* clone relations.Total with type t14 = int, predicate rel6 = (<=),
|
|
prop Total1 = Total, *)
|
|
|
|
(* clone relations.TotalOrder with type t15 = int, predicate rel7 = (<=),
|
|
prop Total2 = Total, prop Antisymm3 = Antisymm, prop Trans4 = Trans,
|
|
prop Refl4 = Refl, *)
|
|
|
|
axiom ZeroLessOne : zero <= one
|
|
|
|
axiom CompatOrderAdd :
|
|
forall x:int, y:int, z:int. x <= y -> (x + z) <= (y + z)
|
|
|
|
axiom CompatOrderMult :
|
|
forall x:int, y:int, z:int. x <= y -> zero <= z -> (x * z) <= (y * z)
|
|
|
|
(* meta remove_unused:dependency prop CompatOrderMult, function ( * ) *)
|
|
|
|
(* clone algebra.OrderedUnitaryCommutativeRing with type t16 = int,
|
|
predicate (<=') = (<=), constant one2 = one, function ( *'''') = ( * ),
|
|
function (-''''_) = (-_), function (+'''') = (+), constant zero4 = zero,
|
|
prop CompatOrderMult1 = CompatOrderMult,
|
|
prop CompatOrderAdd1 = CompatOrderAdd, prop ZeroLessOne1 = ZeroLessOne,
|
|
prop Total3 = Total, prop Antisymm4 = Antisymm, prop Trans5 = Trans,
|
|
prop Refl5 = Refl, prop NonTrivialRing2 = NonTrivialRing,
|
|
prop Unitary2 = Unitary, prop Comm9 = Comm4,
|
|
prop Mul_distr_r4 = Mul_distr_r, prop Mul_distr_l4 = Mul_distr_l,
|
|
prop Assoc12 = Assoc5, prop Comm10 = Comm, prop Inv_def_r6 = Inv_def_r,
|
|
prop Inv_def_l6 = Inv_def_l, prop Unit_def_r7 = Unit_def_r,
|
|
prop Unit_def_l7 = Unit_def_l, prop Assoc13 = Assoc, *)
|
|
|
|
(* meta remove_unused:keep function (+) *)
|
|
|
|
(* meta remove_unused:keep function (-) *)
|
|
|
|
(* meta remove_unused:keep function (-_) *)
|
|
|
|
(* meta remove_unused:keep predicate (<) *)
|
|
|
|
(* meta remove_unused:keep predicate (<=) *)
|
|
|
|
(* meta remove_unused:keep predicate (>) *)
|
|
|
|
(* meta remove_unused:keep predicate (>=) *)
|
|
|
|
(* use int.Int *)
|
|
|
|
type a = <range 22 46>
|
|
|
|
function a'int a : int
|
|
|
|
constant a'maxInt : int = 46
|
|
|
|
constant a'minInt : int = 22
|
|
|
|
predicate a'eq (a:a) (b:a) = a'int a = a'int b
|
|
|
|
axiom a'inj : forall a:a, b:a. a'eq a b -> a = b
|
|
|
|
(* meta range_type type a, function a'int *)
|
|
|
|
(* meta model_projection function a'int *)
|
|
|
|
(* meta remove_unused:dependency prop a'inj, predicate a'eq *)
|
|
|
|
(* clone Test with type a1 = a, predicate a'eq1 = a'eq,
|
|
constant a'minInt1 = a'minInt, constant a'maxInt1 = a'maxInt,
|
|
function a'int1 = a'int, prop a'inj1 = a'inj, *)
|
|
|
|
type a1 = <range 22 46>
|
|
|
|
function a'int1 a1 : int
|
|
|
|
constant a'maxInt1 : int = 46
|
|
|
|
constant a'minInt1 : int = 22
|
|
|
|
predicate a'eq1 (a:a1) (b:a1) = a'int1 a = a'int1 b
|
|
|
|
axiom a'inj1 : forall a:a1, b:a1. a'eq1 a b -> a = b
|
|
|
|
(* meta range_type type a1, function a'int1 *)
|
|
|
|
(* meta model_projection function a'int1 *)
|
|
|
|
(* meta remove_unused:dependency prop a'inj1, predicate a'eq1 *)
|
|
|
|
goal f1'vc :
|
|
forall b:a1.
|
|
a'int1 b = 42 -> (let result'unused = (42:a1) in 42 = a'int1 b)
|
|
|
|
end
|
|
|