Relations, typed

A relation is a set of tuples, indexed by Rel α β: its tuples are Tup α β, whose components are the list α followed by β. So Rel [Int] Bool relates Ints to Bools, and Rel [] α is a unary relation. A tuple is built with mkTup (.cons a (.last b)), and a component is read at a typed position, t.tupAt col%1.

The set operators are restated at a relation's index (relUnion, relMember, …); relToSet crosses to Set, for setMap and setFold. cvc5 marks every relation-specific kind experimental.

Tuples

structure Cvc.Typed.Term.Tup.Components [Ω] (α : List Type) (β : Type) : Type

The components of a tuple, in order, along with the index they denote.

last and cons are the only builders, so the number of terms and the number of components the index describes stay in step.

• terms : Cvc.Untyped.Terms

def Cvc.Typed.Term.Tup.Components.last [Ω] {β : Type} (component : Term β) : Components [] β

The final component.

Equations

• Cvc.Typed.Term.Tup.Components.last component = { terms := #[component.erase] }

def Cvc.Typed.Term.Tup.Components.cons [Ω] {α : Type} {αs : List Type} {β : Type} (component : Term α) (rest : Components αs β) : Components (α :: αs) β

Adds a component in front of the ones collected so far.

Equations

• Cvc.Typed.Term.Tup.Components.cons component rest = { terms := #[component.erase] ++ Cvc.Typed.Term.Tup.Components.terms✝ rest }

def Cvc.Typed.Term.Tup.Components.toUntyped [Ω] {α : List Type} {β : Type} (cs : Components α β) : Untyped.Terms

The components' terms, sort-erased and in order; free.

Equations

• cs.toUntyped = Cvc.Typed.Term.Tup.Components.terms✝ cs

@[reducible, inline]

abbrev Cvc.Typed.Term.Tup.Components.erase [Ω] {α : List Type} {β : Type} (cs : Components α β) : Untyped.Terms

The components' terms, sort-erased and in order; free.

Equations

• cs.erase = cs.toUntyped

def Cvc.Typed.Term.mkTup [Ω] {α : List Type} {β : Type} (components : Tup.Components α β) : Env (Term (Tup α β))

The tuple whose components are the given ones.

A component that is itself a tuple stays one: Tup [α] (Tup [β] γ) denotes (Tuple α (Tuple β γ)), not a three-component tuple.

Equations

• Cvc.Typed.Term.mkTup components = Cvc.Untyped.Term.mkTuple (Cvc.Typed.Term.Tup.Components.terms✝ components)

def Cvc.Typed.Term.tupFst [Ω] {α : Type} {αs : List Type} {β : Type} (tuple : Term (Tup (α :: αs) β)) : Env (Term α)

The first component.

Equations

• tuple.tupFst = Cvc.Untyped.Term.tupleSelect 0 tuple.erase

def Cvc.Typed.Term.tupLast [Ω] {α : List Type} {β : Type} (tuple : Term (Tup α β)) : Env (Term β)

The last component, at any arity.

Equations

• tuple.tupLast = Cvc.Untyped.Term.tupleSelect α.length tuple.erase

def Cvc.Typed.Term.tupRest [Ω] {α : Type} {αs : List Type} {β : Type} (tuple : Term (Tup (α :: αs) β)) : Env (Term (Tup αs β))

Every component but the first, as a tuple.

A projection rather than a selection, since the result has more than one component in general. Composing it with tupFst reaches any position.

Equations

• tuple.tupRest = Cvc.Untyped.Term.tupleProject (Array.map (fun (x : Nat) => x + 1) (Array.range (αs.length + 1))) tuple.erase

def Cvc.Typed.Term.tupAt [Ω] {α : List Type} {β γ : Type} (tuple : Term (Tup α β)) (idx : Col α β γ) : Env (Term γ)

The component at the given position, at that component's own type.

The general form of tupFst/tupLast, and the way to reach a middle component without composing tupRest: t.tupAt col%1 is the second one.

Equations

• tuple.tupAt idx = Cvc.Untyped.Term.tupleSelect idx.toNat tuple.erase

def Cvc.Typed.Term.tupProject [Ω] {α : List Type} {β : Type} {α' : List Type} {β' : Type} (cols : Cols α β α' β') (tuple : Term (Tup α β)) : Env (Term (Tup α' β'))

The tuple of the components at the given positions: t.tupProject cols% [2, 0].

Projecting one position gives a one-component tuple, where tupAt gives the component.

Equations

• Cvc.Typed.Term.tupProject cols tuple = Cvc.Untyped.Term.tupleProject cols.toArray tuple.erase

Crossing to and from sets

Both directions are the identity on terms: a relation is a set of tuples, and only the index differs. They are here for the operators that leave the relation world, and for interoperating with code written against Set.

def Cvc.Typed.Term.relToSet [Ω] {α : List Type} {β : Type} [Ord (Tup α β)] (rel : Term (Rel α β)) : Term (Set (Tup α β))

Reads a relation as the set of tuples it is.

Equations

• rel.relToSet = rel

def Cvc.Typed.Term.relOfSet [Ω] {α : List Type} {β : Type} [Ord (Tup α β)] (set : Term (Set (Tup α β))) : Term (Rel α β)

Reads a set of tuples as the relation it is.

Equations

• set.relOfSet = set

Relational operators

def Cvc.Typed.Term.relJoin [Ω] {α : List Type} {μ : Type} {α' : List Type} {β' : Type} (lft : Term (Rel α μ)) (rgt : Term (Rel (μ :: α') β')) : Env (Term (Rel (α ++ α') β'))

Composition: lft's last component and rgt's first are the same mu, and both are dropped.

The shared mu is cvc5's joinability requirement, stated in the signature rather than checked at run time.

Equations

• lft.relJoin rgt = lft.erase.relJoin rgt.erase

def Cvc.Typed.Term.relProduct [Ω] {α : List Type} {β : Type} {α' : List Type} {β' : Type} (lft : Term (Rel α β)) (rgt : Term (Rel α' β')) : Env (Term (Rel (α ++ β :: α') β'))

Cartesian product: every pairing, with the components appended.

Equations

• lft.relProduct rgt = lft.erase.relProduct rgt.erase

@[reducible, inline]

abbrev Cvc.Typed.Term.transposed (α : List Type) (β : Type) : Type

The components of a transposed relation: the whole list, reversed.

Equations

• Cvc.Typed.Term.transposed [] x✝ = Cvc.Rel [] x✝
• Cvc.Typed.Term.transposed (hd :: tl) x✝ = Cvc.Rel (x✝ :: tl.reverse) hd

def Cvc.Typed.Term.relTranspose [Ω] {α : List Type} {β : Type} (rel : Term (Rel α β)) : Env (Term (transposed α β))

Reverses every tuple's components.

Equations

• rel.relTranspose = rel.erase.relTranspose

def Cvc.Typed.Term.relTclosure [Ω] {α : Type} (rel : Term (Rel [α] α)) : Env (Term (Rel [α] α))

Transitive closure of a homogeneous binary relation.

Equations

• rel.relTclosure = rel.erase.relTclosure

def Cvc.Typed.Term.relIden [Ω] {α : Type} (rel : Term (Rel [] α)) : Env (Term (Rel [α] α))

The identity relation over a unary relation's elements.

Rel [] α is the unary relation — the split index says so directly, with no separate one-component tuple type needed.

Equations

• rel.relIden = rel.erase.relIden

def Cvc.Typed.Term.relJoinImage [Ω] {α β : Type} (rel : Term (Rel [α] β)) (size : Term Int) : Env (Term (Rel [] α))

The elements of a binary relation related to at least size others.

Equations

• rel.relJoinImage size = rel.erase.relJoinImage size.erase

def Cvc.Typed.Term.relGroup [Ω] {α : List Type} {β : Type} [Ord (Rel α β)] (indices : Array Nat) (rel : Term (Rel α β)) : Env (Term (Set (Rel α β)))

Partitions the relation, putting tuples that agree on the given components in the same part.

Answers a set of relations. The indices choose what is compared and so do not reach the result's sort.

Equations

• Cvc.Typed.Term.relGroup indices rel = Cvc.Untyped.Term.relGroup indices rel.erase

def Cvc.Typed.Term.relAggregate [Ω] {γ : Type} {α : List Type} {β : Type} [Ord γ] (indices : Array Nat) (f : Term (Tup α β → γ → γ)) (init : Term γ) (rel : Term (Rel α β)) : Env (Term (Set γ))

Folds each group of tuples that agree on the given components.

The groups are relGroup's, but the answer is a set of accumulators rather than a set of relations: f runs over each group's tuples starting from init, and the result collects one value of gamma per group.

f is a function-sorted term, which Term.lambda builds. Its two arguments are a tuple of the relation and the accumulator, in that order, and its result is the new accumulator — so gamma is fixed by init and by f's codomain together, and nothing about the fold has to be checked at run time.

The indices only say what is grouped, so they do not reach the result's sort. With none of them every tuple is in one group, which is an ordinary fold over the whole relation.

Equations

• Cvc.Typed.Term.relAggregate indices f init rel = Cvc.Untyped.Term.relAggregate indices f.erase init.erase rel.erase

def Cvc.Typed.Term.relTableJoin [Ω] {α : List Type} {β : Type} {α' : List Type} {β' : Type} (indices : Array (Nat × Nat)) (lft : Term (Rel α β)) (rgt : Term (Rel α' β')) : Env (Term (Rel (α ++ β :: α') β'))

Equi-join: the product, keeping the pairings whose given component pairs agree.

The result's sort is the product's, since the pairs only filter.

Equations

• Cvc.Typed.Term.relTableJoin indices lft rgt = Cvc.Untyped.Term.relTableJoin indices lft.erase rgt.erase

def Cvc.Typed.Term.relProject [Ω] {α : List Type} {β : Type} {α' : List Type} {β' : Type} (cols : Cols α β α' β') (rel : Term (Rel α β)) : Env (Term (Rel α' β'))

Projects every tuple onto the given components, in the order given.

Positions are written cols% [2, 0], and may reorder and repeat components. Untyped.Term.relProject takes them as an Array Nat, for positions known only at run time.

Equations

• Cvc.Typed.Term.relProject cols rel = Cvc.Untyped.Term.relProject cols.toArray rel.erase

The set operators, at a relation's index

Same operators, same behaviour; only the index differs, so a relation never has to be read as a set to be built or constrained.

def Cvc.Typed.Term.relMember [Ω] {α : List Type} {β : Type} (elm : Term (Tup α β)) (rel : Term (Rel α β)) : Env (Term Bool)

Whether a tuple is in the relation.

Equations

• elm.relMember rel = elm.erase.setMember rel.erase

def Cvc.Typed.Term.relSubset [Ω] {α : List Type} {β : Type} (lft rgt : Term (Rel α β)) : Env (Term Bool)

Whether every tuple of the first relation is in the second.

Equations

• lft.relSubset rgt = lft.erase.setSubset rgt.erase

def Cvc.Typed.Term.relIsEmpty [Ω] {α : List Type} {β : Type} (rel : Term (Rel α β)) : Env (Term Bool)

Whether the relation has no tuple.

Equations

• rel.relIsEmpty = rel.erase.setIsEmpty

def Cvc.Typed.Term.relIsSingleton [Ω] {α : List Type} {β : Type} (rel : Term (Rel α β)) : Env (Term Bool)

Whether the relation has exactly one tuple.

Equations

• rel.relIsSingleton = rel.erase.setIsSingleton

def Cvc.Typed.Term.relSingleton [Ω] {α : List Type} {β : Type} (elm : Term (Tup α β)) : Env (Term (Rel α β))

The relation holding exactly one tuple.

Equations

• elm.relSingleton = elm.erase.setSingleton

def Cvc.Typed.Term.relInsert [Ω] {α : List Type} {β : Type} (elm : Term (Tup α β)) (rel : Term (Rel α β)) : Env (Term (Rel α β))

The relation with one more tuple.

Equations

• elm.relInsert rel = elm.erase.setInsert rel.erase

def Cvc.Typed.Term.relUnion [Ω] {α : List Type} {β : Type} (lft rgt : Term (Rel α β)) : Env (Term (Rel α β))

Union.

Equations

• lft.relUnion rgt = lft.erase.setUnion rgt.erase

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

N-ary version of relUnion, requires at least two elements.

Equations

• Cvc.Typed.Term.relUnionN rels atLeastTwoElements = Cvc.Untyped.Term.setUnionN rels atLeastTwoElements

def Cvc.Typed.Term.relInter [Ω] {α : List Type} {β : Type} (lft rgt : Term (Rel α β)) : Env (Term (Rel α β))

Intersection.

Equations

• lft.relInter rgt = lft.erase.setInter rgt.erase

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

N-ary version of relInter, requires at least two elements.

Equations

• Cvc.Typed.Term.relInterN rels atLeastTwoElements = Cvc.Untyped.Term.setInterN rels atLeastTwoElements

def Cvc.Typed.Term.relMinus [Ω] {α : List Type} {β : Type} (lft rgt : Term (Rel α β)) : Env (Term (Rel α β))

Difference.

Equations

• lft.relMinus rgt = lft.erase.setMinus rgt.erase

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

N-ary version of relMinus, requires at least two elements.

Equations

• Cvc.Typed.Term.relMinusN rels atLeastTwoElements = Cvc.Untyped.Term.setMinusN rels atLeastTwoElements

def Cvc.Typed.Term.relComplement [Ω] {α : List Type} {β : Type} (rel : Term (Rel α β)) : Env (Term (Rel α β))

Complement, against every tuple of the relation's shape.

Equations

• rel.relComplement = rel.erase.setComplement

def Cvc.Typed.Term.relCard [Ω] {α : List Type} {β : Type} (rel : Term (Rel α β)) : Env (Term Int)

How many tuples the relation holds.

Equations

• rel.relCard = rel.erase.setCard

def Cvc.Typed.Term.relChoose [Ω] {α : List Type} {β : Type} (rel : Term (Rel α β)) : Env (Term (Tup α β))

Some tuple of the relation, unspecified which; undefined on the empty relation.

Equations

• rel.relChoose = rel.erase.setChoose

def Cvc.Typed.Term.relFilter [Ω] {α : List Type} {β : Type} (p : Term (Tup α β → Bool)) (rel : Term (Rel α β)) : Env (Term (Rel α β))

The tuples satisfying a predicate.

Equations

• p.relFilter rel = p.erase.setFilter rel.erase

def Cvc.Typed.Term.relAll [Ω] {α : List Type} {β : Type} (p : Term (Tup α β → Bool)) (rel : Term (Rel α β)) : Env (Term Bool)

Whether every tuple satisfies a predicate.

Equations

• p.relAll rel = p.erase.setAll rel.erase

def Cvc.Typed.Term.relSome [Ω] {α : List Type} {β : Type} (p : Term (Tup α β → Bool)) (rel : Term (Rel α β)) : Env (Term Bool)

Whether some tuple satisfies a predicate.

Equations

• p.relSome rel = p.erase.setSome rel.erase

def Cvc.Typed.Term.relEmpty' [Ω] (α : List Type) (β : Type) [ToTypList α] [ToTyp β] : Env (Term (Rel α β))

The empty relation of the given shape.

Equations

• Cvc.Typed.Term.relEmpty' α β = do let __do_lift ← Cvc.Srt.of (Cvc.Tup α β) Cvc.Untyped.Term.setEmpty __do_lift

@[reducible, inline]

abbrev Cvc.Typed.Term.relEmpty [Ω] {α : List Type} {β : Type} [ToTypList α] [ToTyp β] : Env (Term (Rel α β))

The empty relation of the given shape.

Equations

• Cvc.Typed.Term.relEmpty = Cvc.Typed.Term.relEmpty' α β

def Cvc.Typed.Term.relUniverse' [Ω] (α : List Type) (β : Type) [ToTypList α] [ToTyp β] : Env (Term (Rel α β))

The relation holding every tuple of its shape.

Equations

• Cvc.Typed.Term.relUniverse' α β = do let __do_lift ← Cvc.Srt.of (Cvc.Tup α β) Cvc.Untyped.Term.setUniverse __do_lift

@[reducible, inline]

abbrev Cvc.Typed.Term.relUniverse [Ω] {α : List Type} {β : Type} [ToTypList α] [ToTyp β] : Env (Term (Rel α β))

The relation holding every tuple of its shape.

Equations

• Cvc.Typed.Term.relUniverse = Cvc.Typed.Term.relUniverse' α β