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.

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"}}}

deps.edn

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.

(clojure-version)

0.1s

check clojure versionLaTTe Proof Assistant (Clojure)

"1.10.0"

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

16.9s

requiresClojure+LaTTe (Clojure)

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

0.4s

composition-injectiveClojure+LaTTe (Clojure)

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

(type-check?
 [T :type][U :type][f (==> T U)]
 (pre-image T U f)
 (==> U (set T)))

0.3s

Clojure+LaTTe (Clojure)

true

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

0.4s

Axiom of ChoiceClojure+LaTTe (Clojure)

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

0.3s

Clojure+LaTTe (Clojure)

Vector(3) [:declared, :theorem, ex-right-inverse]

0.4s

Clojure+LaTTe (Clojure)

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

0.4s

Clojure+LaTTe (Clojure)

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

0.3s

Clojure+LaTTe (Clojure)

Vector(2) [:qed, right-inverse-injective]