Attempts at using claude code #4
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
- Add core types section (Proof, BoolRef, ExprRef, SortRef) - Document Z3 basics and operator overloading - Highlight preferred @Theorem decorator style over kd.Lemma - Add complete tactics reference organized by purpose - Document definitions, axioms, and FreshVar usage - Add algebraic datatypes examples (Inductive, Struct, etc.) - Include quantifier helpers (QForAll, QExists, QImplies) - Document Calc for equational reasoning - Add theory maturity status to guide which modules to use This comprehensive reference improves AI assistance performance by providing clear, organized information about the library's API and recommended usage patterns. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <[email protected]>
- Renamed kernel function instan2 -> specialize - Renamed tactic method instan -> specialize - Updated all internal usages in tactics.py and zf.py - Updated CLAUDE.md documentation - All tests pass (392 passed) This aligns with standard proof assistant naming conventions where "specialize" is used for universal quantifier instantiation. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <[email protected]>
examples/intlist.py: - Complete theory of integer lists with Inductive datatype - Defines length, append, and reverse functions - Proves properties: length_nonneg, append_nil_r, length_append, append_assoc, rev_append, rev_rev - Demonstrates proper use of @Theorem decorator - Shows how to handle induction on datatypes CLAUDE.md improvements: - Document that induct() generates ForAll for ALL constructor fields - Add requirement to use fixes() not fix() after induction on Cons - New "Common Proof Patterns" section with: - Standard induction proof structure - How to use by= parameter effectively - Debugging tips for proof timeouts - Add examples/intlist.py to stable examples list Key lesson: After l.induct(x) on a datatype like IntList with Cons(head, tail), must use `head, tail = l.fixes()` to open both fields, not `l.fix()` which fails on multiple quantifiers. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <[email protected]>
…tyles examples/intlist.py additions: - Define mem, map, filter, and sum functions on integer lists - Prove 9 new theorems: * mem_append_tactic (tactic style) * mem_append_left (shows reusing lemmas) * length_rev, length_map, length_filter * map_append (Isar style with explicit have statements) * sum_append (detailed Isar style) * sum_map_double (map-sum fusion property) * Sanity check that append is not commutative - Total: 15 theorems with concrete examples CLAUDE.md updates: - Split proof patterns into "Tactic-style" and "Isar-style" - Document tactic style (Lean/Rocq): fix, induct, auto - Document Isar style (Isabelle): explicit forward reasoning with have - Key insight: `pf.have(fact)` transforms goal to `fact -> goal` - After multiple `have` statements, must use `pf.auto()` to discharge - `pf.show(exact_goal)` requires exact match then proves - Clarify when to use each style: tactic for concise, Isar for clarity Key lessons documented: - Isar-style accumulates implications that need discharging - Tactic-style lets Z3 do more automatic work - Both styles work, choose based on proof readability needs 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <[email protected]>
examples/intlist.py additions (Section 2): - FreshVar demonstration: Schema variables for parametric proofs - Functions: take, drop, all, zip (with Struct IntPair) - Tactics explored: * simp with unfold=True * rw (rewrite) for equational steps * Calc for multi-step equational reasoning * sub() context manager for subgoals - Proofs with detailed Lean/Coq/Isabelle comparisons in docstrings - Total: 20+ theorems with 10 features demonstrated Key insights documented: - FreshVar usage: Create schema variables, then generalize with .forall() - Variable scoping: Must use fresh Consts for each function definition - Proof instability: Integer case analysis (take_drop) can timeout - Limitation: Higher-order quantification (∀P. ...) problematic in Z3 - Comparison notes showing equivalent syntax in Lean/Coq/Isabelle CLAUDE.md additions (user requested): - Development philosophy: recommend improvements, track learnings - Document proof instability concerns - Note limitations vs other proof assistants Features successfully demonstrated: ✓ FreshVar and .forall() generalization ✓ simp, rw, Calc tactics ✓ Struct (IntPair) and multiple Inductives ✓ Concrete predicate usage (avoiding higher-order issues) ✓ Side-by-side comparisons with Lean/Coq/Isabelle syntax 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <[email protected]>
Changed direct comparisons to True/False to use smt.BoolVal(True/False) for Z3 expressions to comply with ruff E712 linting rules. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I had it update CLAUDE.md after I changed it some.
Told it to go off to the races on examples/intlist.py . Pretty impressed so far.