The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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

On Tue, Jan 7, 2020, 22:16 jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

I have to mull over Mario's response, but I think there are usages of
Coq's Prop that require it to be constructive (non-LEM).  My own work
relies on this - it also rests on the fact that Prop will be erased,
leaving Type as the program, but uses Prop to carry around simple
computation as well as propositions in order to prove more complex
computation in Type.  I'd be curious if the same technique is possible
in Lean.

On Tue, 7 Jan 2020 21:20:33 -0500
Mario Carneiro <di.gama AT gmail.com> wrote:

> On Tue, Jan 7, 2020 at 8:51 PM jonikelee AT gmail.com
> <jonikelee AT gmail.com> wrote:
>
> > [decloaking from lurker mode to add my $0.02]
> >
> > Does having LEM built into Lean interfere with the user's ability to
> > exploit the Curry-Howard isomorphism?
> >
> > If so, that seems like a bad trade off: a small convenience for a
> > small group of people (Fields Medal wanabees) that imposes a large
> > inconvenience for a large group of people (software engineers).
> > 
>
> I haven't found that Lean's ontology poses any serious issues for
> writing software, and if anything I think it helps. Lean makes a
> sharp distinction between data (in Type) and proofs (in Prop), and
> proofs are erased during code execution. So if you build a sorting
> function of type forall l : list A, { l2 : list A | l2 is a sorted
> permutation of l }, then the "list A" part is data, which can be
> executed assuming it doesn't use the axiom of choice in its
> definition, and the "l2 is a sorted permutation of l" part is a
> proof, so it completely disappears during execution. You can use
> choice if you want to prove this fact, as it is just a conventional
> mathematical assertion; it will not interfere with the computability
> of the overall function.
>
> So it's a half-baked kind of constructivism, that is constructive
> only in the places where it actually matters to producing code. That
> seems like a reasonable compromise to me. In particular, LEM is not
> executable in any case, because it is a Prop; you can't case analyze
> on it unless you are proving another Prop and this too will be
> erased. Whenever you use "if" in Lean it infers decidability of the
> predicate in question, and this proof of decidability lives in Type
> and can be executed.