Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Lecture

Coq: Overview

Description

This lecture introduces Coq, a proof assistant, focusing on the theorem and_comm, which states that for all propositions P and Q, if P and Q are true, then Q and P are also true. The lecture covers the process of proving this theorem step by step using Coq's proof assistant.

Official source

Related concepts (27)

Proof assistant

In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer. A recent effort within this field is making these tools use artificial intelligence to automate the formalization of ordinary mathematics.

Coq

Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics (procedures) and various decision procedures.

Mathematical proof

A mathematical proof is a deductive argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every proof can, in principle, be constructed using only certain basic or original assumptions known as axioms, along with the accepted rules of inference. Proofs are examples of exhaustive deductive reasoning which establish logical certainty, to be distinguished from empirical arguments or non-exhaustive inductive reasoning which establish "reasonable expectation".

Lean (proof assistant)

Lean is a theorem prover and programming language. It is based on the calculus of constructions with inductive types. The Lean project is an open-source project hosted on GitHub. It was launched by Leonardo de Moura at Microsoft Research in 2013. Lean has an interface, implemented as a Visual Studio Code extension and Language Server Protocol server, that differentiates it from other interactive theorem provers. It has native support for Unicode symbols, which can be typed using LaTeX-like sequences, such as "\times" for "×".

Isabelle (proof assistant)

The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring yet supporting explicit proof objects. Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of formal methods.

Related lectures (53)

Coq: Introduction

Introduces Coq, covering defining propositions, proving theorems, and using tactics.

The Languages of Isabelle: Isar, ML, and Scala

Explores the languages of Isabelle, focusing on Isar, ML, and Scala, covering proof schemes, Natural Deduction rules, inductive definitions, and the LCF approach.

Automated Reasoning: Formal Verification with LISA

Explores formal verification using the LISA proof assistant and the OCBSL Equivalence Checker.

Proofs: Logic, Mathematics & Algorithms

Explores proof concepts, techniques, and applications in logic, mathematics, and algorithms.

Coq Workshop: Inductive Data Types and Proofs

Covers the definition of an inductive data type in Coq and how to build proofs interactively using tactics.

Related concepts (27)

Proof assistant

Coq

Mathematical proof

Lean (proof assistant)

Isabelle (proof assistant)