demos: proof_userland_tactics — a tactic from userland

[Kampouse]

A demo, not a proposal: on stock 2.0.37, a tactic as a library.

• propositions as data (P), Interp : P -> Type into native goals
• auto(p) -> Maybe<Interp(p)> decides the fragment; Some{...} carries the proof term, None{} is the honest refusal
• quantified laws (min_le, le_succ_r) stay hand-proved beside it; instances go through the tactic, definitionally — Interp(PLe{a, b}) normalizes to the native goal itself, so there is no glue

The README shows the run transcript, including what happens when a bug is introduced in min: the tactic flips Some -> None and names the unprovable goal, and the quantified law fails with it. That None is the agent-facing signal: not "error", but "here is what I could not prove".

The load-bearing feature is a computed type family in a generic signature (Maybe<Interp(p)> as a return type). No quote, no unify, no compiler changes — reflection, not metaprogramming; the Limits section says so plainly (match A on a Type parameter is a dead-region error, and goal introspection does not exist, so the framework reaches exactly the fragment you embed, soundly, and nothing else).

Verified on 2.0.37 (darwin/arm64):

$ bend demos/proof_userland_tactics/main.bend
Some Some None
$ bend demos/proof_userland_tactics/PROOF.bend
ALL PROOFS CHECK

and the buggy-min edit reproduces Some None None + SOME PROOFS FAIL.

[Kampouse]

i was reading the otherday some part of https://fstar-lang.org/papers/metafstar/ and
seen in the repo there was no tactics well you can have them just sharing its possible in the userland