Quantifiers, sort-erased

A quantified formula binds its variables the way a lambda does: they are BVars gathered into a variable list, and the body mentions them as ordinary terms. Two spellings are offered.

• mkForall/mkExists take the bound variables explicitly, as BVars.lambda does.
• forallH/existsH take the body as a Lean function of the variables, so that no BVar is ever written by hand. The H is for higher-order abstract syntax: binding is borrowed from Lean's own fun.

A quantifier binds at least one variable, cvc5 rejecting an empty variable list. Asserting a quantified formula needs a logic with quantifiers, such as the default ALL; a QF_ logic rejects it.

cvc5's WITNESS binder is deliberately not wrapped: asserting a term that contains one aborts the process rather than raising an error.

def Cvc.Untyped.Term.mkForall [Ω] (bvs : BVars) (body : Term) (_nonEmpty : 0 < Array.size bvs := by (try grind) <;> fail "failed to prove a quantifier binds at least one variable") : Env Term

Universal quantification of body over bvs.

Equations

• Cvc.Untyped.Term.mkForall bvs body _nonEmpty = Cvc.Untyped.Term.mkQuant✝ cvc5.Kind.FORALL bvs body

def Cvc.Untyped.Term.mkExists [Ω] (bvs : BVars) (body : Term) (_nonEmpty : 0 < Array.size bvs := by (try grind) <;> fail "failed to prove a quantifier binds at least one variable") : Env Term

Existential quantification of body over bvs.

Equations

• Cvc.Untyped.Term.mkExists bvs body _nonEmpty = Cvc.Untyped.Term.mkQuant✝ cvc5.Kind.EXISTS bvs body

Binding through Lean functions

The body is a Lean function of the variables, one Term argument per variable, as for Term.lambdaH: see Binder, which both share.

def Cvc.Untyped.Term.forallH [Ω] {φ : Type} [Binder φ] (binders : List (String × Srt)) (body : φ) : Env Term

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

binders names each variable and gives its sort, in the order the function takes them:

Term.forallH [("x", int), ("y", int)] fun x y => do Term.equal (← Term.add x y) (← Term.add y x)

Equations

• Cvc.Untyped.Term.forallH binders body = do let __x ← Cvc.Untyped.Term.Binder.bindAll binders body match __x with | (bvs, body) => Cvc.Untyped.Term.mkQuant✝ cvc5.Kind.FORALL bvs body

def Cvc.Untyped.Term.existsH [Ω] {φ : Type} [Binder φ] (binders : List (String × Srt)) (body : φ) : Env Term

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

binders names each variable and gives its sort, in the order the function takes them.

Equations

• Cvc.Untyped.Term.existsH binders body = do let __x ← Cvc.Untyped.Term.Binder.bindAll binders body match __x with | (bvs, body) => Cvc.Untyped.Term.mkQuant✝ cvc5.Kind.EXISTS bvs body

The view of a quantifier

Written by hand, as the quantifiers are: a bound variable is not something a specification describes. forall and exists are Lean keywords, hence the primes.

inductive Cvc.Untyped.View.Quant [Ω] : Type

A quantified formula, taken apart one level, sort-erased.

• forall' [Ω] (vars : BVars) (body : Term) (patterns : Option Term) : View.Quant

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

• exists' [Ω] (vars : BVars) (body : Term) (patterns : Option Term) : View.Quant

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

def Cvc.Untyped.View.Quant.of? [Ω] (t : Term) : Option View.Quant

Takes a term apart one level, if it is a quantified formula.

Equations

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

smt!

smt! ∀ (x y : s) (b : t), body and smt! ∃ … are Lean's own quantifier syntax, binders in parentheses as fun takes them. A binder's sort is a Lean type (Int) or a Srt value (int).

The body extends as far right as it can, as in Lean, so a quantifier in argument position needs parentheses. Each variable is named as the writer named it, which is also the name cvc5 prints.

def Cvc.smtForall : Lean.ParserDescr

Universal quantification.

Equations

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

def Cvc.smtExists : Lean.ParserDescr

Existential quantification.

Equations

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