The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

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.