The Coq mailing list

[mechvel AT scico.botik.ru]

On 2020-03-03 22:43, Jason Gross wrote:
> I'm in the process of writing my thesis on proof assistant performance
> bottlenecks (with a focus on Coq), and there's a large class of
> performance bottlenecks that come from (mis)using the power of
> dependent types.  So in writing the introduction, I want to provide
> some justification for the design decision of using dependent types,
> rather than, say, set theory or classical logic (as in, e.g.,
> Isabelle/HOL).  And the only reasons I can come up with are "it's fun"
> and "lots of people do it"
>
> So I'm asking these mailing lists: why do we base proof assistants on
> dependent type theory?  What are the trade-offs involved?
> I'm interested both in explanations and arguments given on list, as
> well as in references to papers that discuss these sorts of choices.


For example, mathematicians write:
"In any field F there is an inversion operation for a nonzero elements:
inv : F\{0} -> F
".
With dependent types, the type of inv is expressed as

      (x : F) -> x /= 0# -> F

This type depends on the value x, and this value can change during some 
computation.
And I do not know how to express as a type this mathematical notion.
There are many such examples.

Also dependent types are good for constructive proofs.
For example, consider a theorem
"For any prime number p there exists a prime q greater than p".
With dependent types, we prove a stronger statement:
"This provided below algorithm A takes any prime number p and returns a 
prime q greater than p".
If one cannot invent a constructive proof, but can prove the thing in a 
classical logic,
then one can add the postulate of excluded third and write a classical 
proof in Agda.

Regards,

------
Sergei