Recommend relevant Isabelle/HOL or Coq standard library theories, lemmas, and tactics based on proof goals. Use when: (1) Users need library lemmas for their proof, (2) Proof goals match standard library patterns, (3) Users ask what libraries to import, (4) Specific lemmas are needed for list/set/arithmetic operations, (5) Users are stuck and need to know what library support exists, or (6) Guidance on find_theorems/Search commands is needed. Supports both Isabelle/HOL and Coq standard libraries.
Recommend relevant libraries, lemmas, and theories from Isabelle/HOL or Coq standard libraries based on proof goals.
Examine the goal to identify:
Identify which proof assistant:
Based on the domain, recommend appropriate libraries:
For list operations:
Require Import List. Import ListNotations.For arithmetic:
Require Import Arith Lia.For sets:
Require Import MSets.For logic:
Require Import Logic.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:
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
Teach users how to find lemmas themselves:
Isabelle:
find_theorems "pattern"
find_theorems name: "keyword"
sledgehammer
Coq:
Search pattern.
Search "keyword".
Locate "notation".
Common goals:
length_append, length_rev, length_maprev_rev_ident, rev_appendappend_assoc, append_Nilmap_append, map_mapin_set_member, set_appendLibraries:
List libraryCommon goals:
add_commute, mult_commuteadd_assoc, mult_assocadd_mult_distribarith/lia tacticsLibraries:
Arith, Lia, NiaCommon goals:
Un_commute, Int_commutesubset_refl, subset_transUn_iff, Int_iffLibraries:
MSets or custom definitionsCommon goals:
conjI, conjEdisjI1, disjI2impI, mpallI, exILibraries:
Logic (mostly automatic)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.
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.
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.
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.
Isabelle:
find_theorems "rev (rev _) = _"
find_theorems "length (_ @ _)"
find_theorems "_ + _ = _ + _"
Coq:
Search rev.
Search (_ ++ _).
Search (?x + ?y = ?y + ?x).
Isabelle:
find_theorems name: "append"
find_theorems name: "comm"
Coq:
Search "append".
Search "comm" (_ + _).
Coq:
Search (list _ -> nat).
Search (_ -> _ -> _ + _).
Isabelle:
lemma "goal"
sledgehammer
(* Suggests relevant lemmas and tactics *)
Coq:
Lemma goal : statement.
Proof.
auto. (* Try automatic tactics *)
Qed.
rev_rev_ident or by simprev_involutivelength_append or by simpapp_lengthadd_commute or by simpplus_comm or liaset_appendin_app_iffmap_appendmap_appFor complete examples with specific proof goals and library recommendations, see examples.md.