Compatibility of impredicative Set and function extensionality
Compatibility of impredicative Set and function extensionality
coq
Differences between Coq and Agda
Coq has been designed with theorem proving in mind, whereas Agda has been designed with dependently-typed programming in mind. They are somewhat equivalent on the theoretical side (even though they have differences, Coq being slightly more conservative in its axioms and sticking closer to the mathematical foundation of CIC by default), but I would trust … Read more
Difference between type parameters and indices?
When you see a family of types, you may wonder whether each of the arguments it has are parameters or indices. Parameters are merely indicative that the type is somewhat generic, and behaves parametrically with regards to the argument supplied. What this means for instance, is that the type List T will have the same … Read more
Why is my definition not allowed because of strict positivity?
Unfortunately, there’s nothing super deep about this example. As you noted Agda accepts it, and what trips Coq is the lack of uniformity in the parameters. For example, it accepts this: Inductive SwitchNSPA (A : Type) : Type := | switchNSPA : SwitchNSPA A -> SwitchNSPA A. Inductive UseSwitchNSPA := | useSwitchNSPA : SwitchNSPA UseSwitchNSPA … Read more
What are the strengths and weaknesses of the Isabelle proof assistant compared to Coq?
I am mostly familiar with Coq, and do not have much experience with Isabelle/HOL, but I might be able to help a little bit. Perhaps others with more experience on Isabelle/HOL can help improve this. There are two big points of divergence between the two systems: the underlying theories and the style of interaction. I’ll … Read more