Add product list example proving the append homomorphism

[jsiek]

What

Adds examples/product.pf, a new worked example: the classic intro-to-functional-programming product function over List<UInt>,

product :: [Int] -> Int
product []     = 1
product (x:xs) = x * product xs

and a proof that it is a homomorphism from (List<UInt>, ++) to (UInt, *):

product(xs ++ ys) = product(xs) * product(ys)

This is the multiplicative twin of the library's length_append, proved by structural induction on xs. The example is not already covered in examples/ (the existing concat.pf, sum_*, and length-related examples are distinct functions).

Validation

Both parsers accept it with no warnings:

python deduce.py examples/product.pf            # valid
python deduce.py --lalr examples/product.pf     # valid

The file also includes three assert sanity checks (product([2,3,4]) = 24, product(@[]<UInt>) = 1, product([5]) = 5).

Note

While writing this with the recommended mcp__deduce__* workflow I hit a friction point filed as #991: the MCP check_file tool reported the proof clean, but deduce.py flagged two redundant replace arguments that an auto rule already handles. The committed proof has those redundant arguments removed.

🤖 Generated with Claude Code