# LaTTe Environment

This article builds a reusable nextjournal environment for LaTTe

LaTTe is a proof assistant library for the Clojure programming language based on a simple dependent-typed lambda-calculus.

## Dependencies

We're installing LaTTe Kernel along with the standard library and typed sets theory.

{:deps {org.clojure/clojure {:mvn/version "1.10.0"} latte {:mvn/version "1.0b2-SNAPSHOT"} latte-prelude {:mvn/version "1.0b2-SNAPSHOT"} latte-sets {:mvn/version "1.0b2-SNAPSHOT"} compliment {:mvn/version "0.3.9"}}}

The dependency snippet above is mounted as *deps.edn* file into the clojure runtime we're using:

This environment is exported in order to be transcluded from within other articles needing LaTTe libraries.

(clojure-version)

## Some basic examples of proofs for functional properties

We'll take a short tour of the techniques used by LaTTe to prove theorems. See latte-prelude reference for available *classic* theorems, definitions, and axioms.

(ns latte-hello-world (:refer-clojure :exclude [and or not set]) (:require [latte.core :as latte :refer [defthm defimplicit definition example defaxiom proof assume have pose qed type-check?]] [latte-prelude.fun :refer [injective surjective compose]] [latte-sets.core :refer [set elem set-equal emptyset] :as sets] [latte-prelude.equal :refer [equal] :as e] [latte-prelude.prop :refer [not and or absurd]] [latte-prelude.quant :refer [exists ex ex-elim] :as q] [latte-sets.core]))

As a first proof we show a very basic result about function:

(defthm compose-injective "If the composition of two functions is injective, then the right function is injective." [[T :type] [U :type] [V :type] [f (==> U V)] [g (==> T U)]] (==> (injective (compose f g)) (injective g))) (proof compose-injective (assume [Hc (injective (compose f g)) x T y T Hi (equal (g x) (g y))] (have <a> (equal (f (g x)) (f (g y))) :by (e/eq-cong f Hi)) (have <b> (equal ((compose f g) x) ((compose f g) y)) :by <a>) (have <c> (equal x y) :by (Hc x y <b>))) "(Hc x y <b>) takes instances x,y of type T, and the codomain equality" (qed <c>))

Somewhat more involved is to show that *every surjective function has a right inverse*. This, and the above results, are not contained in LaTTe prelude.

(definition pre-image "Given a function f of T in U, gives a predicate over U describing pre-images of elements of U via f" [[T :type][U :type][f (==> T U)]] (lambda [u U] (lambda [t T] (equal (f t) u)))) (type-check? [T :type][U :type][f (==> T U)] (pre-image T U f) (==> U (set T)))

In order to prove the existence of right inverses, we need to extend LaTTe by the classical **Axiom of Choice** in its typed variant. *Given a family of non-empty sets over the type T indexed over a type U, it's possible to choose an element in each set respecting the indexing*.

(defaxiom ax-choice "There exists a choice function for every family of non-empty sets." [[T :type][U :type]] (forall [F (==> U (set T))] (==> (forall [u U] (not (set-equal (F u) (emptyset T)))) (exists [c (==> U T)] (forall [u U] (elem (c u) (F u)))))))

(definition right-inverse "" [[T :type][U :type][f (==> T U)][g (==> U T)]] (forall [u U] (equal (f (g u)) u))) (defthm ex-right-inverse "Given a surjective function g there exists a right inverse of g." [[T :type][U :type]] (forall [f (==> T U)] (==> (surjective f) (exists [g (==> U T)] (right-inverse T U f g)))))

(proof ex-right-inverse (assume [f (==> T U) s (surjective f)] (pose pre := (pre-image T U f)) (pose I := (lambda [g (==> U T)] (forall [u U] (elem (g u) (pre u))))) (assume [u U] (pose N := (lambda [t T] (elem t (pre u)))) (have <exn> (ex N) :by (s u)) (pose E := (set-equal (pre u) (emptyset T))) (assume [t T n (N t) e E] (pose L := (lambda [s (set T)] (elem t s))) (have <l> (L (pre u)) :by n) (have <ll> ((emptyset T) t) :by ((sets/set-equal-prop T (pre u) (emptyset T) L) e n)) (have <no> absurd :by <ll>)) (have <ss> (forall [t T] (==> (N t) (not (set-equal (pre u) (emptyset T))))) :by <no>) (pose AA := (not (set-equal (pre u) (emptyset T)))) (have <aa> (not (set-equal (pre u) (emptyset T))) :by ((ex-elim N AA) <exn> <ss>))) (have <f> (forall [u U] (not (set-equal (pre u) (emptyset T)))) :by <aa>) "We can assert existence of an inverse in the form I" (have <i> (ex I) :by (((ax-choice T U) pre) <f>)) "Now we're going to prove the actual inverse statement." (pose J := (lambda [g (==> U T)] (forall [u U] (equal (f (g u)) u)))) (assume [g (==> U T)] (assume [u U e (elem (g u) (pre u))] (have <e> ((pre u) (g u)) :by e) (have <e1> (equal (f (g u)) u) :by <e>))) (have <a> (forall [g (==> U T)] (forall [u U] (==> (elem (g u) (pre u)) (equal (f (g u)) u)))) :by <e1>) (assume [g (==> U T)] (assume [ig (I g)] (assume [u U] (have <s> (equal (f (g u)) u) :by ((<a> g u) (ig u)))) (have <jg> (J g) :by <s>) (have <exj> (ex J) :by ((q/ex-intro J g) <jg>)))) (pose A := (forall [g (==> U T)] (==> (I g) (ex J)))) (have <igexj> A :by <exj>) (have <exj'> (ex J) :by ((q/ex-elim I (ex J)) <i> <igexj>)) (have <proven> (exists [g (==> U T)] (forall [u U] (equal (f (g u)) u))) :by <exj'>)) (qed <proven>))

Let's conclude with another basic results on functions:

(defthm right-inverse-injective "The right inverse of a function is always injective." [[T :type][U :type][f (==> T U)]] (forall [g (==> U T)] (==> (right-inverse T U f g) (injective g)))) (proof right-inverse-injective (assume [g (==> U T) r (right-inverse T U f g) u U v U e (equal (g u) (g v))] (have <e> (equal (f (g u)) (f (g v))) :by (e/eq-cong f e)) (have <g> (equal (f (g u)) u) :by (r u)) (have <g'> (equal u (f (g u))) :by (e/eq-sym <g>)) (have <h> (equal (f (g v)) v) :by (r v)) (have <i> (equal (f (g u)) v) :by (e/eq-trans <e> <h>)) (have <j> (equal u v) :by (e/eq-trans <g'> <i>))) (qed <j>))