xnning/software_foundation_exercises

Exercises of book Software Foundation

Exercise Solutions

Basic

Book: Software Foundation Version: 3.2

Coq Version: 8.5pl1

Compatibility

• Poly.v: Set Asymmetric Patterns. is needed to use nil directly in patterns.
• Prop.v: Prop is no longer an available name in Coq 8.5. Rename it.
• Imp.v: Require Coq.omega.Omega. Ltac omega := Coq.omega.Omega.omega. is requested in Coq 8.5 to directly use omega.
• Auto.v: info_auto does not print trace anymore and use Info 1 auto instead. But it seems to keep giving unknown...

Progress

Following blue arrows, which is recommended path for one-semester course.

• Basics
• Induction: Proof by Induction
• Lists: Working with Structured Data
• Poly: Polymorphism and Higher-Order Functions
• MoreCoq: More About Coq's Tactics
• Logic: Logic in Coq
• Prop: Propositions and Evidence
• MoreLogic: More on Logic in Coq
• SfLib: Software Foundations Library
• Imp: Simple Imperative Programs
  • Additional Exercises
• Equiv: Program Equivalence
  • Additional Exercises
• Hoare: Hoare Logic, Part I
• Hoare2: Hoare Logic, Part II
• Smallstep: Small-step Operational Semantics
  • A Small-Step Stack Machine
• Auto: More Automation
• Types: Type Systems
  • Additional Exercises
• Stlc: The Simply Typed Lambda-Calculus
• StlcProp: Properties of STLC
  • Additional Exercises