Add plausible property testing framework

[alok]

Summary

• Added the plausible library for property-based testing (similar to QuickCheck)
• Created utilities and examples for using plausible testing
• Integrated plausible checks into existing specs

Key Changes

1. Added plausible dependency - Using leanprover-community/plausible for counterexample finding
2. PlausibleUtils module - Helper functions and tactics for common test patterns
3. PlausibleExamples module - Demonstrations of property testing with lists, matrices, and custom types
4. Updated specs - Added plausible tests to problem_87_spec before sorry to catch assumption violations
5. Documentation - Comprehensive guide in CLAUDE.md for using plausible testing

Benefits

• Early error detection: Find counterexamples quickly before attempting full proofs
• Improved sorry-driven development: Replace bare sorry with by plausible; sorry
• Pit of success: Models can validate assumptions before investing in verification
• Regression testing: Ensure spec changes don't break existing properties

Test Plan

• Add plausible library dependency
• Create testing utilities
• Write example property tests
• Update existing specs
• Run full build to verify compilation (in progress - large codebase)

🤖 Generated with Claude Code

[Copilot]

Pull Request Overview

This PR adds the plausible property-based testing framework to the vericoding project to enhance specification validation through counterexample finding. The integration enables early detection of specification errors and improves the sorry-driven development workflow.

Key changes include:

• Added plausible library dependency and created testing utilities
• Integrated plausible tests into existing specifications for early validation
• Updated import paths and build configuration for proper Lean project structure

Reviewed Changes

Copilot reviewed 41 out of 42 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
lakefile.lean	Added plausible dependency and new library targets
lean/Testing/PlausibleUtils.lean	Created utility functions and tactics for property testing
lean/Testing/PlausibleExamples.lean	Added comprehensive examples of plausible usage patterns
vericoding/core/language_tools.py	Enhanced Lean verification to run from project root directory
config/language_config.yaml	Updated Lean build commands to use lake instead of direct lean calls
lean/Benchmarks/clever/src/lean4/specs/problem_87_spec.lean	Added plausible validation tests before proof attempt
Multiple spec files	Fixed import paths and added missing helper definitions

[Copilot]

The findCounterexample function is incomplete with a sorry implementation. This could cause runtime errors if called, and the function signature suggests it should return actual counterexamples.

Suggested change

	sorry
	let mut i := 0
	while i < maxAttempts do
	let x ← Sampleable.sample
	let holds ← Testable.check { numInst := 1 } (property x)
	match holds with
	| TestResult.success _ => pure ()
	| _ => return some x
	i := i + 1
	return none

[Copilot]

This property is mathematically incorrect - list concatenation is not commutative. The plausible tactic should find a counterexample, but this demonstrates an intentionally false property as an example.

Suggested change

	example : ∀ (xs ys : List Nat), xs ++ ys = ys ++ xs := by
	example : ∀ (xs ys zs : List Nat), (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by

[Copilot]

This mathematical property is incorrect. For a rectangle with width=1, height=4, perimeter=10 but 2sqrt(4)=4, so 10 ≥ 4 holds, but for width=10, height=1, perimeter=22 but 2sqrt(10)≈6.32, which still holds. However, the correct isoperimetric inequality for rectangles should be perimeter² ≥ 16*area.

Suggested change

	example : ∀ r : Rectangle, r.perimeter ≥ 2 * r.area.sqrt := by
	example : ∀ r : Rectangle, r.perimeter * r.perimeter ≥ 16 * r.area := by

[Copilot]

[nitpick] The variable cwd is initialized but may remain None for non-Lean languages, which could cause issues if other languages also need project root detection in the future.

Suggested change

	cwd = None
	cwd = os.getcwd()