Relates Srt-s to Type-s

Main class IsSrt (α : Type) associates srt : Srt to α. It guarantees this association works both ways by asking for a proof that α = srt.toType.

class Cvc.IsSrt (α : Type) : Type

Provides a srt : Srt such that α = srt.toType.

• srt : Srt

  Srt version of α.

• h_bij : α = (srt α).toType

  Turning srt into a Type results in α.

@[reducible, inline]

abbrev Cvc.getSrt (α : Type) [I : IsSrt α] : Srt

Retrieves the Srt corresponding to a Type.

Equations

• Cvc.getSrt α = Cvc.IsSrt.srt α

instance Cvc.Srt.instIsSrt (srt : Srt) : IsSrt srt.toType

Equations

• srt.instIsSrt = { srt := srt, h_bij := ⋯ }

@[reducible, inline]

abbrev Cvc.Srt.ofType (α : Type) [I : IsSrt α] : Srt

Retrieves the Srt corresponding to a Type.

Equations

• Cvc.Srt.ofType = Cvc.getSrt

@[simp]

theorem Cvc.Srt.toType_ofType (α : Type) [I : IsSrt α] : (ofType α).toType = α

@[simp]

theorem Cvc.Srt.ofType_toType (srt : Srt) : ofType srt.toType = srt

Instances for simple types

instance Cvc.IsSrt.instUnit : IsSrt Unit

Equations

• Cvc.IsSrt.instUnit = { srt := Cvc.Srt.unit, h_bij := Cvc.IsSrt.instUnit._proof_1 }

instance Cvc.IsSrt.instBool : IsSrt Bool

Equations

• Cvc.IsSrt.instBool = { srt := Cvc.Srt.bool, h_bij := Cvc.IsSrt.instBool._proof_1 }

instance Cvc.IsSrt.instInt : IsSrt Int

Equations

• Cvc.IsSrt.instInt = { srt := Cvc.Srt.int, h_bij := Cvc.IsSrt.instInt._proof_1 }

instance Cvc.IsSrt.instRat : IsSrt Rat

Equations

• Cvc.IsSrt.instRat = { srt := Cvc.Srt.real, h_bij := Cvc.IsSrt.instRat._proof_1 }

instance Cvc.IsSrt.instString : IsSrt String

Equations

• Cvc.IsSrt.instString = { srt := Cvc.Srt.string, h_bij := Cvc.IsSrt.instString._proof_1 }

instance Cvc.IsSrt.instRoundingMode : IsSrt RoundingMode

Equations

• Cvc.IsSrt.instRoundingMode = { srt := Cvc.Srt.roundingMode, h_bij := Cvc.IsSrt.instRoundingMode._proof_1 }

instance Cvc.IsSrt.instRegex : IsSrt Cvc.Regex

Equations

• Cvc.IsSrt.instRegex = { srt := Cvc.Srt.regex, h_bij := Cvc.IsSrt.instRegex._proof_1 }

Instances for non-Srt-parameterized types

instance Cvc.IsSrt.instAnyFloat {exp sig : UInt32} : IsSrt (Cvc.AnyFloat exp sig)

Equations

• Cvc.IsSrt.instAnyFloat = { srt := Cvc.Srt.float exp sig, h_bij := ⋯ }

instance Cvc.IsSrt.instAbstract {k : Srt.Kind} : IsSrt (Cvc.Abstract k)

Equations

• Cvc.IsSrt.instAbstract = { srt := Cvc.Srt.abstract k, h_bij := ⋯ }

instance Cvc.IsSrt.instFiniteField {n : Nat} : IsSrt (FiniteField n)

Equations

• Cvc.IsSrt.instFiniteField = { srt := Cvc.Srt.finiteField n, h_bij := ⋯ }

instance Cvc.IsSrt.instBitVec {size : Nat} : IsSrt (BitVec size)

Equations

• Cvc.IsSrt.instBitVec = { srt := Cvc.Srt.bitVec size, h_bij := ⋯ }

instance Cvc.IsSrt.instUninterpreted {name : String} : IsSrt (Uninterpreted name)

Equations

• Cvc.IsSrt.instUninterpreted = { srt := Cvc.Srt.uninterpreted name, h_bij := ⋯ }

Instances composite types

instance Cvc.IsSrt.instArray {α : Type} [A : IsSrt α] : IsSrt (Array α)

Equations

• Cvc.IsSrt.instArray = { srt := (Cvc.IsSrt.srt α).seq, h_bij := ⋯ }

instance Cvc.IsSrt.instFunction {α β : Type} [A : IsSrt α] [B : IsSrt β] : IsSrt (α → β)

Equations

• Cvc.IsSrt.instFunction = { srt := (Cvc.IsSrt.srt α).function (Cvc.IsSrt.srt β), h_bij := ⋯ }

instance Cvc.IsSrt.instProd {α β : Type} [A : IsSrt α] [B : IsSrt β] : IsSrt (α × β)

Equations

• Cvc.IsSrt.instProd = { srt := (Cvc.IsSrt.srt α).prod (Cvc.IsSrt.srt β), h_bij := ⋯ }

instance Cvc.IsSrt.instTMap {α β : Type} [A : IsSrt α] [B : IsSrt β] : IsSrt (Cvc.TMap α β)

Equations

• Cvc.IsSrt.instTMap = { srt := (Cvc.IsSrt.srt α).array (Cvc.IsSrt.srt β), h_bij := ⋯ }

instance Cvc.IsSrt.instBag {α : Type} [A : IsSrt α] : IsSrt (Cvc.Bag α)

Equations

• Cvc.IsSrt.instBag = { srt := (Cvc.IsSrt.srt α).bag, h_bij := ⋯ }

instance Cvc.IsSrt.instSet {α : Type} [A : IsSrt α] : IsSrt (Cvc.Set α)

Equations

• Cvc.IsSrt.instSet = { srt := (Cvc.IsSrt.srt α).set, h_bij := ⋯ }

Refinement of IsSrt to arithmetic sorts

@[reducible, inline]

abbrev Cvc.is_arith (α : Type) [IsSrt α] : Prop

Proof that the sort associated to α is arithmetic.

Equations

• Cvc.is_arith α = (Cvc.Srt.ofType α).is_arith

instance Cvc.instDecidableIs_arith {α : Type} [IsSrt α] : Decidable (Cvc.is_arith α)

Equations

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

@[simp]

theorem Cvc.is_arith_def (α : Type) [inst : IsSrt α] : Cvc.is_arith α → α = Int ∨ α = Rat

def Cvc.is_arith_srt_def (α : Type) [inst : IsSrt α] : Cvc.is_arith α → IsSrt.srt α = Srt.int ∨ IsSrt.srt α = Srt.real

Equations

• ⋯ = ⋯

class Cvc.IsSrt.Arith (α : Type) extends Cvc.IsSrt α : Type

Extends IsSrt with a proof that α's Srt is arithmetic.

• srt : Srt
• h_bij : α = (srt α).toType
• h_arith : Cvc.is_arith α

  Sort srt is an arithmetic sort.

Instances for Int and Rat (Real)

instance Cvc.IsSrt.Arith.instInt : IsSrt.Arith Int

Equations

• Cvc.IsSrt.Arith.instInt = { toIsSrt := Cvc.IsSrt.instInt, h_arith := Cvc.IsSrt.Arith.instInt._proof_1 }

instance Cvc.IsSrt.Arith.instRat : IsSrt.Arith Rat

Equations

• Cvc.IsSrt.Arith.instRat = { toIsSrt := Cvc.IsSrt.instRat, h_arith := Cvc.IsSrt.Arith.instRat._proof_1 }

theorem Cvc.IsSrt.Arith.int_or_rat (α : Type) [inst : IsSrt.Arith α] : α = Int ∨ α = Rat

def Cvc.IsSrt.Arith.int_or_rat' (α : Type) [inst : IsSrt.Arith α] : srt α = Srt.int ∨ srt α = Srt.real

Equations

• ⋯ = ⋯

def Cvc.IsSrt.Arith.inspect' {β : Prop} (α : Type) [inst : IsSrt.Arith α] (fInt : α = Int → β) (fRat : α = Rat → β) : β

Equations

• ⋯ = ⋯

def Cvc.IsSrt.Arith.inspect {α : Type} {β : Sort u} [inst : IsSrt.Arith α] (fInt : srt α = Srt.int → β) (fRat : srt α = Srt.real → β) : β

Equations

• Cvc.IsSrt.Arith.inspect fInt fRat = ⋯.by_cases fInt fRat