Bags, typed

def Cvc.Typed.Term.bagFold [Ω] {α β : Type} [Ord α] (f : Term (α → β → β)) (init : Term β) (b : Term (Bag α)) : Env (Term β)

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

Equations

• f.bagFold init b = Cvc.Untyped.Term.bagFold f init b

def Cvc.Typed.Term.bagCount [Ω] {α : Type} [Ord α] (elm : Term α) (b : Term (Bag α)) : Env (Term Int)

Multiplicity of elm in b; the element comes first, as in cvc5.

Equations

• elm.bagCount b = Cvc.Untyped.Term.bagCount elm b

def Cvc.Typed.Term.bagMake [Ω] {α : Type} [Ord α] (elm : Term α) (count : Term Int) : Env (Term (Bag α))

The bag holding elm count times; the element comes first, as in cvc5.

Equations

• elm.bagMake count = Cvc.Untyped.Term.bagMake elm count

def Cvc.Typed.Term.bagAll [Ω] {α : Type} [Ord α] (p : Term (α → Bool)) (b : Term (Bag α)) : Env (Term Bool)

Whether every element of a bag satisfies a predicate.

Equations

• p.bagAll b = Cvc.Untyped.Term.bagAll p b

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

Difference removing every element occurring on the right.

Equations

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

def Cvc.Typed.Term.bagMap [Ω] {α β : Type} [Ord α] [Ord β] (f : Term (α → β)) (b : Term (Bag α)) : Env (Term (Bag β))

The image of a bag under a function.

Equations

• f.bagMap b = Cvc.Untyped.Term.bagMap f b

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

Union taking the maximum of the multiplicities.

Equations

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

def Cvc.Typed.Term.bagCard [Ω] {α : Type} [Ord α] (b : Term (Bag α)) : Env (Term Int)

Cardinality, counting multiplicities.

Equations

• b.bagCard = Cvc.Untyped.Term.bagCard b

def Cvc.Typed.Term.bagMember [Ω] {α : Type} [Ord α] (elm : Term α) (b : Term (Bag α)) : Env (Term Bool)

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

Equations

• elm.bagMember b = Cvc.Untyped.Term.bagMember elm b

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

bagInterMin over two or more terms.

Equations

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

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

The empty bag of elements of sort α.

Equations

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

def Cvc.Typed.Term.bagPartition [Ω] {α : Type} [Ord α] (p : Term (α → α → Bool)) (b : Term (Bag α)) : Env (Term (Bag (Bag α)))

Partitions a bag into the equivalence classes of a binary predicate.

The predicate is expected to be an equivalence relation; the result holds one bag per class.

Equations

• p.bagPartition b = Cvc.Untyped.Term.bagPartition p b

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

Intersection taking the minimum of the multiplicities.

Equations

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

def Cvc.Typed.Term.bagChoose [Ω] {α : Type} [Ord α] (b : Term (Bag α)) : Env (Term α)

An unspecified element of a non-empty bag.

Equations

• b.bagChoose = Cvc.Untyped.Term.bagChoose b

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

Difference subtracting the multiplicities.

Equations

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

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

bagUnionDisjoint over two or more terms.

Equations

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

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

Union adding the multiplicities.

Equations

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

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

bagUnionMax over two or more terms.

Equations

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

def Cvc.Typed.Term.bagFilter [Ω] {α : Type} [Ord α] (p : Term (α → Bool)) (b : Term (Bag α)) : Env (Term (Bag α))

The elements of a bag satisfying a predicate, with their multiplicities.

Equations

• p.bagFilter b = Cvc.Untyped.Term.bagFilter p b

def Cvc.Typed.Term.bagSetof [Ω] {α : Type} [Ord α] (b : Term (Bag α)) : Env (Term (Bag α))

Duplicate removal, yielding a bag whose multiplicities are all at most one.

Equations

• b.bagSetof = Cvc.Untyped.Term.bagSetof b

def Cvc.Typed.Term.bagSome [Ω] {α : Type} [Ord α] (p : Term (α → Bool)) (b : Term (Bag α)) : Env (Term Bool)

Whether some element of a bag satisfies a predicate.

Equations

• p.bagSome b = Cvc.Untyped.Term.bagSome p b

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

Whether every multiplicity in lft is at most the one in rgt.

Equations

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

inductive Cvc.Typed.View.Bag.OnBag [Ω] (γ : Type) [Ord γ] [ToTyp γ] : Type

Bag's operators with a result of sort Bag.

• bagMake [Ω] {γ : Type} [Ord γ] [ToTyp γ] (elm : Term γ) (count : Term Int) : OnBag γ

  The bag holding elm count times; the element comes first, as in cvc5.

• bagSetof [Ω] {γ : Type} [Ord γ] [ToTyp γ] (b : Term (Bag γ)) : OnBag γ

  Duplicate removal, yielding a bag whose multiplicities are all at most one.

• bagUnionMax [Ω] {γ : Type} [Ord γ] [ToTyp γ] (kids : Kids (Bag γ)) : OnBag γ

  Union taking the maximum of the multiplicities.

  kids holds every operand, two or more.

• bagUnionDisjoint [Ω] {γ : Type} [Ord γ] [ToTyp γ] (kids : Kids (Bag γ)) : OnBag γ

  Union adding the multiplicities.

  kids holds every operand, two or more.

• bagInterMin [Ω] {γ : Type} [Ord γ] [ToTyp γ] (kids : Kids (Bag γ)) : OnBag γ

  Intersection taking the minimum of the multiplicities.

  kids holds every operand, two or more.

• bagDifferenceSubtract [Ω] {γ : Type} [Ord γ] [ToTyp γ] (lft rgt : Term (Bag γ)) : OnBag γ

  Difference subtracting the multiplicities.

• bagDifferenceRemove [Ω] {γ : Type} [Ord γ] [ToTyp γ] (lft rgt : Term (Bag γ)) : OnBag γ

  Difference removing every element occurring on the right.

• bagMap [Ω] {γ : Type} [Ord γ] [ToTyp γ] (α : Typ) (f : Term (α.function (Typ?.typ (Typ.of γ))).Denote) (b : Term (Typ.bag (Typ?.typ α)).Denote) : OnBag γ

  The image of a bag under a function.

• bagFilter [Ω] {γ : Type} [Ord γ] [ToTyp γ] (p : Term (γ → Bool)) (b : Term (Bag γ)) : OnBag γ

  The elements of a bag satisfying a predicate, with their multiplicities.

• bagPartition [Ω] {γ : Type} [Ord γ] [ToTyp γ] (α : Typ) {h0 : Typ.of γ = Typ.bag (Typ?.typ α)} (p : Term (α.function (Typ?.typ (α.function (Typ?.typ Typ.bool)))).Denote) (b : Term (Typ.bag (Typ?.typ α)).Denote) : OnBag γ

  Partitions a bag into the equivalence classes of a binary predicate.

  The predicate is expected to be an equivalence relation; the result holds one bag per class.

• bagEmpty [Ω] {γ : Type} [Ord γ] [ToTyp γ] : OnBag γ

  The empty bag of elements of sort α.

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

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

• bagChoose [Ω] {β : Type} [ToTyp β] (b : Term (Typ.bag (Typ?.typ (Typ.of β))).Denote) : OnAny β

  An unspecified element of a non-empty bag.

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

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

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

Bag's operators with a result of sort Int.

• bagCount [Ω] (α : Typ) (elm : Term α.Denote) (b : Term (Typ.bag (Typ?.typ α)).Denote) : OnInt

  Multiplicity of elm in b; the element comes first, as in cvc5.

• bagCard [Ω] (α : Typ) (b : Term (Typ.bag (Typ?.typ α)).Denote) : OnInt

  Cardinality, counting multiplicities.

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

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

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

  An operator with a result of sort Bool.

• bag [Ω] (γ : Typ) [Ord γ.Denote] : OnBag γ.Denote → View.Bag (Typ.bag (Typ?.typ γ))

  An operator with a result of sort Bag.

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

  An operator with a result of sort Int.

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

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

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

Bag's operators with a result of sort Bool.

• bagMember [Ω] (α : Typ) (elm : Term α.Denote) (b : Term (Typ.bag (Typ?.typ α)).Denote) : OnBool

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

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

  Whether every multiplicity in lft is at most the one in rgt.

• bagAll [Ω] (α : Typ) (p : Term (α.function (Typ?.typ Typ.bool)).Denote) (b : Term (Typ.bag (Typ?.typ α)).Denote) : OnBool

  Whether every element of a bag satisfies a predicate.

• bagSome [Ω] (α : Typ) (p : Term (α.function (Typ?.typ Typ.bool)).Denote) (b : Term (Typ.bag (Typ?.typ α)).Denote) : OnBool

  Whether some element of a bag satisfies a predicate.

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

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

Equations

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

Values

def Cvc.Typed.Term.mkBagValue {α : Type} [Ω] [Ord α] [ToTyp α] [ValueToTerm α] (bag : Bag α) : Env (Term (Bag α))

The bag term denoting a bag of values.

Equations

• Cvc.Typed.Term.mkBagValue = Cvc.Untyped.Term.mkBagValue

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

The bag of values a constant bag term denotes.

Equations

• Cvc.Typed.Term.getBagValue = Cvc.Untyped.Term.getBagValue

@[instance_reducible]

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

Equations

• Cvc.Typed.Term.instValueToTermBag = { valueToTerm := fun [Cvc.Ω] => Cvc.Typed.Term.mkBagValue }

@[instance_reducible]

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

Equations

• Cvc.Typed.Term.instTermToValueBag = { termToValue := fun [Cvc.Ω] => Cvc.Typed.Term.getBagValue }