Old PBM763 (2020): Coq and Scala

Coq Labs

• Preparation for Coq LAB01: Problems
• Preparation for Coq LAB01: Solutions
• Coq LAB01: Problems
• Coq LAB01: Solutions
• Coq LAB02: Problems
• Coq LAB02: Solutions

Coq Examples and Tutorials

Official Tutorials:

• Coq in a Hurry
• Mike Nahas Tutorial: Propositional Logic Proofs
• Coq: Predicate Calculus
• Coq: The Full List of Proof Tactics
• Coq Standard Libraries in GitHub (proofs of some known facts that you can use)
• Software Foundations (4 large textbooks on Coq) - beware of some "pretty printed" symbols. They use "∀" instead of "forall", "⇒" instead of "=>"
• Tutorial on Coq Proofs (Yale CS428)
• Some other Coq links (Buffalo CSE191)

Tactics and Cheatsheets

• A Short Coq Tactics Cheatsheet and their Notes on Writing Proofs (Cornell CS3110)
• Coq tactics tutorial (U of Edinburgh)

Specific Examples for "Discrete Structures"

• Proving Tautologies (Buffalo CSE191, p.12-20)
• On classical proofs
• Example: Scottish Club
• Example: Lions and Coffee
• Example: Smullyan's Drinker Theorem
• Example: Everybody Loves My Baby

Classical vs. Intuitionistic Logic

• On classical proofs
• Elim a double negation hypothesis in Coq Proof Assistant? (Classical Logic)
• Axioms (on Classical Logic)
• Logic in Coq
• NNPP and similar proofs
• Five Stages of Accepting Constructive Mathematics

Inductive Proofs and Integers

• Predicates and Quantifiers (Buffalo CSE191, p.30-49)
• Inductively Defined Types (Buffalo CSE191, p.84-106)
• Integer Arithmetic (Buffalo CSE191, p.110-137)
• Number theory results (for Lab02, Problems 16-20)
• Nat modulo
• Recursive functions and proofs about them

Competition Problems with Coq

• LV.NO.2020.9.2;  LV.NO.2020.11.1;