The Coq mailing list

[Christian Doczkal <christian.doczkal AT inria.fr>]

For me, this is about the ability to abstract and the freedom of how to
represent concepts.

For instance, it is not easy to define a type of deterministic finite
automata in Isabelle/HOL in a natural way (i.e., explicit
well-formedness conditions). In Coq, where one has Sigma-types (or
dependent records) one can do:

Record dfa : Type := {
    dfa_state :> finType;
    dfa_start : dfa_state;
    dfa_fin   : {set dfa_state};
    dfa_trans : dfa_state -> char -> dfa_state
}.

This definition is taken from our regular languages journal paper [1]
(https://hal.archives-ouvertes.fr/hal-01832031/document,
https://coq-community.github.io/reglang/)

Paulson [2] uses predicates on hereditarily finite sets instead of
finite types and then needs well-formedness conditions (e.g., that the
transition relation remains with the state space).

We discuss this in [1,Section 14].

Of course, this is just one of many examples where one wants to pair a
type with some operations and then reason about the concept as a whole.

Best,
Christian


1. https://hal.archives-ouvertes.fr/hal-01832031/

2. Paulson, L.C.: A formalisation of finite automata using hereditarily
finite sets. In: Felty, A.P., Middel-dorp, A. (eds.) Automated Deduction
(CADE-25). LNCS, vol. 9195, pp. 231–245. Springer (2015)


On 3/3/20 8:43 PM, 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.
> 
> Thanks,
> Jason