The Coq mailing list

[Julian Michael <julianjohnmichael AT gmail.com>]

 

I think having more code critique on coq-club is something that everyone would benefit from. (Did you use bullets?)

I would encourage you to start a new thread focused on the critique of your development.

Good idea, thanks! I will do that soon—also, I actually didn't know about bullets... I was using the Case/SCase/etc. constructions that were included in Software Foundations. So thanks for that too!

 

On Sun, Nov 29, 2015 at 9:27 AM, Julian Michael <julianjohnmichael AT gmail.com> wrote:

 

I've recently played around with some development along those lines - defining
a natural deduction style proof system in Coq, and proving that it results in
a free Heyting algebra.  I haven't defined a decision procedure for it, much
less proved the completeness - which essentially reduces to cut elimination,
or perhaps as another way of putting it the possibility of reducing a lambda
_expression_ representation of a proof to a normal form.  Unfortunately, it's on
another machine I wouldn't be able to access until Monday, if you'd be
interested in seeing what I have so far.

I assumed the original question was about classical propositional logic. On a related note, I only recently started learning Coq and as an exercise I spent a bit of time trying to formalize the soundness and completeness of a natural-deduction style system with respect to 2-valued truth assignments, in the style of the proof by Kalmar (1935). Never quite finished, but it's mostly there if anyone's interested in taking a look. (It'd be valuable to me to have someone critique my code.) If such a proof is already around somewhere, though, let me know.