Why3 Standard Library index



Relations


Relations and orders

theory EndoRelation
  type t
  predicate rel t t
end

theory Reflexive
  clone export EndoRelation
  axiom Refl : forall x:t. rel x x
end

theory Irreflexive
  clone export EndoRelation
  axiom Strict : forall x:t. not rel x x
end

theory Transitive
  clone export EndoRelation
  axiom Trans : forall x y z:t. rel x y -> rel y z -> rel x z
end

theory Symmetric
  clone export EndoRelation
  axiom Symm : forall x y:t. rel x y -> rel y x
end

theory Asymmetric
  clone export EndoRelation
  axiom Asymm : forall x y:t. rel x y -> not rel y x
end

theory Antisymmetric
  clone export EndoRelation
  axiom Antisymm : forall x y:t. rel x y -> rel y x -> x = y
end

theory Total
  clone export EndoRelation
  axiom Total : forall x y:t. rel x y \/ rel y x
end

theory PreOrder
  clone export Reflexive
  clone export Transitive with type t = t, predicate rel = rel
end

theory Equivalence
  clone export PreOrder
  clone export Symmetric with type t = t, predicate rel = rel
end

theory TotalPreOrder
  clone export PreOrder
  clone export Total with type t = t, predicate rel = rel
end

theory PartialOrder
  clone export PreOrder
  clone export Antisymmetric with type t = t, predicate rel = rel
end

theory TotalOrder
  clone export PartialOrder
  clone export Total with type t = t, predicate rel = rel
end

theory PartialStrictOrder
  clone export Transitive
  clone export Asymmetric with type t = t, predicate rel = rel
end

theory TotalStrictOrder
  clone export PartialStrictOrder
  axiom Trichotomy : forall x y:t. rel x y \/ rel y x \/ x = y
end

theory Inverse
  clone export EndoRelation

  predicate inv_rel (x y : t) = rel y x
end

Closures

theory ReflClosure
  clone export EndoRelation

  inductive relR t t =
  | BaseRefl : forall x:t. relR x x
  | StepRefl : forall x y:t. rel x y -> relR x y
end

theory TransClosure
  clone export EndoRelation

  inductive relT t t =
  | BaseTrans : forall x y:t. rel x y -> relT x y
  | StepTrans : forall x y z:t. relT x y -> rel y z -> relT x z

  lemma relT_transitive:
    forall x y z: t. relT x y -> relT y z -> relT x z
end

theory ReflTransClosure
  clone export EndoRelation

  inductive relTR t t =
  | BaseTransRefl : forall x:t. relTR x x
  | StepTransRefl : forall x y z:t. relTR x y -> rel y z -> relTR x z

  lemma relTR_transitive:
    forall x y z: t. relTR x y -> relTR y z -> relTR x z
end

Lexicographic ordering

theory Lex

  type t1
  type t2

  predicate rel1 t1 t1
  predicate rel2 t2 t2

  inductive lex (t1, t2) (t1, t2) =
  | Lex_1: forall x1 x2 : t1, y1 y2 : t2.
       rel1 x1 x2 -> lex (x1,y1) (x2,y2)
  | Lex_2: forall x : t1, y1 y2 : t2.
       rel2 y1 y2 -> lex (x,y1) (x,y2)

end

Minimum and maximum for total orders

theory MinMax

  type t
  predicate le t t

  clone TotalOrder with type t = t, predicate rel = le

  function min (x y : t) : t = if le x y then x else y
  function max (x y : t) : t = if le x y then y else x

  lemma Min_r : forall x y:t. le y x -> min x y = y
  lemma Max_l : forall x y:t. le y x -> max x y = x

  lemma Min_comm : forall x y:t. min x y = min y x
  lemma Max_comm : forall x y:t. max x y = max y x

  lemma Min_assoc : forall x y z:t. min (min x y) z = min x (min y z)
  lemma Max_assoc : forall x y z:t. max (max x y) z = max x (max y z)

end

Well-founded relation

theory WellFounded

  type t

  predicate r t t

  inductive acc (x: t) =
  | acc_x: forall x: t. (forall y: t. r y x -> acc y) -> acc x

  axiom well_founded: forall x: t. acc x

end

Generated by why3doc 0.88.0