Questions on proof assistants

[Lawrence Paulson]

> On 15 May 2020, at 11:54, Freek Wiedijk <freek at cs.ru.nl> wrote:
> 
> - Lean
> 
> It's a Coq clone by Microsoft, but the Lean
> community has many hardcore former Isabelle users in it
> (Jeremy Avigad, Jasmin Blanchette, etc.)  So it might be
> developing into the best of both worlds.  Also, it removed
> some of the subtleties of Coq that get in the way if you're
> not into constructive/computable mathematics and/or Homotopy
> Type Theory.  For instance, it has functional extensionality:
> if f(x) = g(x) for all x then f = g; in Coq you need an axiom
> for that (and also Thorsten might get angry at you :-)),
> it has proof irrelevance, it has quotient types, it has a
> much simpler definition of the foundations of the system
> (the "logic"), etc.

It is important that we understand which peculiarities of Coq are inherent in the use of dependent types and which are purely incidental. Intensional equality is terrible: it implies that n+0=n and 0+n=n (for n a natural number) are fundamentally different assertions because one holds by definition and the other was proved by induction. Arbitrary details of a definition remain important forever.

The Ssreflect layer strikes me as being intended to provide an extremely simple subformalism type theory in which all assertions are computable, thereby yielding the excluded middle even in the intuitionistic context. And that is why the carriers of groups in the odd order theorem development are lists of booleans expressing the characteristic function of the corresponding finite set. It's ingenious but horrifying at the same time: why can’t you just have some notion of set, including infinite sets? Occasionally “setoids” are mentioned, always with hints of unpleasantness.

So does Lean deal with these issues and give us a natural language of sets, even if they are typed sets? Another question: I seem to keep hearing that type checking in Coq can be computationally intensive to the extent that performance becomes a real issue. Is that again incidental to Coq or inherent to the choice of dependent types? 

And to what extent is the preference for constructive reasoning inherent to type theory as opposed to being a cultural choice of the Coq community? In the case of real analysis, the implications of intuitionism become too big to ignore.

Larry