14.6. Sentences as data🔗

Most users only need the rcf tactic. Programs that construct or inspect sentences directly use the data types below. An atom compares one integer polynomial with zero under one of the six comparison signs, formulas combine atoms with the Boolean connectives, and a sentence adds the one quantifier the decision procedure supports.

inductive type

Hex.RCF.Formula : Type
Hex.RCF.Formula : Type

Boolean combinations of univariate polynomial atoms.

Constructors

Hex.RCF.Formula.atom (a : Hex.RCF.Atom) : Hex.RCF.Formula

A polynomial comparison.

Hex.RCF.Formula.tt : Hex.RCF.Formula

Truth.

Hex.RCF.Formula.ff : Hex.RCF.Formula

Falsity.

Hex.RCF.Formula.not (φ : Hex.RCF.Formula) : Hex.RCF.Formula

Boolean negation.

Hex.RCF.Formula.and (φ ψ : Hex.RCF.Formula) :
  Hex.RCF.Formula

Boolean conjunction.

Hex.RCF.Formula.or (φ ψ : Hex.RCF.Formula) : Hex.RCF.Formula

Boolean disjunction.

Hex.RCF.Formula.imp (φ ψ : Hex.RCF.Formula) :
  Hex.RCF.Formula

Boolean implication.

inductive type

Hex.RCF.Sentence : Type
Hex.RCF.Sentence : Type

A quantifier-free formula under exactly one real or bounded-real quantifier. Bounded quantifiers use the half-open convention (a, b] inherited from real-root isolations.

Constructors

Hex.RCF.Sentence.forallReal (φ : Hex.RCF.Formula) :
  Hex.RCF.Sentence

Universal quantification over the whole domain.

Hex.RCF.Sentence.existsReal (φ : Hex.RCF.Formula) :
  Hex.RCF.Sentence

Existential quantification over the whole domain.

Hex.RCF.Sentence.forallIoc (a b : Dyadic)
  (φ : Hex.RCF.Formula) : Hex.RCF.Sentence

Universal quantification over the half-open dyadic interval (a, b].

Hex.RCF.Sentence.existsIoc (a b : Dyadic)
  (φ : Hex.RCF.Formula) : Hex.RCF.Sentence

Existential quantification over the half-open dyadic interval (a, b].

def

Hex.RCF.Sentence.toProp : Hex.RCF.Sentence → Prop
Hex.RCF.Sentence.toProp :
  Hex.RCF.Sentence → Prop

Interpret a reflected sentence as a Lean proposition.

The #p[...] literal lists coefficients in ascending degree order and normalizes away trailing zeros. This direct construction represents ∀ x : ℝ, x² + 1 > 0 and sends it through the same compiled decision procedure used by the tactic:

open Hex.RCF

private def positiveQuadratic : Sentence :=
  .forallReal (.atom {
    p := #p[1, 0, 1]
    cmp := .gt
  })

#guard Hex.RCF.decide positiveQuadratic == some true

Bounded sentences use Lean's built-in Dyadic endpoints and the half-open interval (a, b]. This sentence represents ∀ x ∈ Set.Ioc (0 : ℝ) 1, x ≥ 0:

open Hex.RCF

private def nonnegativeOnUnit : Sentence :=
  .forallIoc (Dyadic.ofInt 0) (Dyadic.ofInt 1)
    (.atom {
      p := #p[0, 1]
      cmp := .ge
    })

#guard Hex.RCF.decide nonnegativeOnUnit == some true

For clients that need the evidence as well as the verdict, Hex.RCF.build? returns the certificate together with its replay verdict:

def

Hex.RCF.build? (s : Hex.RCF.Sentence) : Option Hex.RCF.BuildResult
Hex.RCF.build? (s : Hex.RCF.Sentence) :
  Option Hex.RCF.BuildResult

Assemble a certificate and reject it if replay finds malformed evidence.

open Hex.RCF

example (s : Sentence) (result : BuildResult)
    (h : build? s = some result) :
    result.certificate.replay? s =
      some result.verdict :=
  replay_build h

build? s = none means certificate construction or replay failed. It is distinct from a successful result whose verdict is false.