arabelatso/skills-4-se/library-for-proof-advisor

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