4. Terms🔗

Cvc.lean exposes two API-s for terms: Typed and Untyped. The former provides very strong static guarantees by strongly-typing terms; the latter does not but is more flexible, allowing in particular to build lists/arrays of terms of different sorts.

NB: cvc.lean enforces type-safety through definition irreducibility, which means you need to use Lean's module system to get any of its benefits.

Terms can be constructed by calling constructor-functions, but cvc.lean also provides a syntax extension smt! ... that supports Lean-like syntax to create terms, described in its own section. The discussion below presents both, but the rest of this document will almost always rely on the syntax extension.

4.1. Typed Terms🔗

def

Cvc.Typed.Term [Ω] : Type → Type
Cvc.Typed.Term [Ω] : Type → Type

Documentation

A cvc5 term whose sort is the one the Lean type α denotes.

Term Int, Term (Set Bool) and Term (Int → Bool) are terms of the SMT-LIB sorts Int, (Set Bool) and (-> Int Bool); a Lean type denotes a sort through its ToTyp instance. Every constructor states its sorts through the index, so a sort mistake is a Lean type error rather than a cvc5 error at runtime, and a value read out of a model comes back as an α.

The index is phantom: at runtime a Term α is exactly a Cvc.Untyped.Term. toUntyped (or erase) goes down for free, and Cvc.Untyped.Term.toTyped (or typeCheck) goes up by checking the term's sort.

Typed terms have a type parameter for the actual Srt of that term. We saw previously that ToTyp links types to Srt-s, and it is precisely the mechanism used here. Typing terms lets us check statically that term constructors are invoked in a valid way, and makes their signature as precise as it can be.

def

Cvc.Typed.Term.mkBool [Ω] (b : Bool) : Env (Typed.Term Bool)
Cvc.Typed.Term.mkBool [Ω] (b : Bool) :
  Env (Typed.Term Bool)

Documentation

A boolean literal.

def

Cvc.Typed.Term.and [Ω] (lft rgt : Typed.Term Bool) :
  Env (Typed.Term Bool)
Cvc.Typed.Term.and [Ω]
  (lft rgt : Typed.Term Bool) :
  Env (Typed.Term Bool)

Documentation

Binary conjunction.

def

Cvc.Typed.Term.mkInt [Ω] (i : Int) : Env (Typed.Term Int)
Cvc.Typed.Term.mkInt [Ω] (i : Int) :
  Env (Typed.Term Int)

Documentation

An integer literal.

Some term operators are polymorphic: addition for instance works on any arithmetic terms as long as they have the same sort.

def

Cvc.Typed.Term.add [Ω] {α : Type} [ToTyp α] [IsArith α]
  (lft rgt : Typed.Term α) : Env (Typed.Term α)
Cvc.Typed.Term.add [Ω] {α : Type}
  [ToTyp α] [IsArith α]
  (lft rgt : Typed.Term α) :
  Env (Typed.Term α)

Documentation

Binary addition.

Notice that the type-class constraint IsArith α must hold, which asks for a proof that the Typ associated to α is actually arithmetic.

type class

Cvc.IsArith (α : Type) [A : ToTyp α] : Prop
Cvc.IsArith (α : Type) [A : ToTyp α] :
  Prop

Documentation and 1 method

α denotes an arithmetic sort: Int or Rat.

Instance Constructor

Cvc.IsArith.mk

Methods

valid_typ : (ToTyp.typ α).isArith = true

Proof that α's Typ is arithmetic.

We can declare function symbols by either letting type inference figure out the type for us, or by providing it explicitly.

def

Cvc.Typed.Term.mkSymbol [Ω] {α : Type} [ToTyp α] (name : String) :
  Env (Typed.Term α)
Cvc.Typed.Term.mkSymbol [Ω] {α : Type}
  [ToTyp α] (name : String) :
  Env (Typed.Term α)

Documentation

A fresh uninterpreted constant of sort α, named name.

def

Cvc.Typed.Term.mkSymbolAs [Ω] (α : Type) [ToTyp α] (name : String) :
  Env (Typed.Term α)
Cvc.Typed.Term.mkSymbolAs [Ω] (α : Type)
  [ToTyp α] (name : String) :
  Env (Typed.Term α)

Documentation

A symbol of the sort α describes, naming α explicitly.

4.1.1. Examples🔗

Examples of using term constructors follow, feel free to hover around to make sure the terms are correctly typed.

open Typed in conj := (and b1 b2)
i1_pos := (<= 0 i1)
ite := (ite (<= 0 i1) i1 i2)
#eval Env.runIO do
  let b1 ← Term.mkSymbolAs Bool "b1"
  let b2 ← Term.mkSymbol "b2"
  let conj ← b1.and b2
  println! "conj := {conj}"
  let i1 ← Term.mkSymbol "i1"
  let zero ← Term.mkInt 0
  let i1_pos ← zero.le i1
  println! "i1_pos := {i1_pos}"
  let i2 ← Term.mkSymbol "i2"
  let ite ← i1_pos.ite i1 i2
  println! "ite := {ite}"

conj := (and b1 b2)
i1_pos := (<= 0 i1)
ite := (ite (<= 0 i1) i1 i2)

Using the smt! extension:

open Typed in conj := (and b1 b2)
i1_pos := (<= 0 i1)
ite := (ite (<= 0 i1) i1 i2)
#eval Env.runIO do
  let b1 ← Term.mkSymbol "b1"
  let b2 ← Term.mkSymbol "b2"
  let conj ← smt! b1 ∧ b2
  println! "conj := {conj}"
  let i1 ← Term.mkSymbol "i1"
  let i1_pos ← smt! 0 ≤ i1
  println! "i1_pos := {i1_pos}"
  let i2 ← Term.mkSymbol "i2"
  let ite ← smt! if 0 ≤ i1 then i1 else i2
  println! "ite := {ite}"

Strong-typing works with functions/function application as well.

open Typed in f : (-> Int Bool Int) := f
f_i : (-> Bool Int) := (f i)
f_i_b : Int := (f i b)
f_i_b' : Int := (f i b)
#eval Env.runIO do
  let f ← Term.mkSymbolAs (Int → Bool → Int) "f"
  println! "f : {← f.getSort} := {f}"
  let i ← Term.mkSymbol "i"
  let f_i ← f.apply i
  println! "f_i : {← f_i.getSort} := {f_i}"
  let b ← Term.mkSymbol "b"
  let f_i_b ← f_i.apply b
  println! "f_i_b : {← f_i_b.getSort} := {f_i_b}"
  -- alternatively
  let f_i_b' ← f.apply2 i b
  println! "f_i_b' : {← f_i_b'.getSort} := {f_i_b'}"

f : (-> Int Bool Int) := f
f_i : (-> Bool Int) := (f i)
f_i_b : Int := (f i b)
f_i_b' : Int := (f i b)

Using the smt! extension:

open Typed in f_i := (f i)
f_i_b := (f i b)
f_i_b' := (f i b)
#eval Env.runIO do
  let f ← Term.mkSymbolAs (Int → Bool → Int) "f"
  let i ← Term.mkSymbol "i"
  let f_i ← smt! f i
  println! "f_i := {f_i}"
  let b ← Term.mkSymbol "b"
  let f_i_b ← smt! f_i b
  println! "f_i_b := {f_i_b}"

  let f_i_b' ← smt! f i b
  println! "f_i_b' := {f_i_b'}"

Of course, type-checking catches any invalid-sort mistake we make.

open Typed in #eval Env.runIO do
  let b1 ← Term.mkSymbolAs Bool "b1"
  let b2 ← Term.mkSymbolAs Int "b2"
  let conj ← b1.and Application type mismatch: The argument
  b2
has type
  Term Int
but is expected to have type
  Term Bool
in the application
  b1.and b2

Note: The following definitions were not unfolded because their definition is not exposed:
  Term ↦ 6b2
  println! "conj := {conj}"

Another type-checking error on an ill-typed function application:

open Typed in #eval Env.runIO do
  let f ← Term.mkSymbolAs (Bool → String → Rat) "f"
  let b1 ← Term.mkSymbolAs Bool "b1"
  let i1 ← Term.mkSymbolAs Int "i1"
  let f_b1_i1 ← f.apply2 b1 Application type mismatch: The argument
  i1
has type
  Term Int
but is expected to have type
  Term String
in the application
  f.apply2 b1 i1

Note: The following definitions were not unfolded because their definition is not exposed:
  Term ↦ 6i1
  println! "f_b1_i1 := {f_b1_i1}"

4.2. Untyped Terms🔗

def

Cvc.Untyped.Term [Ω] : Type
Cvc.Untyped.Term [Ω] : Type

Documentation

A sort-erased cvc5 term.

The term carries no sort on the Lean side: its sort is known to cvc5 alone, so a sort mistake, such as and applied to an integer, is reported by cvc5 at runtime. In exchange, terms of different sorts share one type, and an Array Term can hold them side by side.

A term belongs to the Ω scope it was built in and cannot leave it. At runtime it is exactly a cvc5 term, so the wrapper costs nothing. typeCheck checks its sort against a Lean type and gives it that type as an index, producing a Cvc.Typed.Term.

Untyped terms do not have a type parameter corresponding to their sort, which means untyped term constructors do not provide any static guarantee that the result is a valid term. Instead, invalid terms will fail at runtime.

def

Cvc.Untyped.Term.mkBool [Ω] (b : Bool) : Env Untyped.Term
Cvc.Untyped.Term.mkBool [Ω] (b : Bool) :
  Env Untyped.Term

Documentation

A boolean literal.

def

Cvc.Untyped.Term.and [Ω] (lft rgt : Untyped.Term) : Env Untyped.Term
Cvc.Untyped.Term.and [Ω]
  (lft rgt : Untyped.Term) :
  Env Untyped.Term

Documentation

Binary conjunction.

def

Cvc.Untyped.Term.mkInt [Ω] (i : Int) : Env Untyped.Term
Cvc.Untyped.Term.mkInt [Ω] (i : Int) :
  Env Untyped.Term

Documentation

An integer literal.

Unlike the typed API, the sort of an untyped term for a function symbol cannot be inferred and must be given explicitly. The first way to do so is to pass the actual sort.

def

Cvc.Untyped.Term.mkSymbol [Ω] (α : Srt) (name : String) :
  Env Untyped.Term
Cvc.Untyped.Term.mkSymbol [Ω] (α : Srt)
  (name : String) : Env Untyped.Term

Documentation

A fresh uninterpreted constant of sort α, named name.

The second way is to pass the Lean type that we would use to create a typed term.

def

Cvc.Untyped.Term.mkSymbolAs [Ω] (α : Type) [ToTyp α] (name : String) :
  Env Untyped.Term
Cvc.Untyped.Term.mkSymbolAs [Ω] (α : Type)
  [ToTyp α] (name : String) :
  Env Untyped.Term

Documentation

mkSymbol at the sort the Lean type α denotes.

4.2.1. Examples🔗

Below is the untyped version of the first typed-term example. No type-inference can take place, so we must always specify what the sort of each symbol is.

open Untyped in conj := (and b1 b2)
i1_pos := (<= 0 i1)
ite := (ite (<= 0 i1) i1 i2)
#eval Env.runIO do
  -- specify the sort using Lean types...
  let b1 ← Term.mkSymbolAs Bool "b1"
  -- ...or using `Srt` values
  let bool ← Srt.bool
  let b2 ← Term.mkSymbol bool "b2"
  let conj ← b1.and b2
  println! "conj := {conj}"
  let i1 ← Term.mkSymbolAs Int "i1"
  let zero ← Term.mkInt 0
  let i1_pos ← zero.le i1
  println! "i1_pos := {i1_pos}"
  let i2 ← Term.mkSymbolAs Int "i2"
  let ite ← i1_pos.ite i1 i2
  println! "ite := {ite}"

conj := (and b1 b2)
i1_pos := (<= 0 i1)
ite := (ite (<= 0 i1) i1 i2)

Using the smt! extension:

open Untyped in conj := (and b1 b2)
i1_pos := (<= 0 i1)
ite := (ite (<= 0 i1) i1 i2)
#eval Env.runIO do
  let b1 ← Term.mkSymbolAs Bool "b1"
  let b2 ← Term.mkSymbolAs Bool "b2"
  let conj ← smt! b1 ∧ b2
  println! "conj := {conj}"
  let i1 ← Term.mkSymbolAs Int "i1"
  let i1_pos ← smt! 0 ≤ i1
  println! "i1_pos := {i1_pos}"
  let i2 ← Term.mkSymbolAs Int "i2"
  let ite ← smt! if 0 ≤ i1 then i1 else i2
  println! "ite := {ite}"

On functions:

open Untyped in f : (-> Int Bool Int) := f
f_i : (-> Bool Int) := (f i)
f_i_b : Int := (f i b)
f_i_b' : Int := (f i b)
#eval Env.runIO do
  let f ← Term.mkSymbolAs (Int → Bool → Int) "f"
  println! "f : {← f.getSort} := {f}"
  let i ← Term.mkSymbolAs Int "i"
  let f_i ← f.apply i
  println! "f_i : {← f_i.getSort} := {f_i}"
  let b ← Term.mkSymbolAs Bool "b"
  let f_i_b ← f_i.apply b
  println! "f_i_b : {← f_i_b.getSort} := {f_i_b}"
  -- alternatively
  let f_i_b' ← f.apply2 i b
  println! "f_i_b' : {← f_i_b'.getSort} := {f_i_b'}"

f : (-> Int Bool Int) := f
f_i : (-> Bool Int) := (f i)
f_i_b : Int := (f i b)
f_i_b' : Int := (f i b)

Using the smt! extension:

open Untyped in f_i := (f i)
f_i_b := (f i b)
f_i_b' := (f i b)
#eval Env.runIO do
  let f ← Term.mkSymbolAs (Int → Bool → Int) "f"
  let i ← Term.mkSymbolAs Int "i"
  let f_i ← smt! f i
  println! "f_i := {f_i}"
  let b ← Term.mkSymbolAs Bool "b"
  let f_i_b ← smt! f_i b
  println! "f_i_b := {f_i_b}"

  let f_i_b' ← smt! f i b
  println! "f_i_b' := {f_i_b'}"

Since no type-checking is taking place, we can compile invalid terms without issue.

section variable [Ω] open Untyped
def badTerms : Env Unit := do
  let b1 ← Term.mkSymbolAs Bool "b1"
  let b2 ← Term.mkSymbolAs Int "b2"
  let conj ← b1.and b2
  println! "conj := {conj}"
end

Running that code fails with a relatively obscure error.

expecting a Boolean subexpression#eval Env.runIO badTerms

expecting a Boolean subexpression

4.3. Untyped/typed conversions🔗

Every type that exists in both layers converts the same way: toTyped goes from the sort-erased value to the typed one, and toUntyped the other way. Two families of aliases say what the conversion does:

a type indexed by a sort, such as Typed.Term Bool or a bound variable, also answers to erase going down, and going up has toTypedAs, which takes the index explicitly, besides toTyped, which infers it; their aliases are typeCheckAs and typeCheck;
a type with no index but with both a typed and a sort-erased API, such as a solver, answers to relax going down.

4.3.1. Untyped to typed🔗

Untyped.Term.toTypedAs checks, at runtime, an untyped term against (the sort associated to) a static type to produce a typed term.

def

Cvc.Untyped.Term.toTypedAs [Ω] (α : Type) [ToTyp α] (t : Untyped.Term) :
  Env (Typed.Term α)
Cvc.Untyped.Term.toTypedAs [Ω] (α : Type)
  [ToTyp α] (t : Untyped.Term) :
  Env (Typed.Term α)

Documentation

Types a sort-erased term at α, checking its sort against α's.

toTyped infers α from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

If the term's type can be inferred from context, Untyped.Term.toTyped is a more concise alternative.

def

Cvc.Untyped.Term.toTyped [Ω] {α : Type} [ToTyp α] (t : Untyped.Term) :
  Env (Typed.Term α)
Cvc.Untyped.Term.toTyped [Ω] {α : Type}
  [ToTyp α] (t : Untyped.Term) :
  Env (Typed.Term α)

Documentation

Types a sort-erased term at α, checking its sort against α's.

toTyped infers α from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Under their aliases, Untyped.Term.typeCheckAs and Untyped.Term.typeCheck, the same two functions say what they do. For example:

open Untyped in
boolTerm:  (or x false)
typedTerm: (or x false)
iteTerm:   (ite (or x false) 1 0)

cannot type the following term as `Int`, term has sort `Bool`:
(or x false)
#eval Env.runIO do
  let bool ← Srt.bool
  let x ← Term.mkSymbol bool "x"

  let boolTerm ← smt! x ∨ false
  println! "boolTerm:  {boolTerm}"

  let typedTerm ← boolTerm.toTypedAs Bool
  println! "typedTerm: {typedTerm}"

  let boolToInt (t : Typed.Term Bool) :=
    smt! if t then 1 else 0
  let iteTerm ← boolTerm.typeCheck >>= boolToInt
  println! "iteTerm:   {iteTerm}"

  println! ""
  try
    let illTyped ← boolTerm.typeCheckAs Int
    println! "unexpected: {illTyped}"
  catch e =>
    println! "{e}"

boolTerm:  (or x false)
typedTerm: (or x false)
iteTerm:   (ite (or x false) 1 0)

cannot type the following term as `Int`, term has sort `Bool`:
(or x false)

4.3.2. Typed to untyped🔗

This direction cannot fail: a typed term already is a sort-erased one, and Typed.Term.toUntyped merely forgets its index.

def

Cvc.Typed.Term.toUntyped [Ω] {α : Type} (t : Typed.Term α) :
  Untyped.Term
Cvc.Typed.Term.toUntyped [Ω] {α : Type}
  (t : Typed.Term α) : Untyped.Term

Documentation

The sort-erased term it is, for free: the index is forgotten, nothing is checked.

For example:

open Typed in
typedTerm:   (or x false)
untypedTerm: (or x false)
erase:       (or x false)
#eval Env.runIO do
  let x ← Term.mkSymbol "x"
  let typedTerm ← smt! x ∨ false
  --  ^^^^^^^^^~~~~~ `Typed.Term Bool`
  println! "typedTerm:   {typedTerm}"
  let untypedTerm := typedTerm.toUntyped
  --  ^^^^^^^^^^^~~~~ `Untyped.Term`
  println! "untypedTerm: {untypedTerm}"
  println! "erase:       {typedTerm.erase}"

typedTerm:   (or x false)
untypedTerm: (or x false)
erase:       (or x false)

4.3.3. Every conversion🔗

Going down is always free. Going up checks sorts at runtime, except for solvers and proofs, where there is nothing to check: a solver is the same type in both layers, and a typed proof is a sort-erased one under a type of its own. Where the sort-erased counterpart has no type of its own, there is no way back up.

| typed | sort-erased | down | up | |---|---|---|---| | Term α | Term | toUntyped, erase | toTyped(As), typeCheck(As) | | BVar α | BVar | toUntyped, erase | toTyped(As), typeCheck(As) | | NT α | NT | toUntyped, erase | toTyped(As), typeCheck(As) | | Grammar σ | Grammar | toUntyped, erase | toTyped(As), typeCheck(As) | | Solver.Heap s α β | Solver.Heap s | toUntyped, erase | toTyped(As), typeCheck(As) | | Datatype.Ctor α | Datatype.Ctor | toUntyped, erase | toTyped(As), typeCheck(As) | | Datatype.Field α β | Datatype.Selector | toUntyped, erase | toTyped(As), typeCheck(As) | | record Fields fields | Fields names | toUntyped, erase | toTyped(As), typeCheck(As) | | Solver | Solver | toUntyped, relax | toTyped | | Solver.Proof s pc | Solver.Proof s pc | toUntyped, relax | toTyped | | BVars, NTs | BVars, NTs | toUntyped, erase | none | | datatype Args, tuple and application spines | Terms | toUntyped, erase | none | | Datatype.Case α β | Term | toUntyped, erase | none |

The value classes convert too: a typed TermToValue or ValueToTerm instance gives a sort-erased one and the other way round, so a Lean type given conversions in one layer is usable in both.

4.4. Bound variables, lambdas, quantifiers🔗

Cvc.lean's typed API types bound variables just like it types terms.

def

Cvc.Typed.BVar [Ω] (α : Type) : Type
Cvc.Typed.BVar [Ω] (α : Type) : Type

Documentation

A bound variable of the sort α describes.

It also provides a type for collections of BVar-s.

def

Cvc.Typed.BVars [Ω] : Type 1
Cvc.Typed.BVars [Ω] : Type 1

Documentation and 1 equation

A list of bound variables of assorted sorts: a lambda's or a definition's parameters.

Push them in parameter order: BVars.push y (BVars.push x []) stands for the parameters x then y, so its signature to β is X → Y → β.

Equations

Typed.BVars = List ((α : Type) × ToTyp α × Typed.BVar α)

The untyped API for bound variables is very similar but with no type information. Cvc.Untyped.BVars is thus simply an array of untyped bound variables, and all checks are performed at runtime. We only present the typed API in this section.

As long as this list of bound variables (and their type) is known statically, functions such as Term.lambda are able to deconstruct it and infer the type of the corresponding function.

4.4.1. Lambdas🔗

def

Cvc.Typed.Term.lambda [Ω] {β : Type} (bv : Typed.BVars)
  (body : Typed.Term β) :
  Env (Typed.Term (Typed.BVars.signatureTo β bv))
Cvc.Typed.Term.lambda [Ω] {β : Type}
  (bv : Typed.BVars)
  (body : Typed.Term β) :
  Env
    (Typed.Term
      (Typed.BVars.signatureTo β bv))

Documentation

Creates a lambda from some bound variables and a body.

This first example builds the bound variables list and the lambda term by hand, see below for a much more concise version using smt!.

lam := (lambda ((b Bool) (i2 Int) (r Real)) (ite b (< i1 i2) (= r 0.0)))
sat
- b  := false
- i1 := 0
- r  := 0
#eval Env.runIO do
  let i1 ← Term.mkSymbolAs Int "i1"
  let bv_b ← BVar.mk "b"
  let bv_i2 ← BVar.mk "i2"
  let bv_r ← BVar.mk "r"
  let bVars :=
    BVars.empty |>.push bv_b |>.push bv_i2 |>.push bv_r
  --  vvv~~~ `Term (Bool → Int → Rat → Bool)`
  let lam ← Term.lambda bVars
    (← smt! if bv_b then i1 < bv_i2 else bv_r = 0.0)
  println! "lam := {lam}"

  let b ← Term.mkSymbol "b"
  let r ← Term.mkSymbol "r"
  let solver ← Solver.new
  solver.setOpt .smt_produceModels true
  smt! lam b i1 r >>= solver.assert
  solver.checkSat (ifSat := do
    println! "sat"
    println! "- b  := {← b.getValue}"
    println! "- i1 := {← i1.getValue}"
    println! "- r  := {← r.getValue}")

lam := (lambda ((b Bool) (i2 Int) (r Real)) (ite b (< i1 i2) (= r 0.0)))
sat
- b  := false
- i1 := 0
- r  := 0

Using the smt! syntax extension:

lam := (lambda ((b Bool) (i2 Int) (r Real)) (ite b (< i1 i2) (= r 0.0)))
sat
- b  := false
- i1 := 0
- r  := 0
#eval Env.runIO do
  let i1 ← Term.mkSymbolAs Int "i1"
  let lam ← smt!
    -- feel free to use `λ` instead of `fun`
    fun (b : Bool) (i2 : Int) (r : Rat) =>
      if b then i1 < i2 else r = 0.0
  println! "lam := {lam}"

  let b ← Term.mkSymbol "b"
  let r ← Term.mkSymbol "r"
  let solver ← Solver.new
  solver.setOpt .smt_produceModels true
  smt! lam b i1 r >>= solver.assert
  solver.checkSat (ifSat := do
    println! "sat"
    println! "- b  := {← b.getValue}"
    println! "- i1 := {← i1.getValue}"
    println! "- r  := {← r.getValue}")

lam := (lambda ((b Bool) (i2 Int) (r Real)) (ite b (< i1 i2) (= r 0.0)))
sat
- b  := false
- i1 := 0
- r  := 0

4.4.2. Quantifiers🔗

Unlike lambdas, quantifier terms simply have sort Bool which makes typing much easier.

def

Cvc.Typed.Term.mkForall [Ω] (bvs : Typed.BVars) (body : Typed.Term Bool)
  (_nonEmpty : bvs ≠ [] := by
    (try simp) <;>
      fail
        "failed to prove this quantifier binds at least one variable") :
  Env (Typed.Term Bool)
Cvc.Typed.Term.mkForall [Ω]
  (bvs : Typed.BVars)
  (body : Typed.Term Bool)
  (_nonEmpty : bvs ≠ [] := by
    (try simp) <;>
      fail
        "failed to prove this quantifier binds at least one variable") :
  Env (Typed.Term Bool)

Documentation

Universal quantification of body over bvs.

def

Cvc.Typed.Term.mkExists [Ω] (bvs : Typed.BVars) (body : Typed.Term Bool)
  (_nonEmpty : bvs ≠ [] := by
    (try simp) <;>
      fail
        "failed to prove this quantifier binds at least one variable") :
  Env (Typed.Term Bool)
Cvc.Typed.Term.mkExists [Ω]
  (bvs : Typed.BVars)
  (body : Typed.Term Bool)
  (_nonEmpty : bvs ≠ [] := by
    (try simp) <;>
      fail
        "failed to prove this quantifier binds at least one variable") :
  Env (Typed.Term Bool)

Documentation

Existential quantification of body over bvs.

Here is an example of building quantified terms by hand, smt! version below.

exists_i := (exists ((i Int)) (forall ((j Int)) (=> (< n j) (< i j))))
sat
- n := -1
#eval Env.runIO do
  let n ← Term.mkSymbolAs Int "n"
  let i ← BVar.mk "i"
  let j ← BVar.mk "j"
  let bVars_j := BVars.empty.push j
  let all_le ← Term.mkForall bVars_j (← smt! n < j → i < j)
  let bVars_i := BVars.empty.push i
  let exists_i ← Term.mkExists bVars_i all_le
  println! "exists_i := {exists_i}"

  let solver ← Solver.new
  solver.setOpt .smt_produceModels true
  solver.assert exists_i
  solver.checkSat (ifSat := do
    println! "sat"
    println! "- n := {← n.getValue}")

exists_i := (exists ((i Int)) (forall ((j Int)) (=> (< n j) (< i j))))
sat
- n := -1

With the smt! extension:

exists_i := (exists ((i Int)) (forall ((j Int)) (=> (< n j) (< i j))))
sat
- n := -1
#eval Env.runIO do
  let n ← Term.mkSymbolAs Int "n"
  let exists_i ← smt!
    ∃ (i : Int), ∀ (j : Int), n < j → i < j
  println! "exists_i := {exists_i}"

  let solver ← Solver.new
  solver.setOpt .smt_produceModels true
  solver.assert exists_i
  solver.checkSat (ifSat := do
    println! "sat"
    println! "- n := {← n.getValue}"
  )

exists_i := (exists ((i Int)) (forall ((j Int)) (=> (< n j) (< i j))))
sat
- n := -1

4.5. Term inspection🔗

Building terms is half of the story: a solver hands terms back — models, unsat cores, proofs, synthesized functions — and a rewrite has to look inside a term before it replaces it. cvc.lean takes a term apart through a view: the term one level down, its operator as a constructor and its kids, indices and names as fields.

import Cvc.Typed.View (or Cvc.Untyped.View) brings in everything this section uses; import Cvc includes it.

4.5.1. The View of the Imported Theories🔗

Each theory comes with a view of its operators, and def.term_view V gathers the views of every theory the current module imports into one inductive V. A theory that is not imported is not viewed: its terms fall into V's catch-all, other. Besides one constructor per operator, V has leaves for values, declared symbols and bound variables.

section
variable [Ω]
open Typed
def.term_view V
end

In the typed layer V : Typ → Type: V τ is a term of sort τ taken apart. Each operator has a constructor whose kids are typed at their sorts — a comparison's operand sort is a field, which types its kids:

@V.lt : [inst : Ω] → (α : Typ) → {h0 : α.isArith = true} → Typed.Kids α.Denote → V Typ.bool#check @V.lt

@V.lt : [inst : Ω] → (α : Typ) → {h0 : α.isArith = true} → Typed.Kids α.Denote → V Typ.bool

V.of τ t views a term t of sort τ. Matching on the sort alongside the view refines both: at .lt .int ks, the kids ks are Term Ints.

open Typed in an integer comparison of #[(+ x 1), (* 2 x)]
#eval Env.runIO do
  let x ← Term.mkSymbolAs Int "x"
  let t ← smt! x + 1 < 2 * x
  match ← V.of .bool t with
  | .lt .int ks =>
    let kids : Array (Term Int) := ks.val
    println! "an integer comparison of {kids}"
  | _ => println! "something else"

an integer comparison of #[(+ x 1), (* 2 x)]

Matching at the wrong sort is caught statically: the kids of a real comparison are not integers.

open Typed in
example [Ω] (v : V .bool) : Option (Kids Int) :=
  match v with
  | .lt .real ks => some Application type mismatch: The argument
  ks
has type
  Kids Rat
but is expected to have type
  Kids Int
in the application
  some ks

Note: The following definitions were not unfolded because their definition is not exposed:
  Term ↦ 4ks
  | _ => none

Application type mismatch: The argument
  ks
has type
  Kids Rat
but is expected to have type
  Kids Int
in the application
  some ks

Note: The following definitions were not unfolded because their definition is not exposed:
  Term ↦ 4

4.5.2. Folding and Rewriting🔗

Term.fold visits a term's nodes depth first, handing each to two optional functions with its view: pre on reaching the node, which may skip its kids or stop the fold, and post on leaving it. The typed layer has two more, prePlain and postPlain, for the nodes whose sort has no Typ — a quantifier's variable list, for instance.

open Typed in integer symbols: #[x, y]
#eval Env.runIO do
  let x ← Term.mkSymbolAs Int "x"
  let y ← Term.mkSymbolAs Int "y"
  let t ← smt! x < y ∧ y = x + 1
  let syms ← t.fold #[] (pre := fun {τ} _ (v : V τ) acc =>
    match τ, v with
    | .int, .symbol x =>
      if acc.contains x then return .descend acc
      else return .descend (acc.push x)
    | _, _ => return .descend acc)
  println! "integer symbols: {syms}"

integer symbols: #[x, y]

Term.walk visits the nodes through a zipper, which also sees where the node sits, and may replace a node. A typed node's replacement is a term of its sort, so a rewrite cannot build an ill-sorted term; a sort-erased replacement is checked. post sees a node rebuilt with its replaced kids, so a bottom-up rewrite is a post alone — here, removing double negations:

open Typed in (and (not (not p)) (not (not (not q)))) ↦ (and p (not q))
#eval Env.runIO do
  let p ← Term.mkSymbolAs Bool "p"
  let q ← Term.mkSymbolAs Bool "q"
  let t ← smt! ¬ ¬ p ∧ ¬ ¬ ¬ q
  let (s, _) ← t.walk () (post := fun {τ} _ (v : V τ) _ =>
    match τ, v with
    | .bool, .not t => do
      match ← V.of .bool t with
      | .not u => return .replace u ()
      | _ => return .continue ()
    | _, _ => return .continue ())
  println! "{t} ↦ {s}"

(and (not (not p)) (not (not (not q)))) ↦ (and p (not q))

The sort-erased layer works the same way, without the sorts: V.of is a pure function there, and a fold runs in any monad.