HoTT in Lean 3

[Floris van Doorn]

A followup to my previous email in another discussion (copied below).

I said in that email that the kernel of Lean 3 is inconsistent with univalence. While this is true, we are currently developing a HoTT library for Lean 3 here:

https://github.com/gebner/hott3

The logic in this library is consistent in the following sense described below. 

In Lean you can define inductive types and inductive propositions. Most inductive propositions can only eliminate to Prop (having them eliminate to Type would be inconsistent with proof irrelevance). There is a rule called singleton elimination, which allows certain propositions which are "subsingletons" to eliminate to all types (I believe that an inductive type is a subsingleton if it has at most one constructor, and all arguments of that constructor are Prop-valued, but don't quote me on that). 

In the Lean 3 HoTT library Gabriel Ebner has written a program that checks whenever you proof a theorem/definition in the HoTT library that singleton elimination is not used. If it is used, then it raises an error (even though the Lean kernel did accept the proof).

We're quite certain that removing singleton elimination makes the kernel consistent with univalence. In fact, I believe that even when assuming `false` (which is the empty type living in Prop) we cannot construct any data in a type from it. This allows us to write metaprograms, like tactics and automation in Lean using Prop, while not using Prop in the HoTT-library.

I think Lean 3 is an interesting proof assistant to work on HoTT-specific automation, since Lean has a very strong metaprogramming language to write tactics in the Lean language itself. It is probably not the long-term "best" proof assistant, since its underlying type theory is not cubical (its underlying type theory is basically the type theory of the HoTT book). Work is in progress to port the formalizations from Lean 2 to Lean 3.

For more information see the readme of the linked Github repository. Any comments are welcome.

Best,

Floris

On 17 December 2017 at 23:43, Floris van Doorn <fpvd...@gmail.com> wrote:

Just to clear some things up in this conversation:

- The Lean kernel is consistent with any form of propositional extensionality, as far as I know.

- The kernel for the current version of Lean, Lean 3, is not designed for HoTT and inconsistent with univalence. However, it does *not* ignore any transport of an equality. The bottom universe in Lean is the universe of propositions, Prop (not to be confused with hProp). What does hold is that there is definitional proof irrelevance for proofs of a proposition, i.e. if P : Prop and p, q : P then p is definitionally equal to q. This means that if we have a proof p : A = A for some type A, then transporting along p is the identity function (because p = refl, definitionally). However, if p : A = B, then transporting along p is not the identity function (which would be type incorrect to state).

- Lean has an evaluator in a virtual machine, which is used to evaluate programs and tactics efficiently outside the kernel. This evaluator is not trusted, and cannot be used when writing any proof in Lean. This evaluator removes all type information and propositions for efficiency, and can evaluate expressions to the wrong answer when axioms are added to the type theory (even if the axioms are consistent). For example, if we add the following lines to Ben's example

```

constant H : HProp_ext

#eval Sig.fst (x H)

```

we see that the evaluator incorrectly evaluates this expression to tt (true). Needless to say, the evaluator was not designed for this, but instead to evaluate tactics like the following quickly.

```

if n < 1000000 then apply tactic1 else apply tactic2

```

I hope this clears up any confusion.

Best,

Floris

[Michael Shulman]

This is very cool! I look forward to hearing more about it.

Some 5 years ago when were trying to be sure that Coq would be
consistent with univalence, we also worried about singleton
elimination, but in that case I think the problem was not definitional
proof irrelevance (which Coq doesn't have) but the fact that Coq used
to implicitly put some inductive definitions, including in particular
the identity type, in Prop even when you didn't tell it to. I don't
remember that we actually derived a contradiction from this, but the
idea of all identity types of all types (in all universes) living in
the bottom universe certainly seemed unlikely to be consistent. We
fixed that with the --indices-matter flag which told Coq to put all
inductive definitions in the correct universe. It sounds like Lean
probably doesn't have this problem, i.e. if you define an inductive
*type* then it is always a type and never turns out to be a
proposition?

> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Floris van Doorn]

On 18 December 2017 at 08:04, Michael Shulman <shu...@sandiego.edu> wrote:

It sounds like Lean
probably doesn't have this problem, i.e. if you define an inductive
*type* then it is always a type and never turns out to be a
proposition?

Exactly. If you ask an inductive type to be in Type, it will never end up in Prop. If you want an inductive type to be in Prop, then you have to tell that explicitly. You can do that for any inductive declaration, but in the cases where singleton elimination doesn't hold, the generated induction principle will only eliminate to the universe Prop.