Assignment 3: Coq

Due: Fri, 24 Feb 2017 23:59:00 -0500

The goals of this assignment are to practice using Coq and gain some experience with an interactive theorem prover.

Setup

Download and install Coq, and optionally an IDE.
For example, on Mac OS X, you can run:

brew install coq
brew install Caskroom/cask/coqide

This will install Coq and the basic Coq IDE. Proof General is another popular IDE choice. See the preface of Software Foundations for more details about them.

Background

Please read the following sections of Software Foundations:

• Preface
• Basics
• Induction: Proof by Induction
• Lists: Working with Structured Data
• Tactics: More Basic Tactics
• Logic: Logic in Coq
• Imp: Simple Imperative Programs
• Extraction: Extracting ML from Coq

Download the source files and complete all 1 and 2 star exercises in the corresponding .v files, with the following exceptions and additions:

• Induction: Skip plus_comm_informal and beq_nat_refl_informal, but add mult-comm.
• Lists: Add alternate, list_exercises.
• Tactics: More Basic Tactics: Skip apply_rewrite. Add apply_exercise1 and beq_nat_sym.
• Logic: Logic in Coq: Add evenb_double_conv, excluded_middle_irrefutable.
• Imp: Simple Imperative Programs: Add optimize_0plus_b, loop_never_stops.

When you’re done, there should be no Admitted calls left for these exercises. You are, of course, welcome to do more of the exercises, which will give you additional practice with the prover.

Submissions and Grading

Please submit a single zip file coq-AndrewID.zip via Blackboard (where AndrewID is obviously replaced with your actual ID). The zip file should be arranged such that it contains:

• One .v file for each chapter above, edited to complete the assigned exercises.
  In other words, you should include:
  • Basics.v
  • Induction.v
  • Lists.v
  • Tactics.v
  • Logic.v
  • Imp.v