HoTT in Lean 3

HoTT in Lean 3

[Floris van Doorn]

[-- Attachment #1: Type: text/plain, Size: 3946 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 4633 bytes --]

Re: [HoTT] HoTT in Lean 3

[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?

On Sun, Dec 17, 2017 at 3:13 PM, Floris van Doorn <fpvd...@gmail.com> wrote:
> 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
>>
> --
> 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.

Re: [HoTT] HoTT in Lean 3

[Floris van Doorn]

[-- Attachment #1: Type: text/plain, Size: 609 bytes --]

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.

[-- Attachment #2: Type: text/html, Size: 944 bytes --]