Logic Project

The project description is available here. It comes with some code, available in a git repository, which might be updated e.g. with more SAT instances for testing. The project is due (as one tarball) by Wednesday, May 27th (midnight).

Resources

• A guide to basic tactics.

Tutorials

The following Coq files will gradually introduce what you need to know about the system.

As an exercise, you must complete unfinished proofs in all of these files: watch for the Admitted parts. Since the goal is to understand the presented elementary aspects of Coq, please refrain from using advanced stuff e.g. found on the web.

1. • Propositional (Coq, HTML)
   • First-order (Coq, HTML)
   • Natural numbers (Coq, HTML)
2. • Extraction (Coq, HTML) updated on Feb 6 (fix in explanation of fack')
   • Decidability (Coq, HTML)
   • More on (co)inductives (Coq, HTML) updated on Feb 13 (fix bonuses)

Project

The task is to write certified programs dealing with LL(1) grammars — a notion that will be covered in depth in the Formal Languages course. It is described in the following files:

• Grammar (Coq, HTML): definition of grammars, derivations, and some LL(1) specific concepts
• Grammar_ex (Coq, HTML): examples to test your understanding of definitions
• Nullable (Coq, HTML): certified computation of nullable set
• LL (Coq, HTML): certified LL(1) parsing

Except for grammar.v which is loaded from the other files, and thus cannot contain any assumption, all files contain assumptions: it is your job to prove them.

The two major tasks, nullable.v and ll.v, are independent.

In order to complete these developments you will have to come up with useful lemmas, and prove them. I do not expect you to fully complete your development: you can leave some lemmas unproved (perhaps as axioms). However, for each such assumption, you MUST provide a comment explaining why you believe that the lemma or axiom holds.

You should send me your solutions (the four files, completed) strictly before Monday, April 6th by email. If this leaves you some spare time, you can try to complete (more) bonuses from the tutorials, or improve your project in some of the following directions:

• Get rid of fuel in the computation of first, i.e. show that for every grammar g there exists k such that nullable_sym g s k iff Nullable g (s::nil).
• Independently of the previous item, improve the fixed point computation of nullable by stopping when nullable_step returns an equal set in nullables.
• Get rid of fuel for the parser. Here, some extra assumptions would be reasonable, but you need to explain them carefully.