Comment by c-cube
2 years ago
If you want something as simple as possible, look at HOL and similar simple logics! CIC is powerful but it's also quite complex in comparison. Proof assistants based on HOL are plenty and they're definitely usable (see Isabelle/HOL, HOL light, etc.)
I did study HOL Light. Although it is very simple, I found parts of it to be a bit ugly. It treats the left of the turnstyle (|-) as a kind of set where you sometimes have to remove all alpha-equivalent terms. I.e., the DEDUCT_ANTISYM_RULE in https://en.wikipedia.org/wiki/HOL_Light. Another thing that I found ugly in HOL Light is that if one looks at the very basic code that is the kernel of the system all variables carry their type around with them. I think the lambda calculus where (\x: T, body) just has the type of x in the lambda and not in every instance of x inside body is just nicer.
I agree that the treatment of alpha equivalence might not be the best. Isabelle/HOL has pattern unification which makes it easier.
For the type variables: it's a matter of taste! I prefer it this way, and it's quite useful if you expect terms and theorems to have free variables (quite common in automatic provers). Having free variables is a good way to specify things like rewrite rules, backward chaining clauses, etc. so it doesn't come out of the blue.