Sets, typed

def Cvc.Typed.Term.setInsert [Ω] {α : Type} [Ord α] (elm : Term α) (s : Term (Set α)) : Env (Term (Set α))

Inserts elm into s; the element comes first, as in cvc5.

Equations

• elm.setInsert s = Cvc.Untyped.Term.setInsert elm s

def Cvc.Typed.Term.setInter [Ω] {α : Type} [Ord α] (lft rgt : Term (Set α)) : Env (Term (Set α))

Set intersection.

Equations

• lft.setInter rgt = Cvc.Untyped.Term.setInter lft rgt

def Cvc.Typed.Term.setAll [Ω] {α : Type} [Ord α] (p : Term (α → Bool)) (s : Term (Set α)) : Env (Term Bool)

Whether every element of a set satisfies a predicate.

Equations

• p.setAll s = Cvc.Untyped.Term.setAll p s

def Cvc.Typed.Term.setSingleton [Ω] {α : Type} [Ord α] (elm : Term α) : Env (Term (Set α))

The singleton set containing one element.

Equations

• elm.setSingleton = Cvc.Untyped.Term.setSingleton elm

def Cvc.Typed.Term.setFilter [Ω] {α : Type} [Ord α] (p : Term (α → Bool)) (s : Term (Set α)) : Env (Term (Set α))

The elements of a set satisfying a predicate.

Equations

• p.setFilter s = Cvc.Untyped.Term.setFilter p s

def Cvc.Typed.Term.setInterN [Ω] {α : Type} [Ord α] (terms : Terms (Set α)) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env (Term (Set α))

setInter over two or more terms.

Equations

• Cvc.Typed.Term.setInterN terms atLeastTwoElements = Cvc.Untyped.Term.setInterN terms atLeastTwoElements

def Cvc.Typed.Term.setIsSingleton [Ω] {α : Type} [Ord α] (s : Term (Set α)) : Env (Term Bool)

Whether s has exactly one element.

Equations

• s.setIsSingleton = Cvc.Untyped.Term.setIsSingleton s

def Cvc.Typed.Term.setCard [Ω] {α : Type} [Ord α] (s : Term (Set α)) : Env (Term Int)

Cardinality.

Equations

• s.setCard = Cvc.Untyped.Term.setCard s

def Cvc.Typed.Term.setUniverse [Ω] {α : Type} [Ord α] [ToTyp α] : Env (Term (Set α))

The set of every element of sort α.

Equations

• Cvc.Typed.Term.setUniverse = do let srtOfα ← Cvc.Srt.of α Cvc.Untyped.Term.setUniverse srtOfα

def Cvc.Typed.Term.setComplement [Ω] {α : Type} [Ord α] (s : Term (Set α)) : Env (Term (Set α))

Set complement, relative to the universe set of the element sort.

Equations

• s.setComplement = Cvc.Untyped.Term.setComplement s

def Cvc.Typed.Term.setUnion [Ω] {α : Type} [Ord α] (lft rgt : Term (Set α)) : Env (Term (Set α))

Set union.

Equations

• lft.setUnion rgt = Cvc.Untyped.Term.setUnion lft rgt

def Cvc.Typed.Term.setFold [Ω] {α β : Type} [Ord α] (f : Term (α → β → β)) (init : Term β) (s : Term (Set α)) : Env (Term β)

Folds f over the elements of s from init, in no specified order.

Equations

• f.setFold init s = Cvc.Untyped.Term.setFold f init s

def Cvc.Typed.Term.setMinus [Ω] {α : Type} [Ord α] (lft rgt : Term (Set α)) : Env (Term (Set α))

Set difference.

Equations

• lft.setMinus rgt = Cvc.Untyped.Term.setMinus lft rgt

def Cvc.Typed.Term.setIsEmpty [Ω] {α : Type} [Ord α] (s : Term (Set α)) : Env (Term Bool)

Whether s is empty.

Equations

• s.setIsEmpty = Cvc.Untyped.Term.setIsEmpty s

def Cvc.Typed.Term.setEmpty [Ω] {α : Type} [Ord α] [ToTyp α] : Env (Term (Set α))

The empty set of elements of sort α.

Equations

• Cvc.Typed.Term.setEmpty = do let srtOfα ← Cvc.Srt.of α Cvc.Untyped.Term.setEmpty srtOfα

def Cvc.Typed.Term.setUnionN [Ω] {α : Type} [Ord α] (terms : Terms (Set α)) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env (Term (Set α))

setUnion over two or more terms.

Equations

• Cvc.Typed.Term.setUnionN terms atLeastTwoElements = Cvc.Untyped.Term.setUnionN terms atLeastTwoElements

def Cvc.Typed.Term.setMap [Ω] {α β : Type} [Ord α] [Ord β] (f : Term (α → β)) (s : Term (Set α)) : Env (Term (Set β))

The image of a set under a function.

Equations

• f.setMap s = Cvc.Untyped.Term.setMap f s

def Cvc.Typed.Term.setSome [Ω] {α : Type} [Ord α] (p : Term (α → Bool)) (s : Term (Set α)) : Env (Term Bool)

Whether some element of a set satisfies a predicate.

Equations

• p.setSome s = Cvc.Untyped.Term.setSome p s

def Cvc.Typed.Term.setMinusN [Ω] {α : Type} [Ord α] (terms : Terms (Set α)) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env (Term (Set α))

setMinus over two or more terms.

Equations

• Cvc.Typed.Term.setMinusN terms atLeastTwoElements = Cvc.Untyped.Term.setMinusN terms atLeastTwoElements

def Cvc.Typed.Term.setChoose [Ω] {α : Type} [Ord α] (s : Term (Set α)) : Env (Term α)

An unspecified element of a non-empty set.

Equations

• s.setChoose = Cvc.Untyped.Term.setChoose s

def Cvc.Typed.Term.setMember [Ω] {α : Type} [Ord α] (elm : Term α) (s : Term (Set α)) : Env (Term Bool)

Whether elm is in s; the element comes first, as in cvc5.

Equations

• elm.setMember s = Cvc.Untyped.Term.setMember elm s

def Cvc.Typed.Term.setSubset [Ω] {α : Type} [Ord α] (lft rgt : Term (Set α)) : Env (Term Bool)

Whether lft is a subset of rgt.

Equations

• lft.setSubset rgt = Cvc.Untyped.Term.setSubset lft rgt

inductive Cvc.Typed.View.Set.OnBool [Ω] : Type

Set's operators with a result of sort Bool.

• setMember [Ω] (α : Typ) (elm : Term α.Denote) (s : Term (Typ.set (Typ?.typ α)).Denote) : OnBool

  Whether elm is in s; the element comes first, as in cvc5.

• setSubset [Ω] (α : Typ) (lft rgt : Term (Typ.set (Typ?.typ α)).Denote) : OnBool

  Whether lft is a subset of rgt.

• setIsEmpty [Ω] (α : Typ) (s : Term (Typ.set (Typ?.typ α)).Denote) : OnBool

  Whether s is empty.

• setIsSingleton [Ω] (α : Typ) (s : Term (Typ.set (Typ?.typ α)).Denote) : OnBool

  Whether s has exactly one element.

• setAll [Ω] (α : Typ) (p : Term (α.function (Typ?.typ Typ.bool)).Denote) (s : Term (Typ.set (Typ?.typ α)).Denote) : OnBool

  Whether every element of a set satisfies a predicate.

• setSome [Ω] (α : Typ) (p : Term (α.function (Typ?.typ Typ.bool)).Denote) (s : Term (Typ.set (Typ?.typ α)).Denote) : OnBool

  Whether some element of a set satisfies a predicate.

def Cvc.Typed.View.Set.of [Ω] (τ : Typ) (t : Term τ.Denote) : Env (Option (View.Set τ))

Takes a term apart one level, at its sort, if Set owns its operator and the term's sort fits it.

Equations

• One or more equations did not get rendered due to their size.

inductive Cvc.Typed.View.Set.OnInt [Ω] : Type

Set's operators with a result of sort Int.

• setCard [Ω] (α : Typ) (s : Term (Typ.set (Typ?.typ α)).Denote) : OnInt

  Cardinality.

inductive Cvc.Typed.View.Set.OnAny [Ω] (β : Type) [ToTyp β] : Type

Set's operators whose result's sort is a type variable.

• setChoose [Ω] {β : Type} [ToTyp β] (s : Term (Typ.set (Typ?.typ (Typ.of β))).Denote) : OnAny β

  An unspecified element of a non-empty set.

• setFold [Ω] {β : Type} [ToTyp β] (α : Typ) (f : Term (α.function (Typ?.typ ((Typ.of β).function (Typ?.typ (Typ.of β))))).Denote) (init : Term β) (s : Term (Typ.set (Typ?.typ α)).Denote) : OnAny β

  Folds f over the elements of s from init, in no specified order.

inductive Cvc.Typed.View.Set.OnSet [Ω] (γ : Type) [Ord γ] [ToTyp γ] : Type

Set's operators with a result of sort Set.

• setSingleton [Ω] {γ : Type} [Ord γ] [ToTyp γ] (elm : Term γ) : OnSet γ

  The singleton set containing one element.

• setInsert [Ω] {γ : Type} [Ord γ] [ToTyp γ] (elm : Term γ) (s : Term (Set γ)) : OnSet γ

  Inserts elm into s; the element comes first, as in cvc5.

• setUnion [Ω] {γ : Type} [Ord γ] [ToTyp γ] (kids : Kids (Set γ)) : OnSet γ

  Set union.

  kids holds every operand, two or more.

• setInter [Ω] {γ : Type} [Ord γ] [ToTyp γ] (kids : Kids (Set γ)) : OnSet γ

  Set intersection.

  kids holds every operand, two or more.

• setMinus [Ω] {γ : Type} [Ord γ] [ToTyp γ] (kids : Kids (Set γ)) : OnSet γ

  Set difference.

  kids holds every operand, two or more.

• setComplement [Ω] {γ : Type} [Ord γ] [ToTyp γ] (s : Term (Set γ)) : OnSet γ

  Set complement, relative to the universe set of the element sort.

• setMap [Ω] {γ : Type} [Ord γ] [ToTyp γ] (α : Typ) (f : Term (α.function (Typ?.typ (Typ.of γ))).Denote) (s : Term (Typ.set (Typ?.typ α)).Denote) : OnSet γ

  The image of a set under a function.

• setFilter [Ω] {γ : Type} [Ord γ] [ToTyp γ] (p : Term (γ → Bool)) (s : Term (Set γ)) : OnSet γ

  The elements of a set satisfying a predicate.

• setEmpty [Ω] {γ : Type} [Ord γ] [ToTyp γ] : OnSet γ

  The empty set of elements of sort α.

• setUniverse [Ω] {γ : Type} [Ord γ] [ToTyp γ] : OnSet γ

  The set of every element of sort α.

inductive Cvc.Typed.View.Set [Ω] : Typ → Type

Set's operators, taken apart one level, indexed by the sort each produces.

• bool [Ω] : OnBool → View.Set Typ.bool

  An operator with a result of sort Bool.

• set [Ω] (γ : Typ) [Ord γ.Denote] : OnSet γ.Denote → View.Set (Typ.set (Typ?.typ γ))

  An operator with a result of sort Set.

• int [Ω] : OnInt → View.Set Typ.int

  An operator with a result of sort Int.

• any [Ω] {τ : Typ} : OnAny τ.Denote → View.Set τ

  An operator whose result's sort is a type variable.

Values

def Cvc.Typed.Term.isSetValue [Ω] {α : Type} [Ord α] (term : Term (Set α)) : Bool

Whether a term is a set value: a canonical union of singletons of values, as a model answers.

A set built from constructors is generally not one, and the universe set never is.

Equations

• term.isSetValue = Cvc.Untyped.Term.isSetValue term

def Cvc.Typed.Term.mkSetValue {α : Type} [Ω] [Ord α] [ToTyp α] [ValueToTerm α] (set : Set α) : Env (Term (Set α))

The set term denoting a set of values.

Equations

• Cvc.Typed.Term.mkSetValue = Cvc.Untyped.Term.mkSetValue

def Cvc.Typed.Term.getSetValue {α : Type} [Ω] [Ord α] [TermToValue α] : Term (Set α) → Env (Set α)

The set of values a constant set term denotes.

Only a set value in cvc5's normal form, such as a model's answer, is accepted: a term built by mkSetValue is not one.

Equations

• Cvc.Typed.Term.getSetValue = Cvc.Untyped.Term.getSetValue

@[instance_reducible]

instance Cvc.Typed.Term.instValueToTermSet {α : Type} [Ord α] [ToTyp α] [ValueToTerm α] : ValueToTerm (Set α)

Equations

• Cvc.Typed.Term.instValueToTermSet = { valueToTerm := fun [Cvc.Ω] => Cvc.Typed.Term.mkSetValue }

@[instance_reducible]

instance Cvc.Typed.Term.instTermToValueSet {α : Type} [Ord α] [TermToValue α] : TermToValue (Set α)

Equations

• Cvc.Typed.Term.instTermToValueSet = { termToValue := fun [Cvc.Ω] => Cvc.Typed.Term.getSetValue }

Comprehension

{ elem | bvs. pred }, whose index is the element's: the bound variables' sorts do not reach the result. See Cvc.Untyped.Term.setComprehension for what cvc5 supports of it.

def Cvc.Typed.Term.setComprehension [Ω] {β : Type} [ToTyp β] [Ord β] (bvs : BVars) (pred : Term Bool) (elem : Term β) (_nonEmpty : bvs ≠ [] := by (try simp) <;> fail "failed to prove a comprehension binds at least one variable") : Env (Term (Set β))

The set of the values elem takes, over the bindings of bvs that satisfy pred.

Equations

• Cvc.Typed.Term.setComprehension bvs pred elem _nonEmpty = Cvc.Untyped.Term.setComprehension bvs.erase pred elem ⋯