Tuples, typed

A tuple's index is a Lean product, and products flatten to the right exactly as function sorts curry: α × β × γ denotes (Tuple α β γ), one tuple of three components, not a pair whose second component is a pair. Left-nesting is what nests, so (α × β) × γ is the two-component tuple whose first component is a tuple.

So a tuple's last component cannot itself be a tuple: mkTuple x (.cons y (.last z)) builds a Term (α × β × γ), and Components.last refuses a product. Relations and tables use another tuple index, Tup α β in Cvc.Typed.Theory.Relation, which nests freely and reaches any component at a typed position.

A tuple's value is its Lean product: Solver.getValue on a Term (Int × Bool) answers (1, true), and mkValue (1, true) builds the tuple.

Construction

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

Components of a tuple, built with last and cons: .cons y (.last z) is y then z.

• terms : Cvc.Untyped.Terms

def Cvc.Typed.Term.Components.last [Ω] {α : Type} [ToTyp α] (component : Term α) (_isFlat : (Typ.of α).isFlat = true := by (try simp [Typ.isFlat, Typ.of, ToTyp.typ, Srt.prod]) <;> fail "a tuple's last component cannot itself be a tuple: its components would flatten into \ the tuple being built. Nest to the left instead.") : Components α

The last component of a tuple.

Its index must not itself be a product: α × β flattens β's components into the tuple being built, and a single term cannot stand for several of them. Nest to the left instead — a Term ((γ × δ) × ε) really is a tuple whose first component is a tuple.

Equations

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

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

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

Equations

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

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

The components' terms, sort-erased and flat, as the sort-erased Term.mkTuple takes them.

Equations

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

@[reducible, inline]

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

The components' terms, sort-erased and flat, as the sort-erased Term.mkTuple takes them.

Equations

• cs.erase = cs.toUntyped

def Cvc.Typed.Term.mkTuple [Ω] {α β : Type} [ToTyp α] (fst : Term α) (rest : Components β) : Env (Term (α × β))

The tuple whose components are the given ones, in order.

A tuple has at least two components, which is why the first is separate: Components on its own describes a single index, and only α × β describes a tuple.

Equations

• fst.mkTuple rest = Cvc.Untyped.Term.mkTuple (#[fst.erase] ++ Cvc.Typed.Term.Components.terms✝ rest)

def Cvc.Typed.Term.tupleProject [Ω] {α : Type} [ToTyp α] (indices : Array Nat) (tuple : Term α) : Env Untyped.Term

The tuple of the components at the given indices, in the order given.

The result is sort-erased: which components an index array selects is a runtime value, so no Lean index describes it. Untyped.Term.typeCheck puts an index back on once you know what it is.

Equations

• Cvc.Typed.Term.tupleProject indices tuple = Cvc.Untyped.Term.tupleProject indices tuple

Values

def Cvc.Typed.Term.isTupleValue [Ω] {α β : Type} [ToTyp α] [ToTyp β] (term : Term (α × β)) : Bool

Determine if this term is a tuple value.

Equations

• term.isTupleValue = Cvc.Untyped.Term.isTupleValue term

def Cvc.Typed.Term.getTupleValue [Ω] {α β : Type} [ToTyp α] [ToTyp β] (term : Term (α × β)) : Res Untyped.Terms

The components a constant tuple term denotes, failing if it denotes none.

Sort-erased, like getKids: a tuple's components have as many different indices as it has components, and an array holds one type.

Equations

• term.getTupleValue = Cvc.Untyped.Term.getTupleValue term

Selection

fst and snd read a tuple as Lean's Prod.fst and Prod.snd read a product: on an α × β × γ, snd answers the tuple (Tuple β γ). A single middle component has no typed accessor here: use Untyped.Term.tupleSelect then typeCheck, or the Tup index, whose tupAt reaches any component.

def Cvc.Typed.Term.fst [Ω] {α β : Type} (t : Term (α × β)) : Env (Term α)

The first component, as Lean's Prod.fst, at any arity.

Equations

• t.fst = Cvc.Untyped.Term.tupleSelect 0 t.erase

def Cvc.Typed.Term.snd [Ω] {β α : Type} [B : ToTyp β] (t : Term (α × β)) : Env (Term β)

Everything but the first component, as Lean's Prod.snd.

The second component of a pair; on a longer tuple, the tuple of every component past the first — (Tuple β γ) for an α × β × γ, built as (tuple (tuple.select 1 t) (tuple.select 2 t)).

Equations

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

def Cvc.Typed.Term.pairComponents? [Ω] {β α : Type} [ToTyp β] (t : Term (α × β)) (_isFlat : (Typ.of β).isFlat = true := by (try simp [Typ.isFlat, Typ.of, ToTyp.typ, Srt.prod]) <;> fail "the second component is a tuple, so this is not a pair") : Env (Option (Term α × Term β))

A pair literal's two components, none if the term is not a literal.

Pairs only: a longer tuple's tail has no term of its own. The datatype view takes any tuple apart.

Equations

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