Rocq Alethe walker R-2: walker scaffolding + clausal layer

Mirror of Lean PR #42 — the biggest single PR in the Rocq arc.
Establishes the EConstr construction template every subsequent
PR follows.

What's added:

* Reference resolution helpers mirroring `term_mode.ml`'s lazy
  `Rocqlib.lib_ref` pattern: num.Z.* arithmetic operators and
  comparisons, num.pos.* positive constructors, core.* logical
  connectives, core.eq.type, core.False.type, etc.
* `positive_of_z` / `z_lit` integer literal construction (the
  walker emits Z constructors directly; `parse_int_atom` handles
  both "-3" and rational-denominator-1 "-3/1" forms cvc5 emits).
* Walker types: `walker_ctx` (Names.Id.Map of atom name →
  EConstr local-var), `walker_state` (mutable Hashtbl of step
  id → proof+clause). Lean used `StateRefT MetaM`; Coq plugin
  convention is OCaml refs + Hashtbl since the walking phase
  itself is pure OCaml (no Proofview) — only goal assignment
  crosses into `Proofview.Refine.refine`.
* `sexp_to_constr` / `list_to_constr` / `and_or_chain` covering
  the LIA fragment: integer literals, +/-/*/<=/</>=/>/= over Z,
  not/and/or/cl/=>, true/false. For `=` we hardcode the type
  as Z for R-2's scope; boolean equality arrives in R-7
  alongside equiv1/equiv2.
* Four rule elaborators (clausal layer):
  - `elab_assume_literal` — match assume literal against local
    hyp by `Reductionops.is_conv`, return `mkVar` of the match.
  - `elab_false_step` — `(cl (not false))` → `fun (h : False) => h`
    via raw `EConstr.mkLambda` + `mkRel 1`.
  - `elab_or` — passthrough restating premise's proof under
    the step's flattened clause-literal list.
  - `elab_resolution_simple` — complementary-singleton pair
    only (n-ary lift in R-4).
* `walk_proof` dispatch: phase 1 seeds assumes against local
  context, phase 2 walks steps in order.
* `walker_test` tactic entry point — parses, walks, defeq-
  checks against goal, refines. On any error (parse fail, walker
  error, type mismatch) raises `tclZEROMSG` cleanly so test
  failures surface as tactic errors, not crashes.

Exposed via `g_proof_broker.mlg`:

  alethe_walker_test "..." (string literal trace)

Mirror of Lean's `aletheWalkerTest`. One test in `Test.v`
(`alethe_walker_clausal_axiom_free`) closes `forall A, A -> ~A -> False`
via a hand-written 3-step trace, proves axiom-free (allowlist
entry: []).

Validation: local Rocq env broken per project memory (no
zarith/rocq-runtime locally); rely on CI for build + axiom
gate. May need iterations to nail down exact EConstr API names
(`Reductionops.is_conv` vs `Equality.conv?`, `Tacticals.tclZEROMSG`
vs `Proofview.tclZERO`, `Sorts.Relevant` enum location, etc.) —
that's the documented Rocq parity workflow.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Author: levineuwirth