bend2-learn-proofs

Extract — Bend2 learn/proofs: Canonical proof workflow

• URL: https://bend2.dev/learn/proofs/
• Site: bend2.dev learn docs (canonical tutorial)
• Related (already extracted): what-is-bend2.md, bend2-vs-lean.md, bend README extract
• Read via: defuddle parse —md
• Overlap note: Core law/def/{==} ideas appear in what-is-bend2; this page is the worked half_ok tutorial (statement + rewrite motive + Empty branch). Not redundant for DIY harness wiring.

Claims / workflow

Worked example: prove Nat.double(half(x)) == x for even x.

1. Predicate as type: IsEven(n): Type via match (0→Unit, odd→Empty, 2n+p→IsEven(p)).
2. Executable half: structural match on Nat.
3. law half_ok: for x: Nat / for e: IsEven(x) / {Nat.double(half(x)) == x : Nat} — equality proposition with type annotation.
4. def half_ok proves the law: match on x:
   • 0n → {==} (both sides compute equal)
   • odd → match e: with no cases (Empty uninhabited)
   • 2n+p → recursive IH %half_ok(p, e) : {2n+Nat.double(half(p)) == 2n+_ : Nat} then {==}
5. Rewrite motive: in %equation : motive, _ marks the RHS slot replaced by equation’s LHS; sides reduce; {==} closes.
6. Recursion must use structurally smaller p.
7. Run: bend main.bend evaluates pure main; -o main compiles native.

Quotes / teaching points

“Bend quantifies with for x: Nat and states equality as {left == right : Nat}.”

“half(1n) returns zero, but the law makes no assertion about that input: IsEven(1n) is Empty.”

“Bend performs this proof with ordinary recursion and an explicit rewrite motive. Lean’s tactics can construct these proof terms automatically.”

DIY / fleet relevance

• Agent repair target for Bend: emit matching law+def, use {==}, %ih : motive with _, Empty-elim via empty match — no tactics to lean on.
• Spec discipline: restricting with IsEven avoids proving false claims on odd inputs (vacuity via Empty).
• CI gate remains bend PROOF.bend / checker; this page is the human/agent curriculum for the proof dialect.
• Choose Bend when affine+executable laws matter; Lean when tactics/mathlib needed (links bend2-vs-lean).

Caveats

• Tutorial only — no maturity/kernel claims beyond what’s on sister notes.
• Checker↔Lean formalization mismatches still apply (see what-is-bend2 extract); source proof ≠ full toolchain trust.