coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fwd: "Lean is like Coq but better"

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Fwd: "Lean is like Coq but better"
Date: Wed, 8 Jan 2020 00:15:47 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qv1-f48.google.com
Ironport-phdr: 9a23:+U18uBcdnfz+472OxXBdrGaGlGMj4u6mDksu8pMizoh2WeGdxcS6Yx7h7PlgxGXEQZ/co6odzbaP6Oa6BDNLvsfJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRu7oR/PusQWg4ZuJaQ8xx/UqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU09nzchM5tg6JBuB+vqRxxzZDJbo+WNvV+cKTTctwGSmRORctRSy5MD5mgY4YVE+YNI+BVpJT9qVsUqhu+ABGhCO3tyj9PgH/23K463PolEQ7YwgMtBN0OsHHOo9X0MKceS/y6zK7NzTnNcvhb3jX96I/OchAgovGDQ7ZwftTPxkQ0GAPFi0+fqY3hPz+PyusNtG2b4vNmWOmyiGAnsxl8riazysookIXEhYIYxkra+SlkxIs5P9K1RU1jbdK6EZZcqzyWOo5rTs4mX25lvSk3x7watZKneSUG1ZcqyhzaZvOaboeF4BzuWeOTLDp5nn1oereyiAyy/EWiyuDxU8q53EtQoSdHlNTHq2oD2AbJ6sedT/tw5keh1iiL1wDU8uxEJFo7lavfK5I4274wiIcfvV3NHiL5m0j6lqCWdkIj+uin7+TofK/qqYObN49xkg3+M6IuldKjAekgLAQCQ2yW9f6/2bDj50H1XqhGg/ksnqTWs53WPcEbqbS4Aw9R3IYj8RG/DzK+3dQamnkHKlNFeBGZgIjtJV7BPuv1Dfi6g1u2kTdrw+rKMaHmApXINnTDiqvufa5h605Azwo+1cxQ55VNCr0YPP3zXlLxu8fDAx8iMw20xv7nB89n2oMfX2KPGK6ZP7nIvV+G/OJ8a9WLMYQSoXP2L+Uvz//ol34w31EHLoez2p5CInK/GPVlLkGUbFLjh94AFSEBuQ90BLjoj1uDUjNXanuaUKc15zV9A4WjW9SQDruxiaCMiX/oVqZdYXpLXwjVTCXYMr6cUvJJUxq8Z89sljteCOqkQo4lkAiw7Ur0l+ohIe3T9SkV85nk0YotvryBpVQJ7TVxSv+l/SSIRmBwkHkPQmZvjq96qE15jFyE1Poh2qAKJZlo//pMFzwCG9vE1eUjUoL9XwvAepGCT1P0Gtg=

On Tue, 7 Jan 2020 23:11:54 -0500
Jason Gross
<jasongross9 AT gmail.com>
wrote:

> The standard computational uses of Prop are Acc (the inductive type of
> well-founded accessibility proofs, needed for running well-founded
> recursion) and eq (which, unlike Acc, one might claim should be
> erased in classical / anti-univalent settings). Note that Coq is in
> the process of getting an erasible eq type that can be used in casts,
> but last I checked, allowing casts across this equality results in
> non-termination of reduction. (I can dig up the relevant pull
> request discussion if anyone wants me to.)

I didn't use Prop for computation, I used it to carry around
computation - keeping some throw-away computation separate (and
erasable) from the actual program. This is certainly not what Prop was
designed to do, but it did it anyway. It would not be able to if it
was tied down with LEM, I believe.

Re: [Coq-Club] Fwd: "Lean is like Coq but better", (continued)