Library Usage Advisor

Recommend relevant libraries, lemmas, and theories from Isabelle/HOL or Coq standard libraries based on proof goals.

Workflow

1. Analyze the Proof Goal

Examine the goal to identify:

• Domain: Lists, sets, arithmetic, logic, etc.
• Operations: Specific functions or operators involved
• Pattern: Commutativity, associativity, distributivity, etc.
• Complexity: Simple property vs. complex relationship

2. Determine Target System

Identify which proof assistant:

• Isabelle/HOL: Use Main library and extensions
• Coq: Use standard library (List, Arith, etc.)
• Both: Provide recommendations for both systems

3. Identify Relevant Libraries

Based on the domain, recommend appropriate libraries:

For list operations:

• Isabelle: Main (List theory included)
• Coq:

  Require Import List. Import ListNotations.

For arithmetic:

• Isabelle: Main (Nat theory included)
• Coq:

  Require Import Arith Lia.

For sets:

• Isabelle: Main (Set theory included)
• Coq:

  Require Import MSets.

For logic:

• Isabelle: HOL (automatically available)
• Coq:

  Require Import Logic.

4. Search for Specific Lemmas

Look for lemmas that directly match the goal:

Exact matches: Lemmas that prove the goal directly Component lemmas: Lemmas for parts of the goal Related lemmas: Similar properties that might help

Use the library reference files:

• Isabelle library: See isabelle_library.md
• Coq library: See coq_library.md

5. Recommend Usage

Provide concrete recommendations:

Direct application:

lemma "goal"
  by (simp add: relevant_lemma)

With additional steps:

Lemma goal : statement.
Proof.
  apply relevant_lemma.
  (* additional steps *)
Qed.

Manual proof with lemmas: Show how to use lemmas in a structured proof

6. Suggest Search Commands

Teach users how to find lemmas themselves:

Isabelle:

find_theorems "pattern"
find_theorems name: "keyword"
sledgehammer

Coq:

Search pattern.
Search "keyword".
Locate "notation".

Domain-Specific Recommendations

Lists

Common goals:

• Length properties:

  length_append

  ,

  length_rev

  ,

  length_map

• Reverse properties:

  rev_rev_ident

  ,

  rev_append

• Append properties:

  append_assoc

  ,

  append_Nil

• Map properties:

  map_append

  ,

  map_map

• Membership:

  in_set_member

  ,

  set_append

Libraries:

• Isabelle: Main (automatic)
• Coq:

  List

  library

Arithmetic

Common goals:

• Commutativity:

  add_commute

  ,

  mult_commute

• Associativity:

  add_assoc

  ,

  mult_assoc

• Distributivity:

  add_mult_distrib

• Inequalities: Use

  arith

  /

  lia

  tactics

Libraries:

• Isabelle: Main (Nat theory)
• Coq:

  Arith

  ,

  Lia

  ,

  Nia

Sets

Common goals:

• Union/intersection:

  Un_commute

  ,

  Int_commute

• Subset:

  subset_refl

  ,

  subset_trans

• Membership:

  Un_iff

  ,

  Int_iff

Libraries:

• Isabelle: Main (Set theory)
• Coq:

  MSets

  or custom definitions

Logic

Common goals:

• Conjunction:

  conjI

  ,

  conjE

• Disjunction:

  disjI1

  ,

  disjI2

• Implication:

  impI

  ,

  mp

• Quantifiers:

  allI

  ,

  exI

Libraries:

• Isabelle: HOL (automatic)
• Coq:

  Logic

  (mostly automatic)

Recommendation Patterns

Pattern 1: Exact Lemma Match

When goal exactly matches a known lemma:

Isabelle:

lemma "rev (rev xs) = xs"
  by (simp add: rev_rev_ident)

Coq:

Lemma example : forall l, rev (rev l) = l.
Proof.
  apply rev_involutive.
Qed.

Pattern 2: Combination of Lemmas

When goal needs multiple lemmas:

Isabelle:

lemma "length (rev (xs @ ys)) = length xs + length ys"
  by (simp add: length_rev length_append)

Coq:

Lemma example : forall l1 l2,
  length (rev (l1 ++ l2)) = length l1 + length l2.
Proof.
  intros.
  rewrite rev_length.
  rewrite app_length.
  reflexivity.
Qed.

Pattern 3: Automation

When goal is provable by automation:

Isabelle:

lemma "n + m = m + n"
  by simp
(* Or: by auto, by arith *)

Coq:

Lemma example : forall n m, n + m = m + n.
Proof.
  intros. lia.
Qed.

Pattern 4: Induction with Lemmas

When manual proof needed but lemmas help:

Isabelle:

lemma "property xs"
proof (induction xs)
  case Nil
  show ?case by simp
next
  case (Cons x xs)
  show ?case using Cons.IH by (simp add: helper_lemma)
qed

Coq:

Lemma example : forall l, property l.
Proof.
  induction l as [| x xs IHxs].
  - simpl. reflexivity.
  - simpl. rewrite IHxs. apply helper_lemma.
Qed.

Search Strategies

Strategy 1: Pattern-Based Search

Isabelle:

find_theorems "rev (rev _) = _"
find_theorems "length (_ @ _)"
find_theorems "_ + _ = _ + _"

Coq:

Search rev.
Search (_ ++ _).
Search (?x + ?y = ?y + ?x).

Strategy 2: Name-Based Search

Isabelle:

find_theorems name: "append"
find_theorems name: "comm"

Coq:

Search "append".
Search "comm" (_ + _).

Strategy 3: Type-Based Search

Coq:

Search (list _ -> nat).
Search (_ -> _ -> _ + _).

Strategy 4: Sledgehammer/Auto

Isabelle:

lemma "goal"
  sledgehammer
  (* Suggests relevant lemmas and tactics *)

Coq:

Lemma goal : statement.
Proof.
  auto.  (* Try automatic tactics *)
Qed.

Common Recommendations by Goal Type

"rev (rev xs) = xs"

• Isabelle:

  rev_rev_ident

  or

  by simp

• Coq:

  rev_involutive

"length (xs @ ys) = length xs + length ys"

• Isabelle:

  length_append

  or

  by simp

• Coq:

  app_length

"n + m = m + n"

• Isabelle:

  add_commute

  or

  by simp

• Coq:

  plus_comm

  or

  lia

"x ∈ set (xs @ ys) ⟷ x ∈ set xs ∨ x ∈ set ys"

• Isabelle:

  set_append

• Coq:

  in_app_iff

"map f (xs @ ys) = map f xs @ map f ys"

• Isabelle:

  map_append

• Coq:

  map_app

Examples

For complete examples with specific proof goals and library recommendations, see examples.md.

Tips

• Search first: Use find_theorems/Search before proving manually
• Check automation: Try simp/auto/lia before complex proofs
• Use sledgehammer: In Isabelle, sledgehammer finds relevant lemmas
• Import early: Import all needed libraries at the start
• Learn patterns: Common properties (commutativity, etc.) have standard names
• Read library docs: Browse standard library documentation
• Build intuition: Learn which libraries contain which lemmas
• Combine lemmas: Complex goals often need multiple lemmas
• Simplify first: Use simp/simpl to reduce goals before searching