Discrete 2021: Proof Assistants

Coq

Simple Tautologies

intros x. (For variables)
intros H. (For implications)
unfold not. (Replace "~")
unfold iff. (Replace "<->")
assert (...) as H1.
destruct H1 as [H2 H3].
destruct H1 as [H2 | H3].
exact H.
apply H.

Sample Proofs: Examples from Ch1_4 (Knepley2021, p.13-25)

Non-Constructive Tautologies

Require Import Classical_Prop.
pose (classic (...)) as H.
elim classic.
apply NNPP.
contradiction.

Sample Proofs: Two Non-Constructive Proofs
20 Tautology Samples

Predicates on Finite Sets

Section someName.
Inductive typeName : Type :=
Variable predicateName : typeName -> Prop.
Hypothesis ...
induction varName
reflexivity
discriminate
exists varName

Sample Proofs: Examples from Ch2_3 (Knepley2021, p.43-49)

General Predicate Calculus

Sample Proofs: Examples from Ch2_2 (Knepley2021, p.38-43)
Examples from Ch3_2 (Knepley2021, p.60-68)
Examples from Ch3_3 (Knepley2021, p.69-81)

Integer Divisibility

Open Scope Z_scope.
Close Scope Z_scope.
ring.
rewrite H1 in H2.
rewrite <- H1 in H2.
unfold Z.divide

Sample Proofs: Examples from Rosen2019, Ch1.7

GCD and Induction

Open Scope nat_scope.
Close Scope nat_scope.
destruct n.
induction n.
lia.
omega.
Fixpoint ...

Sample Proofs: Some theorems about GCD
Examples from Rosen2019, Ch1.7
Examples from Ch4_4 (Knepley2021, p.91-105)
Examples from Ch4_5 (Knepley2021, p.106-129)
Some Advanced Induction Examples

Discrete 2020 Coq Samples and Tasks

Old Coq Labs

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"

Classical vs. Intuitionistic Logic

Inductive Proofs and Integers

Competition Problems with Coq

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