Coq Lemma Discovery

Coq Lemma Discovery

Comprehensive guide for discovering and using lemmas in Coq.

Searching for Lemmas

Search Commands

Search by pattern:

Search (_ + _).
(* Finds all lemmas involving addition *)

Search by name:

Search "plus".
(* Finds all lemmas with "plus" in name *)

SearchAbout (deprecated, use Search):

Search nat.
(* Finds all lemmas about nat *)

SearchPattern:

SearchPattern (_ + 0).
(* Finds lemmas matching the pattern *)

Search with constraints:

Search (_ + _) inside Arith.
(* Search only in Arith module *)

Search (_ + _) -"_ * _".
(* Exclude multiplication *)

Locate

Find where a name is defined:

Locate "++".
(* Shows: Notation "x ++ y" := app x y *)

Locate plus.
(* Shows: Constant Coq.Init.Nat.add *)

Print

Display definition or theorem:

Print plus.
(* Shows definition of plus *)

Print Nat.add_comm.
(* Shows statement and proof of commutativity *)

Automatic Proof Search

Auto and Eauto

auto: Applies simple tactics automatically

Lemma example : forall n, n + 0 = n.
Proof.
  auto.
Qed.

eauto: More powerful, uses existential variables

Lemma example : exists n, n + 5 = 10.
Proof.
  eauto.
Qed.

With depth limit:

Proof.
  auto 10.  (* Search depth 10 *)
Qed.

With hint database:

Proof.
  auto with arith.
Qed.

Intuition and Tauto

intuition: Propositional reasoning

Lemma example : forall P Q, P /\ Q -> Q /\ P.
Proof.
  intuition.
Qed.

tauto: Tautology checker

Lemma example : forall P Q, (P -> Q) -> ~Q -> ~P.
Proof.
  tauto.
Qed.

Omega and Lia

omega (deprecated): Linear arithmetic

Require Import Omega.

Lemma example : forall n m, n < m -> n + 1 <= m.
Proof.
  intros. omega.
Qed.

lia: Modern linear integer arithmetic

Require Import Lia.

Lemma example : forall n m, n < m -> n + 1 <= m.
Proof.
  intros. lia.
Qed.

Ring and Field

ring: Ring equations

Require Import Ring.

Lemma example : forall x y, (x + y) * (x + y) = x*x + 2*x*y + y*y.
Proof.
  intros. ring.
Qed.

field: Field equations

Require Import Field.

Lemma example : forall x, x <> 0 -> x / x = 1.
Proof.
  intros. field. auto.
Qed.

Common Lemma Patterns

List Lemmas

Append properties:

Lemma app_nil_l : forall A (l : list A), [] ++ l = l.
Lemma app_nil_r : forall A (l : list A), l ++ [] = l.
Lemma app_assoc : forall A (l m n : list A), l ++ m ++ n = (l ++ m) ++ n.
Lemma app_length : forall A (l l' : list A), length (l ++ l') = length l + length l'.

Map properties:

Lemma map_app : forall A B (f : A -> B) l l',
  map f (l ++ l') = map f l ++ map f l'.
Lemma map_map : forall A B C (f : A -> B) (g : B -> C) l,
  map g (map f l) = map (fun x => g (f x)) l.
Lemma map_length : forall A B (f : A -> B) l,
  length (map f l) = length l.

Filter properties:

Lemma filter_app : forall A (f : A -> bool) l l',
  filter f (l ++ l') = filter f l ++ filter f l'.
Lemma filter_length : forall A (f : A -> bool) l,
  length (filter f l) <= length l.

Reverse properties:

Lemma rev_app_distr : forall A (l l' : list A),
  rev (l ++ l') = rev l' ++ rev l.
Lemma rev_involutive : forall A (l : list A),
  rev (rev l) = l.
Lemma rev_length : forall A (l : list A),
  length (rev l) = length l.

Arithmetic Lemmas

Addition:

Lemma plus_0_l : forall n, 0 + n = n.
Lemma plus_0_r : forall n, n + 0 = n.
Lemma plus_comm : forall n m, n + m = m + n.
Lemma plus_assoc : forall n m p, n + (m + p) = (n + m) + p.
Lemma plus_reg_l : forall n m p, p + n = p + m -> n = m.

Multiplication:

Lemma mult_0_l : forall n, 0 * n = 0.
Lemma mult_1_l : forall n, 1 * n = n.
Lemma mult_comm : forall n m, n * m = m * n.
Lemma mult_assoc : forall n m p, n * (m * p) = (n * m) * p.
Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p.

Ordering:

Lemma le_refl : forall n, n <= n.
Lemma le_trans : forall n m p, n <= m -> m <= p -> n <= p.
Lemma le_antisym : forall n m, n <= m -> m <= n -> n = m.
Lemma plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q.

Boolean Lemmas

Basic properties:

Lemma andb_true_iff : forall b1 b2, b1 && b2 = true <-> b1 = true /\ b2 = true.
Lemma orb_true_iff : forall b1 b2, b1 || b2 = true <-> b1 = true \/ b2 = true.
Lemma negb_involutive : forall b, negb (negb b) = b.

Induction Lemmas

Strengthening Induction

Problem: Induction hypothesis too weak.

Pattern: Generalize with additional parameter.

Example:

(* Too specific *)
Fixpoint sum_n (n : nat) : nat :=
  match n with
  | 0 => 0
  | S n' => n + sum_n n'
  end.

Lemma sum_n_formula : forall n,
  2 * sum_n n = n * (n + 1).
Proof.
  induction n.
  - reflexivity.
  - simpl. (* Stuck: induction hypothesis not strong enough *)
Abort.

(* Generalized version *)
Lemma sum_n_formula_gen : forall n acc,
  2 * (acc + sum_n n) = 2 * acc + n * (n + 1).
Proof.
  induction n; intros; simpl.
  - lia.
  - rewrite IHn. lia.
Qed.

Mutual Induction

Pattern: Define mutually recursive predicates.

Example:

Fixpoint even (n : nat) : bool :=
  match n with
  | 0 => true
  | S n' => odd n'
  end
with odd (n : nat) : bool :=
  match n with
  | 0 => false
  | S n' => even n'
  end.

Lemma even_odd_correct : forall n,
  (even n = true <-> exists k, n = 2 * k) /\
  (odd n = true <-> exists k, n = 2 * k + 1).
Proof.
  induction n.
  - split; split; intros.
    + exists 0. reflexivity.
    + reflexivity.
    + discriminate.
    + destruct H as [k H]. discriminate.
  - destruct IHn as [[IH1 IH2] [IH3 IH4]].
    split; split; intros.
    + (* Use IH3 for odd case *)
    + (* Use IH4 for odd case *)
    + (* Use IH1 for even case *)
    + (* Use IH2 for even case *)
Qed.

Well-Founded Induction

Pattern: Induction on well-founded relation.

Example:

Require Import Wellfounded.

Lemma lt_wf_ind : forall P : nat -> Prop,
  (forall n, (forall m, m < n -> P m) -> P n) ->
  forall n, P n.
Proof.
  intros P H n.
  apply (well_founded_ind lt_wf P H n).
Qed.

Rewriting Lemmas

Basic Rewriting

rewrite: Apply equation left-to-right

Lemma example : forall n, n + 0 = n.
Proof.
  intros. rewrite plus_0_r. reflexivity.
Qed.

rewrite <-: Apply equation right-to-left

Lemma example : forall n, n = n + 0.
Proof.
  intros. rewrite <- plus_0_r. reflexivity.
Qed.

Multiple rewrites:

Lemma example : forall n m, n + m + 0 = m + n.
Proof.
  intros. rewrite plus_0_r, plus_comm. reflexivity.
Qed.

Conditional Rewriting

Pattern: Rewrite under conditions.

Example:

Lemma example : forall n m,
  n < m -> n + 1 <= m.
Proof.
  intros n m H.
  rewrite <- (Nat.succ_pred m).
  - apply le_n_S. apply H.
  - (* Prove m <> 0 *)
    destruct m.
    + inversion H.
    + discriminate.
Qed.

Case Analysis Lemmas

Destruct and Case

destruct: Case analysis on term

Lemma example : forall n, n = 0 \/ n > 0.
Proof.
  intros. destruct n.
  - left. reflexivity.
  - right. apply Nat.lt_0_succ.
Qed.

case_eq: Case analysis with equation

Lemma example : forall b, b = true \/ b = false.
Proof.
  intros. case_eq b; intros.
  - left. auto.
  - right. auto.
Qed.

Inversion

Pattern: Analyze constructor equations.

Example:

Inductive even : nat -> Prop :=
  | even_0 : even 0
  | even_SS : forall n, even n -> even (S (S n)).

Lemma even_not_odd : forall n,
  even n -> ~ even (S n).
Proof.
  intros n H. induction H.
  - intro H'. inversion H'.
  - intro H'. inversion H'. contradiction.
Qed.

Proof Automation with Ltac

Custom Tactics

Simple tactic:

Ltac solve_by_inversion :=
  match goal with
  | H : _ |- _ => inversion H; subst; auto
  end.

Recursive tactic:

Ltac crush :=
  repeat (simpl; auto; try discriminate; try contradiction; try congruence).

Pattern matching tactic:

Ltac destruct_match :=
  match goal with
  | |- context[match ?x with _ => _ end] => destruct x
  | H : context[match ?x with _ => _ end] |- _ => destruct x
  end.

Hint Databases

Create hint database:

Create HintDb my_hints.

Add hints:

Hint Resolve my_lemma : my_hints.
Hint Rewrite my_eq : my_hints.
Hint Constructors my_inductive : my_hints.

Use hints:

Proof.
  auto with my_hints.
Qed.

Lemma Discovery Workflow

Step 1: Try Automatic Tactics

Lemma goal : ...
Proof.
  auto.
  (* or *)
  intuition.
  (* or *)
  lia.
Qed.

Step 2: Search for Lemmas

Search (_ + _).
SearchPattern (_ + 0).

Step 3: Manual Proof

Lemma goal : ...
Proof.
  intros.
  rewrite lemma1.
  apply lemma2.
  reflexivity.
Qed.

Step 4: Identify Missing Lemmas

If proof fails, propose new lemma.

Example: Complete Discovery

Goal:

Lemma filter_map_length : forall A B (f : A -> B) (P : B -> bool) l,
  length (filter P (map f l)) <= length l.

Attempt 1:

Proof.
  induction l; simpl.
  - reflexivity.
  - (* Stuck: need to case on P (f a) *)
Abort.

Search for lemmas:

Search (length (filter _ _)).
(* Finds: filter_length *)

Attempt 2:

Proof.
  induction l; simpl.
  - reflexivity.
  - destruct (P (f a)).
    + simpl. apply le_n_S. apply IHl.
    + (* Stuck: need lemma about <= and S *)
Abort.

Search for lemmas:

Search (_ <= S _).
(* Finds: le_S *)

Final proof:

Proof.
  induction l; simpl.
  - reflexivity.
  - destruct (P (f a)).
    + simpl. apply le_n_S. apply IHl.
    + apply le_S. apply IHl.
Qed.

Alternative with automation:

Proof.
  induction l; simpl; auto.
  destruct (P (f a)); simpl; auto.
Qed.