library-advisor

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.

1.03x

Quality

86%

Does it follow best practices?

Impact

96%

1.03x

Average score across 3 eval scenarios

Securityby

Passed

No known issues

Evaluation results

100%

Coq Proof Assistance: List Properties

Coq library imports and lemma names

Criteria

Without context

With context

List library import

100%

ListNotations import

100%

rev_involutive lemma

100%

in_app_iff lemma

100%

app_length lemma

100%

Proof with apply

100%

Search command shown

100%

Search with pattern

100%

Automation tactic mentioned

100%

No Isabelle-only syntax

100%

Complete proof structure

100%

Isabelle/HOL Arithmetic Proofs: Lemma Discovery and Proof Strategies

Isabelle lemma discovery and automation tactics

Criteria

Without context

With context

add_commute lemma

50%

100%

add_mult_distrib lemma

100%

mult_assoc lemma

100%

Main library

100%

find_theorems shown

100%

find_theorems name search

100%

sledgehammer mentioned

100%

Automation first

100%

simp add: syntax

100%

arith tactic

100%

No Coq-only syntax

100%

Proof structure

100%

90%

Library Advisor: Combined List and Set Proofs

Multi-domain proof assistance and lemma combination

Criteria

Without context

With context

set_append Isabelle lemma

100%

in_app_iff Coq lemma

100%

map_append Isabelle lemma

100%

map_app Coq lemma

100%

Un_commute Isabelle lemma

100%

Int_commute Isabelle lemma

100%

MSets for Coq sets

60%

Combined lemma proof

100%

Isabelle simp add: combination

100%

Automation recommended

100%

Simplify-first tip

100%

Domain identification

62%

100%

Repository: ArabelaTso/Skills-4-SE
Commit: 0f00a4f

Evaluated: 29 days ago
Agent: Claude Code
Model: Claude Sonnet 4.6

Table of Contents

Coq Proof Assistance: List Properties Isabelle/HOL Arithmetic Proofs: Lemma Discovery and Proof Strategies Library Advisor: Combined List and Set Proofs

Is this your skill?

If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.