15. Introduction to Coq and Agda as Proof Assistants

Introduction to Coq and Agda as Proof Assistants

Coq and Agda are interactive theorem proving systems commonly used as proof assistants in the field of formal verification and constructive mathematics.

They provide a formal language for expressing mathematical statements and proofs, and they support the development of certified software by allowing users to specify properties and verify their correctness.

In Coq and Agda, mathematical objects are represented as types, and proofs are represented as terms inhabiting these types.

Key features of Coq and Agda include:

• Dependent types: Both Coq and Agda support dependent types, allowing types to depend on values.
• Interactive proof development: Users can interactively construct proofs step by step, guided by the system's feedback.
• Tactic-based proof scripting: Coq provides a tactic language for scripting proofs, while Agda uses a more direct programming style for proofs.
• Proof automation: Both systems offer libraries of tactics or combinators to automate common proof tasks.

Lab Activity: Proving a Theorem in Coq

Let's prove a simple theorem in Coq to demonstrate the interactive proof development process.

Theorem plus_comm : forall n m : nat, n + m = m + n.
Proof.
  intros n m.
  induction n as [| n' IHn'].
  - simpl. rewrite <- plus_n_O. reflexivity.
  - simpl. rewrite <- IHn'. rewrite <- plus_n_Sm. reflexivity.
Qed.
  

In the lab activity, we prove the commutativity of addition over natural numbers.

We start by introducing the universal quantifiers using the `intros` tactic.

We then perform induction on the first argument `n` using the `induction` tactic.

In the base case, we simplify the expression and apply the `plus_n_O` lemma.

In the inductive case, we simplify the expression, use the induction hypothesis `IHn'`, and apply the `plus_n_Sm` lemma.