Documentation

HexRCF.Syntax

source
inductive Hex.RCF.Cmp :
Type

The six comparisons supported by reflected polynomial atoms.

  • lt : Cmp

    The relation <.

  • le : Cmp

    The relation ≤.

  • eq : Cmp

    The relation =.

  • ge : Cmp

    The relation ≥.

  • gt : Cmp

    The relation >.

  • ne : Cmp

    The relation ≠.

Instances For
    source
    @[instance_reducible]
    instance Hex.RCF.instDecidableEqCmp :
    DecidableEq Cmp
    Equations
    source
    structure Hex.RCF.Atom :
    Type

    An atomic comparison between an integer polynomial and zero.

    • p : ZPoly

      The integer polynomial on the left of the comparison.

    • cmp : Cmp

      The comparison with zero.

    Instances For
      source
      @[instance_reducible]
      instance Hex.RCF.instDecidableEqAtom :
      DecidableEq Atom
      Equations
      source
      def Hex.RCF.instDecidableEqAtom.decEq (x✝ x✝¹ : Atom) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        inductive Hex.RCF.Formula :
        Type

        Boolean combinations of univariate polynomial atoms.

        Instances For
          source
          @[instance_reducible]
          instance Hex.RCF.instDecidableEqFormula :
          DecidableEq Formula
          Equations
          source
          def Hex.RCF.instDecidableEqFormula.decEq (x✝ x✝¹ : Formula) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            inductive 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.

            • forallReal (φ : Formula) : Sentence

              Universal quantification over the whole domain.

            • existsReal (φ : Formula) : Sentence

              Existential quantification over the whole domain.

            • forallIoc (a b : Dyadic) (φ : Formula) : Sentence

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

            • existsIoc (a b : Dyadic) (φ : Formula) : Sentence

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

            Instances For
              source
              @[instance_reducible]
              instance Hex.RCF.instDecidableEqSentence :
              DecidableEq Sentence
              Equations
              source
              def Hex.RCF.instDecidableEqSentence.decEq (x✝ x✝¹ : Sentence) :
              Decidable (x✝ = x✝¹)
              Equations
              Instances For
                source
                def Hex.RCF.Formula.polys :
                Formula → List ZPoly

                All atom polynomials in a formula, in deterministic left-to-right order.

                Equations
                Instances For
                  source
                  def Hex.RCF.Sentence.formula :
                  Sentence → Formula

                  The body of a one-quantifier sentence.

                  Equations
                  Instances For
                    source
                    def Hex.RCF.Sentence.polys (s : Sentence) :
                    List ZPoly

                    The positive-degree atom polynomials used by the carrier decomposition. Constant atoms remain in the reflected formula but, after their truth values are evaluated, do not contribute carrier boundaries.

                    Equations
                    Instances For
                      source
                      def Hex.RCF.Sentence.product (s : Sentence) :
                      ZPoly

                      The product of all nonconstant atom polynomials.

                      Equations
                      Instances For