Proposal for adding Dependent Pairs (Σ-types) to LaTTe

[zampino]

Hello @fredokun 👋 .

First of all thank you very much for suggesting to read Nederpelt's book on type theory and formal proof, it's great to get the overall picture on the lambda cube and the formalisation of maths via types.

I've been reading some papers around formalising mathematics in Coq (e.g. [1], [2] and the introduction to [HoTT]), to have some inspiration for formalising some algebra in LaTTe. A lot of concepts there revolved around dependent pairs, so I thought it could be a nice exercise to try add them to Latte.

I've written an executable notebook https://nextjournal.com/zampino/latte-sigma to explore sigma types and dependent pairs running the code of the fork (and posing some questions :-). If you have an account on nextjournal, I can add you as collaborator there, so that you can run the code. Or you can remix it under your profile.

In the notebook I'm showing modeling of the existential quantifier in terms of a Σ-type and the possibility of defining struct like types via combinations of Σ-types. That seems to work already at this stage of the changes. Here is a static summary :-)

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

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

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

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

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

  (qed q))

For calculating type of pairs, I've been following the reduction rules in the book (sorry for the screenshot).

Far from being ready to merge, in opening an early stage PR I wanted to gauge your possible interest in this or getting some suggestions in general. Maybe defining a roadmap or maybe closing it if it's out of scope for the project? It should be only accretive and shouldn't impact the rest of the kernel functionalities.

[fredokun]

Hello @zampino It's a great PR I am very happy that you find LaTTe interesting enough to even contribute to it ! I have quickly looked at the code, it's very clean and clearly following the current LaTTe style. I have mixed feeling about sigma types, and this is because of the TTFP book (type theory and formal proof). I guess you have read the comments about sigma types (p. 300 in the book) since the rules are given there. In the discussion, I see no compelling arguments in favor of sigma-types for encoding the existentials or subset types. But in the mean time I see no compelling arguments against having them in the kernel, and optionally use them for alternative encodings. As you explain in your nextjournal notebook, this already simplifies the proofs. So here is my proposition : I will create a sigma-types branch and we will interact directly on this branch. We'll postpone until later the decision about wether it's an alternative implementation, or merge into master. Note that I am also interested in sigma-types for the encoding of inductives (which I planned at a later stage, but I don't want them into the kernel because I want to preserve decidability of typing and uniqueness). As a final remark (before creating the branch) I think the normalization must be updated because we have to normalize inside pairs, and also normalize projections. But let's talk about this in the dedicated branch.

[zampino]

Nice, thank you.

I guess you have read the comments about sigma types

Yes I did, and I find the encoding of sets via predicates fine enough. I was mostly looking at dependent pairs to encode quotients of algebraic structures. It seems easier to transport say some binary operation from the carrier type to some choice of representatives for equivalence classes if these are expresses as dependent pairs. But I still need to grasp the details of this construction.

But let's talk about this in the dedicated branch

sure.