4 ms·
Could someone with knowledge of both COQ and LEAN provide more info/comparison? Are they based on the same foundation or are there differences? Might it be poss
by ivan_ah 7y ago
Could someone with knowledge of both COQ and LEAN provide more info/comparison? Are they based on the same foundation or are there differences? Might it be possible to automatically convert proofs between the two? What about "strategies" ?
I was able to find a basic example of the natural numbers and the operation `plus` in both languages, and it seems like the structure is quite similar.
Coq:
Inductive nat : Type :=
| O : nat
| S : nat → nat. (* S stands for successor *)
Fixpoint plus (n : nat) (m : nat) : nat :=
match n with
| O ⇒ m
| S n' ⇒ S (plus n' m)
end.
via https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html#lab30 https://softwarefoundations.cis.upenn.edu/lf-current/Basics....
Lean:
inductive nat : Type
| zero : nat
| succ : nat → nat
def plus : nat → nat → nat
| m nat.zero := m
| m (nat.succ n) := nat.succ (plus m n)
via https://leanprover.github.io/introduction_to_lean/ https://leanprover.github.io/introduction_to_lean/
- krapht 7y agoThere are subtle differences. What ostensibly they are both based on the calculus of inductive constructions, there are incompatible extensions to the logic in the kernel. The majority is convertible, though. If I had to make a programming analogy, it would be like converting between C++ and D, or different Lisp dialects. The difference is bigger than Python 3 vs Python 2, but less than F# vs OCaml. Clearly possible, in a sense, and if you can read one language, you can read the other, but automatic conversion is just out of reach due to edge cases.