Adding dependent Pairs to LaTTe

I'm working on some changes to LaTTe kernel for adding Σ-types. This notebook is a runnable playground to show properties of dependent pairs within LaTTe type constructs . As a first result we're showing how Σ-types can encode the existential quantifier, obtaining much easier proofs for introduction and elimination rules. I'm also exploring the formation of compound struct-likes types via a combination of Σ-types.

Here I'm sourcing latte-prelude from my repo, which in turn sources the forked latte-kernel.

{:deps
 {org.clojure/clojure 
  {:mvn/version "1.10.0"}
	compliment 
  {:mvn/version "0.3.9"}
  latte-prelude
  {:git/url "https://github.com/zampino/latte-prelude"
   :sha "94b2a25731ba1ea741b8eb14ec3a1695cfa5d7b6"}}}

deps.edn

(ns latte-sigma
  (:refer-clojure :exclude [= and or not set equal])
  (:require [latte.core :as l :refer [definition
                                      defimplicit
                                      defthm
                                      try-proof assume have qed]]
            [latte-prelude.prop :as p :refer [<=>]]
            [latte-prelude.equal :as equal]))

0.1s

Sigma Ex (Clojure)

Routine Type checking

Following the following reduction rules [TODO: write formulas]

\frac{\Sigma}{\Pi}

The constant pair for the pairing constructor was added as well as pr1, pr2 for projections and the binding form (Σ [t T] M) for the type of dependent pairs, with the following typing properties:

(l/type-check?
 [A :type][B :type][a A][b B]
 (pair a b)
 (Σ [x A] B))

0.0s

Sigma Ex (Clojure)

true

(pr (l/type-of
      [T :type][P (==> T :type)][u T][v (P u)]
      (pair u v)))

0.6s

Sigma Ex (Clojure)

(definition s "section from base to set"
  [[T :type][P (==> T :type)]]
  (λ [t T] (==> T (P t))))

(prn (l/type-of
      [T :type][P (==> T :type)]
      [t T][f ((s T P) t)]
      (pair t (f t))))

(prn (l/type-of
      [T :type][P (==> T :type)]
      [t T][f ((s T P) t)]
      (pr1 (pair t (f t)))))

(prn (l/type-of
      [T :type][P (==> T :type)]
      [t T][f ((s T P) t)]
      (pr2 (pair t (f t)))))

0.6s

Sigma Ex (Clojure)

Modeling the existential Quantifier

Sigma types are dual to product types, if the latter can encode the universal quantifier the first can model the existential quantifier. We define

(definition ex-sigma-def
  "The existential quantifier via Σ type"
  [[T :type][P (==> T :type)]]
  (Σ [x T] (P x)))

(defimplicit ex'
  "The existential quantifier, expressed implicitely via Σ types"
  [def-env ctx [P P-ty]]
  (let [[T _] (p/decompose-impl-type def-env ctx P-ty)]
    (list #'ex-sigma-def T P)))

(defthm ex-sigma-elim-thm
  "Σ-Existential Quantifier Elimination "
  [[T :type][P (==> T :type)][A :type]]
  (==> (ex' P)
       (forall [x T] (==> (P x) A))
       A))

0.2s

Sigma Ex (Clojure)

Vector(3) [:declared, :theorem, ex-sigma-elim-thm]

A prof for elimination of the existential quantifier becomes super short, it suffices to exhibit a lambda term applying the implication form to the components of a pair which witnesses the Σ-type.

(try-proof 'ex-sigma-elim-thm
  (qed
    (λ [p (Σ [t T] (P t))]
      (λ [f (Π [x T] (==> (P x) A))]
        (f (pr1 p) (pr2 p))))))

0.1s

Sigma Ex (Clojure)

Vector(2) [:qed, ex-sigma-elim-thm]

Compare the above with the natural application to ordinary pairs, i.e. inhabitants of the conjunction type (and A B). We can also give a somewhat longer proof

(try-proof 'ex-sigma-elim-thm
  (assume [p (ex' P)
           f (∀ [x T] (==> (P x) A))]
    (have g (==> (P (pr1 p)) A) :by (f (pr1 p)))
    (have a A :by (g (pr2 p))))
  (qed a))

0.1s

Sigma Ex (Clojure)

Vector(2) [:qed, ex-sigma-elim-thm]

Also introduction theorems become very easy to prove

(defthm ex-sigma-intro-thm
  "Σ-Existential Quantifier Introduction"
  [[T :type][P (==> T :type)][t T]]
  (==> (P t) (ex' P)))

(try-proof 'ex-sigma-intro-thm
  (qed (λ [x (P t)] (pair t x))))

0.1s

Sigma Ex (Clojure)

Vector(2) [:qed, ex-sigma-intro-thm]

and agan a longer proof

(try-proof 'ex-sigma-intro-thm
  (assume [w (P t)]
    (have q (ex' P) :by (pair t w)))
  (qed q))

0.1s

Sigma Ex (Clojure)

Vector(2) [:qed, ex-sigma-intro-thm]

Compound Types via Σ-types (structs?)

Sigma types comes also at hand for constructing compound (struct like) types, projections being now constants of the language

(definition magma 
  "Bourbakian Magma over a type"
  [[T :type]]
  (==> T T T))

0.1s

Sigma Ex (Clojure)

Vector(3) [:defined, :term, magma]

(def = equal/equal)
(definition associative 
  "associativity of a magma"
  [[T :type][m (magma T)]]
  (forall [a b c T]
    (= (m (m a b) c)
       (m a (m b c)))))

0.1s

Sigma Ex (Clojure)

Vector(3) [:defined, :term, associative]

(definition l-identity
  "right identity"
  [[T :type][m (magma T)][e T]]
  (forall [x T] (= (m x e) x)))

0.1s

Sigma Ex (Clojure)

Vector(3) [:defined, :term, l-identity]

(definition Monoid 
  "a (right) Monoid is an associative magma with right identity"
  [[T :type]]
  (Σ [e T]
     (Σ [m (magma T)]
        (Σ [l (l-identity T m e)]
           (associative T m)))))

0.1s

Sigma Ex (Clojure)

Vector(3) [:defined, :term, Monoid]

Now given a type T, from an inhabitant of the Monoid type (a 4-tuple) we can rebuild witnesses for its properties by applying a combination of the projections. [TODO] define right leaning tuples. And typing doesn't blow up :-)

(l/type-of
 [T :type]
 (Monoid T))

0.1s

Sigma Ex (Clojure)

✳

(l/type-of 
 [T :type][m (Monoid T)]
 (pr1 (pr2 m)))

0.0s

Sigma Ex (Clojure)

List(4) (==>, T, T, T)

(definition set "Sets are Predicates"
  [[T :type]]
  (==> T :type))

(definition set-equal
  [[T :type][P (set T)][Q (set T)]]
  (∀ [t T] (<=> (P t) (Q t))))

0.5s

Sigma Ex (Clojure)

Vector(3) [:defined, :term, set-equal]

(definition xchoice 
  "a choice on sets"
  [[T :type]]
  (Π [P (set T)] (==> (ex' P) T)))

0.1s

Sigma Ex (Clojure)

Vector(3) [:defined, :term, xchoice]

(definition correct 
  "the chosen element satiesfies the predicate"
  [[T :type][x (xchoice T)]]
  (∀ [P (set T)]
     (∀ [xP (ex' P)] (P (x P xP)))))

0.1s

Sigma Ex (Clojure)

Vector(3) [:defined, :term, correct]

(definition extensional
  [[T :type][f (xchoice T)]]
  (∀ [P Q (set T)]
    (∀ [xP (ex' P)]
      (∀ [xQ (ex' Q)]
        (==> (set-equal T P Q)
             (= (f P xP) (f Q xQ)))))))

0.2s

Sigma Ex (Clojure)

Vector(3) [:defined, :term, extensional]

todo define quotients as sigma types

(Quot M xc rho) := (Σ [t T] (= t (xc (class-of rho t) (exrefl rho t))))

Open Questions

I didn't have to touch beta-delta reduction in adding pairs, but it sufficed to touch typing . This is maybe not surprising as pairs cannot be reduced? Can we introduce redexes for applying functions to pairs provided the application has the correct type (like in the ex-elimination above)?

Following the Σ-typed approach to structs, what do we actually gain, apart from a reduced context, with respect to defining structures via an ordinary latte-prelude.prop/and? How could we define a struct constructor with named fields à la Coq (or Clojure) records?

In case of non-dependent pairs, is it worth introducing an unparser for ordinary pairs (say (X A B) the cartesian product) in the same way ==> corresponds to non-dependent functions in (Π [a A] B)? And what would be the relation between (X A B) and (p/and A B)?