Quantifiers, typed

A quantified formula is a Term Bool whatever it binds, and so is its body. There are three spellings:

• mkForall/mkExists take the bound variables as a BVars list, as BVars.lambda does.

• forallH/existsH take the body as a Lean function of the variables. Here each variable's sort comes from the type of its argument, so a quantifier reads like a Lean one:

  Term.forallH fun (x y : Term Int) => smt! x + y = y + x
  

• smt! ∀ (x y : Int), x + y = y + x, and ∃ likewise.

A quantifier binds at least one variable: neither spelling accepts none.

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

Universal quantification of body over bvs.

Equations

• Cvc.Typed.Term.mkForall bvs body _nonEmpty = Cvc.Untyped.Term.mkForall bvs.erase body ⋯

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

Existential quantification of body over bvs.

Equations

• Cvc.Typed.Term.mkExists bvs body _nonEmpty = Cvc.Untyped.Term.mkExists bvs.erase body ⋯

Binding through Lean functions

Binder φ says that φ is the type of a quantifier's body written as a Lean function: one Term α argument per bound variable, ending in Env (Term Bool). The variable's sort is α's. There is no instance for a bare Env (Term Bool), so a body binding no variable does not typecheck.

The arguments' types are what the sorts come from, so they must be known: write fun (x : Term Int) => … rather than fun x => … when nothing else in the body pins them down.

class Cvc.Typed.Term.Binder [Ω] (φ : Type) : Type

φ is a quantifier body taking one Term α per bound variable.

• bind : List String → Nat → φ → Env (Untyped.BVars × Term Bool)

  Creates one bound variable per argument of f and applies f to them.

  The i-th variable is named names[i], or x{i} when names has no such element.

@[reducible, inline]

abbrev Cvc.Typed.Term.Binder.nameAt (names : List String) (i : Nat) : String

The name of the i-th bound variable: names[i], or x{i} when there is none.

Equations

• Cvc.Typed.Term.Binder.nameAt = Cvc.Typed.Term.LambdaBinder.nameAt

@[instance_reducible]

instance Cvc.Typed.Term.instBinderForallEnvBoolOfToTyp [Ω] {α : Type} [ToTyp α] : Binder (Term α → Env (Term Bool))

The binder for a body taking the last bound variable.

Equations

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

@[instance_reducible]

instance Cvc.Typed.Term.instBinderForallOfToTyp [Ω] {α ψ : Type} [ToTyp α] [Binder ψ] : Binder (Term α → ψ)

The binder for a body taking a bound variable and more.

Equations

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

def Cvc.Typed.Term.forallH [Ω] {φ : Type} [Binder φ] (body : φ) (names : List String := []) : Env (Term Bool)

Universal quantification of a body written as a Lean function of its variables.

names names the variables in the order the function takes them; a variable without one is named x{i}, after its position.

Equations

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

def Cvc.Typed.Term.existsH [Ω] {φ : Type} [Binder φ] (body : φ) (names : List String := []) : Env (Term Bool)

Existential quantification of a body written as a Lean function of its variables.

names names the variables in the order the function takes them; a variable without one is named x{i}, after its position.

Equations

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

Viewing a quantifier

The variables' sorts come as a list of Typs, as an application's arguments do, and the body mentions the variables: walking into it meets them as the aggregate's bvar leaf.

inductive Cvc.Typed.View.Quant.Vars [Ω] : List Typ → Type

A binder's variables, each a BVar σ.Denote at its sort σ, in order; never empty.

• last [Ω] {τ : Typ} (x : BVar τ.Denote) : Vars [τ]

  The last variable.

• cons [Ω] {τs : List Typ} {τ : Typ} (x : BVar τ.Denote) (rest : Vars τs) : Vars (τ :: τs)

  One more variable, in front of the others.

def Cvc.Typed.View.Quant.Vars.toBVars [Ω] {doms : List Typ} (vars : Vars doms) : BVars

The same variables as a BVars list, so that a viewed binder can be rebuilt.

Equations

• vars.toBVars = Cvc.Typed.View.Quant.Vars.toBVars.go✝ vars []

theorem Cvc.Typed.View.Quant.Vars.toBVars_ne_nil [Ω] {doms : List Typ} (vars : Vars doms) : vars.toBVars ≠ []

A binder always has a variable, so its BVars are never empty: what mkForall asks for.

def Cvc.Typed.View.Quant.Vars.toStrings [Ω] {doms : List Typ} : Vars doms → List String

The variables as cvc5 prints them, x : Int.

Equations

• (Cvc.Typed.View.Quant.Vars.last x_1).toStrings = [toString x_1.toTerm ++ toString " : " ++ toString τ]
• (Cvc.Typed.View.Quant.Vars.cons x_1 rest).toStrings = (toString x_1.toTerm ++ toString " : " ++ toString τ) :: rest.toStrings

inductive Cvc.Typed.View.Quant [Ω] : Typ → Type

A quantified formula taken apart one level; always of sort Bool.

forall and exists are Lean keywords, hence the primes. The instantiation patterns stay sort-erased, a pattern mixing sorts.

• forall' [Ω] (doms : List Typ) (vars : Vars doms) (body : Term Bool) (patterns : Option Untyped.Term) : View.Quant Typ.bool

  ∀ x₁ … xₙ, body, with cvc5's instantiation patterns if it has any.

• exists' [Ω] (doms : List Typ) (vars : Vars doms) (body : Term Bool) (patterns : Option Untyped.Term) : View.Quant Typ.bool

  ∃ x₁ … xₙ, body, with cvc5's instantiation patterns if it has any.

def Cvc.Typed.View.Quant.of [Ω] (τ : Typ) (t : Term τ.Denote) : Env (Option (View.Quant τ))

Takes a quantified formula apart one level, none for any other term.

Also none when a variable's sort is one no Typ describes.

Equations

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

smt!

A binder's type is the variable's index, so smt! ∀ (x : Int), x + 0 = x binds a Term Int.