Andrea Amantini / Aug 22 2019
Remix of Clojure by Nextjournal

LaTTe Environment

This article builds a reusable nextjournal environment for LaTTe

LaTTe Proof Assistant
LaTTe Proof Assistant (Clojure)
exporting environment

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


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

  {:mvn/version "1.10.0"}
  {:mvn/version "1.0b2-SNAPSHOT"}
  {:mvn/version "1.0b2-SNAPSHOT"}
  {:mvn/version "1.0b2-SNAPSHOT"}
  compliment {:mvn/version "0.3.9"}}}
Extensible Data Notation

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

LaTTe Proof Assistant
LaTTe Proof Assistant (Clojure)
exporting environment

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


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
            [ :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]

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>))
Vector(2) [:qed, compose-injective]

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))))

 [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)))))))
Vector(3) [:declared, :axiom, ax-choice]
(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)))))
Vector(3) [:declared, :theorem, ex-right-inverse]
Clojure+LaTTe (Clojure)
LaTTe Proof Assistant
(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>))
Vector(2) [:qed, ex-right-inverse]

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>))
Vector(2) [:qed, right-inverse-injective]