The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,

you can also have a look at our development about logic and semantics,
in particular the file:

file:///home/courtieu/work/loglangcoq/coq_src/html/loglangcoq.logique.deduction_naturelle.html

It is a straightforward definition of natural deduction (propositional
fragment) with the simplest possible definition of formulas and there
semantics. A few tactics allow to easily apply the rules. We use utf8
notation to stay as close as possible to usual notations. proof
environments are multisets of formulas and thanks to setoid rewrite
this is not too painful.

There is a proof of correctness and completeness of the logic too at the end.

Sorry comments and constant names are in french (this was for french
students) but it should be easy to read anyway. I can try to translate
things if asked for.

It compiles with coq 7.1.

table of contents of the whole dev is there:
http://cedric.cnam.fr/~courtiep/downloads/loglangcoq/toc.html

Hope this helps
Pierre



2018-02-19 17:50 GMT+01:00 Daniel Schepler 
<dschepler AT gmail.com>:
> On Mon, Feb 19, 2018 at 6:16 AM, 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.
>
> I have a development of both under
> https://github.com/dschepler/coq-sequent-calculus .  It's not
> extremely well commented, though, so I'm not sure how useful it would
> be for beginners.
>
>> 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
>
> Well, my development actually made an inductive proposition of
> provability - but it would hopefully be simple enough to change that
> to a type of proof objects if needed.
>
>> 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).
>
> I think that might be mixing up the formal structure of an implication
> proof on the one hand, and the interpretation of such a proof as a
> function on the other.  In particular, my ND_proves proposition is a
> function "list (prop atom) -> prop atom -> Prop" of both a context and
> a goal, with the context being a crucial ingredient because in natural
> deduction proofs, the context to the left of the turnstyle varies
> through the different parts of the proof tree.  In particular, the
> form of an implication proof is:
>
> | ND_cond_proof {Γ P Q} :
>   P :: Γ ⊢ Q ->
>   Γ ⊢ P ⊃ Q
>
> And then I didn't develop this explicitly, though I did develop an
> interpretation in terms of Heyting algebras which could be adapted.
> But the interpretation of a proof object in Γ ⊢ P as a function in the
> sense of Curry-Howard would look something like an element of
> (fold_left (fun (Q : prop) (X : Type) => prop_interp Q -> X) Γ
> (prop_interp P)) where
> Variable type_assign : atom -> Type.
> Fixpoint prop_interp (P : prop atom) : Type :=
> match P with
> | atom_prop x => type_assign x
> | bot_prop => Empty_set
> | top_prop => unit
> | and_prop Q R => prop_interp Q * prop_interp R
> | or_prop Q R => prop_interp Q + prop_interp R
> | impl_prop Q R => prop_interp Q -> prop_interp R  (* <- this term is
> probably what you were thinking of *)
> end.
>
> In this formulation, the interpretation types of both sides of
> ND_cond_proof end up being pretty much the same, so the corresponding
> map of interpretation types would just be essentially the identity
> map.
>
>> 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.
>
> I think the definition of ND_proves (or classic_ND_proves in
> ClassicalND.v) should be straightforward enough to read.  And it would
> be easy to play around with constructing proofs using the proof rules
> - I don't remember having too many examples of intuitionistic natural
> deduction, except as steps in equivalence proofs with my formulations
> of sequent calculus and with a Hilbert-style proof system.  But in
> ClassicalND.v, I do have example proofs of excluded middle and
> Peirce's law based on the classical proof rule of "proof by
> contradiction".  For this part, what I wrote above about Curry-Howard
> style interpretations of proof objects as functions wouldn't be needed
> at all.
>
> Though be warned I did make a few choices which are apparently
> nonstandard.  For example, my formulation includes an explicit cut
> rule even though it could easily be deduced from a combination of the
> "conditional proof" and "modus ponens" rules.  (This was because my
> intended interpretation of this proof rule was more like "let x :=
> interp phi in interp psi" rather than "(fun x => interp psi) (interp
> phi)".)  On the other hand, the version of sequent calculus I
> presented is a cut-free version since my goal there was to formalize a
> proof of the cut elimination theorem.
>
> (Also, I developed that in Coq 8.5, I think, so I can't promise all
> the proofs would still work in the latest Coq version.)
> --
> Daniel Schepler