From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.95.200 with SMTP id t191mr9324717vkb.124.1513552445453; Sun, 17 Dec 2017 15:14:05 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.159.43.69 with SMTP id q5ls3928728uaj.17.gmail; Sun, 17 Dec 2017 15:14:04 -0800 (PST) X-Received: by 10.31.211.131 with SMTP id k125mr3613583vkg.113.1513552444186; Sun, 17 Dec 2017 15:14:04 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513552444; cv=none; d=google.com; s=arc-20160816; b=GRemZ8WkyYNFW+rDK9lWTivwHSGlKqb3M+V/PTeeK1s6AdSKusFaVifqyQVUvPPNY9 UR7OXrTHuMtTfR2QZYenFtt4rwjmnNSg/+VpfVLJnosHg8QSxGgbIOElRQCDUBBTSi8i pYG6h7n17ZLJJPE8vqkEmPVG8bw08CDSFoqGsiIdcqJDMMH22tWBAXQ3dxjVDYNwZtJW yacyQhavvfqFtYwFR6LaUocePTm1ccb43kFn7Q2I4ZQoBwbQvUc7RRuSWMBqRSN1eWX9 T+PNcu1Dj8CiVfveq3DuMNM2f3xZSugYQXG4NLUXnwMdCDwNVHkyGF6J87NDLIyS8dLJ MMLw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:mime-version:dkim-signature :arc-authentication-results; bh=BA1A3gG9b0E7KQ8oag9ez8a5gST3puqo4wVZ/RHcrQ8=; b=FxniybVjZSq2k7v9ZZe7BkuRy4Wre8GmWeWYIBcjRmtTbLLm/Qo3ZlBiKVIS16JbHh ctQ9K3yd2BUAxYVFJ1HCluns/UTzq6x/dGx8Cgphmv665j9tyCGrUOfSxuPpGRHtcpGO NmCEM1LtMhASsEK4OHHKDQL1jp1scORLBdDM4PnczCWeY81VRw5KH1nhCkvJXvJo3B42 X6KXMcQWsijpd0Bi29ygEJQLJKx6RZOVRkkeXJIEqXKb4i1q2kF8RcU8B+KbWjWPkGOj 7bylU8eWasz4nQ5HXRxPj79mw/P4+NsStZ6NKR8njBESirWx+RJbnQTIfVA1pqmwc+Wb MUVw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=HrPBo/yb; spf=pass (google.com: domain of fpvd...@gmail.com designates 2607:f8b0:4001:c06::229 as permitted sender) smtp.mailfrom=fpvd...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-io0-x229.google.com (mail-io0-x229.google.com. [2607:f8b0:4001:c06::229]) by gmr-mx.google.com with ESMTPS id a25si85824uak.4.2017.12.17.15.14.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 17 Dec 2017 15:14:04 -0800 (PST) Received-SPF: pass (google.com: domain of fpvd...@gmail.com designates 2607:f8b0:4001:c06::229 as permitted sender) client-ip=2607:f8b0:4001:c06::229; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=HrPBo/yb; spf=pass (google.com: domain of fpvd...@gmail.com designates 2607:f8b0:4001:c06::229 as permitted sender) smtp.mailfrom=fpvd...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-io0-x229.google.com with SMTP id f18so2873117ioh.1 for ; Sun, 17 Dec 2017 15:14:04 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to:cc; bh=BA1A3gG9b0E7KQ8oag9ez8a5gST3puqo4wVZ/RHcrQ8=; b=HrPBo/ybJdzuvCiiIhJZxODXMYcZpl3QrwFfIKEtoZSTI+8spl4+XNS+FMsJktTzxw 3ea35AfednevKjZPWWDpKqI5XWZeKvMSvUm4xzILFnaT5a/fe2b22YqdwsTxWnRQ+BTU 7KQu4W5K+OoIaDAixJfwuskswCooeJzi3gpTMpFpgMFCtoiakvyBVP849DDqKJlBUups 5gmvhdZ6sDNCX9iFD9xBlfrlCBHMheB9zZTXSZQz1vj2IObasjd8pJg5nB/q2kcRpNU3 PvT4eqF6D7ioiERCm83/BYZBSg+ZvgzzAx9xPSfynX7mVXQSt3rehy1o4XgDf5zYScMP 2HHA== X-Gm-Message-State: AKGB3mIjwSerl/1HchPh/N7O4vGv07YbVeMcBDQ4IIQK/K3jIkPOnHYu 5a3yNhL9dN/X/2F2zr8oujFK6g9gkoCwCETyrlnz6vjP X-Received: by 10.107.130.85 with SMTP id e82mr21733429iod.30.1513552443373; Sun, 17 Dec 2017 15:14:03 -0800 (PST) MIME-Version: 1.0 Received: by 10.2.155.50 with HTTP; Sun, 17 Dec 2017 15:13:42 -0800 (PST) From: Floris van Doorn Date: Mon, 18 Dec 2017 00:13:42 +0100 Message-ID: Subject: HoTT in Lean 3 To: Homotopy Type Theory Cc: Jeremy Avigad , Gabriel Ebner , Rob Lewis Content-Type: multipart/alternative; boundary="001a113eb794bc957c0560916309" --001a113eb794bc957c0560916309 Content-Type: text/plain; charset="UTF-8" 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 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 > > --001a113eb794bc957c0560916309 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
A followup to my previous email in another discussion= (copied below).

I said in that email that the ker= nel of Lean 3 is inconsistent with univalence. While this is true, we are c= urrently developing a HoTT library for Lean 3 here:
https://github.com/gebner/hott3
The logic in this library is consistent in the following sense descri= bed below.=C2=A0

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

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

We're quite cer= tain that removing singleton elimination makes the kernel consistent with u= nivalence. 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.

<= div>I think Lean 3 is an interesting proof assistant to work on HoTT-specif= ic automation, since Lean has a very strong metaprogramming language to wri= te tactics in the Lean language itself. It is probably not the long-term &q= uot;best" proof assistant, since its underlying type theory is not cub= ical (its underlying type theory is basically the type theory of the HoTT b= ook). 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=C2=A0<fpvd= ...@gmail.com>=C2=A0wrote:
Just to clear some things up in this co= nversation:

- The Lean kernel is consistent with any for= m of propositional extensionality, as far as I know.
- The kernel= for the current version of Lean, Lean 3, is not designed for HoTT and inco= nsistent with univalence. However, it does *not* ignore any transport of an= equality. The bottom universe in Lean is the universe of propositions, Pro= p (not to be confused with hProp). What does hold is that there is definiti= onal 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 pr= oof p : A =3D A for some type A, then transporting along p is the identity = function (because p =3D refl, definitionally). However, if p : A =3D B, the= n transporting along p is not the identity function (which would be type in= correct to state).
- Lean has an evaluator in a virtual machine, = which is used to evaluate programs and tactics efficiently outside the kern= el. This evaluator is not trusted, and cannot be used when writing any proo= f in Lean. This evaluator removes all type information and propositions for= efficiency, and can evaluate expressions to the wrong answer when axioms a= re added to the type theory (even if the axioms are consistent). For exampl= e, 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 expres= sion 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

--001a113eb794bc957c0560916309--