TUTORIAL

This tutorial demonstrates core primitives with examples, annotated with mathematical equivalents and theorems from the system.

Basic Constructs

let universal : exp = Power Prop

Defines the power set of propositions, , a higher type in .

let set_a : exp =
  Set (Lam ("x", Real,
    RealIneq (Gt, Var "x", Zero)))

Represents the set of positive reals, .

let sup_a : exp = Sup set_a

Computes the supremum, , as the set is unbounded above.

let inf_a : exp = Inf set_a

Computes the infimum, , the greatest lower bound.

Intervals and Measures

let interval_a_b (a : exp) (b : exp) : exp =
  Set (Lam ("x", Real,
    And (RealIneq (Lte, a, Var "x"),
         RealIneq (Lte, Var "x", b))))

Defines the closed interval .

let lebesgue_measure (a : exp) (b : exp) : exp =
  Mu (Real, Power (Set Real),
    Lam ("A", Set Real,
      If (RealIneq (Lte, a, b),
          RealOps (Minus, b, a),
          Infinity)))

Constructs the Lebesgue measure: for , otherwise.

Integration

let integral_term : exp =
  Lam ("f", Forall ("x", Real, Real),
    Lam ("a", Real, Lam ("b", Real,
      Lebesgue (Var "f",
        Mu (Real, Power (Set Real),
          Lam ("A", Set Real,
            If (And (RealIneq (Lte, Var "a", Var "b"),
            SetEq (Var "A", interval_a_b (Var "a") (Var "b"))),
        RealOps (Minus, Var "b", Var "a"), Zero))),
        interval_a_b (Var "a") (Var "b")))))

Defines the Lebesgue integral , with .

let integral_sig : exp =
  Forall ("f", Forall ("x", Real, Real),
    Forall ("a", Real, Forall ("b", Real, Real)))

Type signature for the integral: .

let l2_space : exp =
  Lam ("f", Forall ("x", Real, Real),
    RealIneq (Lt, Lebesgue (Lam ("x", Real,
      RealOps (Pow, RealOps (Abs, App (Var "f", Var "x"), Zero),
      RealOps (Plus, One, One))),
      lebesgue_measure Zero Infinity,
      interval_a_b Zero Infinity), Infinity))

Defines the space: , .

Sequences and Limits

let sequence_a : exp =
    Lam ("n", Nat, RealOps (Div, One, NatToReal (Var "n")))

Sequence , converging to 0.

let limit_a : exp =
  Limit (Seq sequence_a, Infinity, Zero,
    Lam ("ε", Real, Lam ("p", RealIneq (Gt, Var "ε", Zero),
      Pair (RealOps (Div, One, Var "ε"),
        Lam ("n", Nat, Lam ("q", RealIneq (Gt, Var "n", Var "N"),
          RealIneq (Lt, RealOps (Abs,
          RealOps (Minus, App (sequence_a, Var "n"), Zero), Zero),
            Var "ε")))))))

Proves : , , , .

let sequence_e : exp =
  Lam ("n", Nat,
    RealOps (Pow,
      RealOps (Plus, One,
        RealOps (Div, One, NatToReal (Var "n"))),
        NatToReal (Var "n")))

Sequence for .

let e : exp =
  Fst (Pair (RealOps (Exp, One, One),
    Limit (Seq sequence_e, Infinity,
      RealOps (Exp, One, One), ...)))

Defines , with limit proof truncated for brevity.

Testing and Verification

let test_set_eq : exp =
  Forall ("x", Real, iff_intro (Lam ("x",
    RealIneq (Lte, Var "x", One), ...

Verifies set equality: .

Runs type and term tests, ensuring correctness (e.g., .