Product-indexed tuples

A Lean product indexes a tuple: α × β × γ is one three-component tuple, as products flatten to the right, while (α × β) × γ has two components, the first a tuple. OneTuple α is the one-component tuple. Relations and tables use the list-shaped Tup of Cvc.Types.Relation.

A tuple's value is the Lean product it is indexed by, converted with the same flattening.

@[reducible, inline]

abbrev Cvc.Typ.isFlat : Typ → Bool

Whether a sort is a single tuple component rather than a tuple of its own.

A product cannot be a tuple's last component: its own components would flatten into the tuple.

Equations

• (Cvc.Typ.prod args).isFlat = false
• Cvc.Typ.bool.isFlat = true
• Cvc.Typ.int.isFlat = true
• Cvc.Typ.real.isFlat = true
• Cvc.Typ.string.isFlat = true
• Cvc.Typ.regex.isFlat = true
• Cvc.Typ.roundingMode.isFlat = true
• (Cvc.Typ.bitVec size).isFlat = true
• (Cvc.Typ.float exp sig).isFlat = true
• (Cvc.Typ.finiteField size).isFlat = true
• (Cvc.Typ.arrayTo idx elm).isFlat = true
• (Cvc.Typ.bag elm).isFlat = true
• (Cvc.Typ.set elm).isFlat = true
• (Cvc.Typ.seq elm).isFlat = true
• elm.nullable.isFlat = true
• (Cvc.Typ.record fields).isFlat = true
• (Cvc.Typ.datatype name).isFlat = true
• (dom.function cod).isFlat = true
• (Cvc.Typ.uninterpreted name).isFlat = true

def Cvc.Srt.prod (α β : Typ) : Typ

The tuple Typ of α then β, flattening a tuple β into its components.

Equations

• Cvc.Srt.prod α (Cvc.Typ.prod args) = Cvc.Typ.prod (α :: args)
• Cvc.Srt.prod α x✝ = Cvc.Typ.prod [α, x✝]

@[instance_reducible]

instance Cvc.Srt.instToTypProd {α β : Type} [A : ToTyp α] [B : ToTyp β] : ToTyp (α × β)

Equations

• Cvc.Srt.instToTypProd = { typ := Cvc.Srt.prod (Cvc.ToTyp.typ α) (Cvc.ToTyp.typ β) }

@[instance_reducible, instance 100]

instance Cvc.instOrdProd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] : Ord (α × β)

Lexicographic order on pairs, so that a set, bag or array index of tuples can be written.

A global instance: importing the library brings it into scope.

Equations

• Cvc.instOrdProd = lexOrd

structure Cvc.OneTuple (α : Type) : Type

A tuple of one component, denoting the one-component SMT tuple sort (Tuple α).

Like any product it nests as a first component and flattens as a last: OneTuple α × β is (Tuple (Tuple α) β) while α × OneTuple β is (Tuple α β).

• value : α

  The component.

def Cvc.instDecidableEqOneTuple.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : OneTuple α✝) : Decidable (x✝ = x✝¹)

Equations

• Cvc.instDecidableEqOneTuple.decEq { value := a } { value := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.instDecidableEqOneTuple {α✝ : Type} [DecidableEq α✝] : DecidableEq (OneTuple α✝)

Equations

• Cvc.instDecidableEqOneTuple = Cvc.instDecidableEqOneTuple.decEq

@[instance_reducible]

instance Cvc.instOrdOneTuple {α✝ : Type} [Ord α✝] : Ord (OneTuple α✝)

Equations

• Cvc.instOrdOneTuple = { compare := Cvc.instOrdOneTuple.ord }

def Cvc.instOrdOneTuple.ord {α✝ : Type} [Ord α✝] : OneTuple α✝ → OneTuple α✝ → Ordering

Equations

• Cvc.instOrdOneTuple.ord { value := a } { value := b } = (compare a b).then Ordering.eq

def Cvc.instHashableOneTuple.hash {α✝ : Type} [Hashable α✝] : OneTuple α✝ → UInt64

Equations

• Cvc.instHashableOneTuple.hash { value := a } = mixHash 0 (hash a)

@[instance_reducible]

instance Cvc.instHashableOneTuple {α✝ : Type} [Hashable α✝] : Hashable (OneTuple α✝)

Equations

• Cvc.instHashableOneTuple = { hash := Cvc.instHashableOneTuple.hash }

@[instance_reducible]

instance Cvc.instReprOneTuple {α✝ : Type} [Repr α✝] : Repr (OneTuple α✝)

Equations

• Cvc.instReprOneTuple = { reprPrec := Cvc.instReprOneTuple.repr }

def Cvc.instReprOneTuple.repr {α✝ : Type} [Repr α✝] : OneTuple α✝ → Nat → Std.Format

Equations

• Cvc.instReprOneTuple.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "value" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.value)).group) " }"

@[instance_reducible]

instance Cvc.OneTuple.instToTyp {α : Type} [A : ToTyp α] : ToTyp (OneTuple α)

Equations

• Cvc.OneTuple.instToTyp = { typ := Cvc.Typ.prod [Cvc.ToTyp.typ α] }