The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

Very helpful. Thanks for this. --Kevin

On Mon, Feb 19, 2018 at 9:54 AM, Gert Smolka <smolka AT ps.uni-saarland.de> wrote:

We cover intuitionistic / classical ND in an introductory class using Coq,

see lecture notes and Coq files at https://courses.ps.uni-saarland.de/icl_17/2/Resources.

This includes Glivenko’s theorem.

There is also a Coq development of Gentzen’s intuitionistic sequent calculus

showing that it is decidable and intereducible with intuitionistic ND, see

http://www.ps.uni-saarland.de/courses/cl-ss16/LectureNotes/html/toc.html.

Gert

On 19. Feb 2018, at 15:16, Kevin Sullivan <sullivan.kevinj AT gmail.com> wrote:

​ I'm looking for a simplest way to teach my early undergraduate students about natural deduction and/or sequent calculus proof objects without having to get into lambda terms and type systems.

The following "POPL tutorial" suggests a standard solution:  formalize proofs  as values of an inductive type, where the constructors mirror the rules of inference.

http://twelf.org/wiki/POPL_Tutorial/Sequent_vs_Natural_Deduction#Syntax_for_Propositions​

The rule for implication introduction says (naturally enough) that if you have a function from proofs of A to proofs of B, you can construct a proof of (Impl A B).

A straightforward translation of this into Coq, as copied right below this sentence, results in a non-positivity error for the encoding of this inference rule.

/* variables */

Inductive var := mk_var: nat -> var.

/* propositions in my minimal propositional logic */

Inductive prop :=

   | atom: var -> prop

   | and: prop -> prop -> prop

   | impl: prop -> prop -> prop.

/* proof rules */

Inductive proof: prop -> Type  :=

  | axiom: forall A: prop, proof A

  | andIntro: forall A B: prop, proof A -> proof B -> proof (and A B)

  | andElimL: forall A B: prop, proof (and A B) -> proof A

  | andElimR: forall A B: prop, proof (and A B) -> proof B

  | implElim: forall A B: prop, proof A -> proof (impl A B) -> proof B

  | implIntro: forall A B: prop, (proof A -> proof B) -> proof (impl A B). (* oops!!! *)

What would be the canonical way to represent the same ideas in Coq in a way that works?

Again, the aim is a super-straightforward pedagogical explication of rules of natural deduction (or sequent calculus), for a propositional logic only, with the ability to "play around" by building proof terms by explicit application of introduction and elimination inference rules. 

Kevin