Documentation

LeanCert.Examples.Basic

Basic Examples #

This file demonstrates LeanCert's verified interval arithmetic core.

All examples in this file use only the fully-verified subset of expressions: const, var, add, mul, neg, sin, cos

The correctness theorems (evalInterval_correct, evalDual_val_correct) are FULLY PROVED with no sorry, no axioms for this subset.

Building supported expressions #

source
def LeanCert.Examples.Basic.xSq :
Core.Expr

The expression x² (x squared)

Equations
Instances For
    source
    def LeanCert.Examples.Basic.xSq_supported :
    Core.ExprSupported xSq

    Proof that x² is in the supported subset

    Equations
    Instances For
      source
      def LeanCert.Examples.Basic.exprSquare :
      Core.Expr

      The expression x² + 2x + 1 = (x + 1)²

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def LeanCert.Examples.Basic.exprSquare_supported :
        Core.ExprSupported exprSquare

        Proof that x² + 2x + 1 is in the supported subset

        Equations
        Instances For
          source
          def LeanCert.Examples.Basic.exprSinCos :
          Core.Expr

          The expression sin(x) + cos(x)

          Equations
          Instances For
            source
            def LeanCert.Examples.Basic.exprSinCos_supported :
            Core.ExprSupported exprSinCos

            Proof that sin(x) + cos(x) is in the supported subset

            Equations
            Instances For

              Interval construction #

              source
              def LeanCert.Examples.Basic.I01 :
              Core.IntervalRat

              The unit interval [0, 1]

              Equations
              Instances For
                source
                def LeanCert.Examples.Basic.symInterval :
                Core.IntervalRat

                The interval [-1, 1]

                Equations
                Instances For
                  source
                  def LeanCert.Examples.Basic.smallInterval :
                  Core.IntervalRat

                  A small interval around 0: [-1/10, 1/10]

                  Equations
                  Instances For

                    Interval membership examples #

                    Expression evaluation examples #

                    Verified interval evaluation #

                    Using smart constructors #

                    source
                    def LeanCert.Examples.Basic.xSq' :
                    { e : Core.Expr // Core.ExprSupported e }

                    Build x² using smart constructors that carry the support proof

                    Equations
                    Instances For

                      Multi-variable example #

                      source
                      def LeanCert.Examples.Basic.exprXY :
                      Core.Expr

                      The expression x * y (product of two variables)

                      Equations
                      Instances For
                        source
                        def LeanCert.Examples.Basic.exprXY_supported :
                        Core.ExprSupported exprXY
                        Equations
                        Instances For
                          source
                          def LeanCert.Examples.Basic.ρ_xy :
                          Engine.IntervalEnv

                          Multi-variable interval environment

                          Equations
                          Instances For