#+TITLE: Extraction

* About

Decision 10 says the thing proven should be the thing running. This
document describes the first instance: the structural containment
check that admission relies on is extracted from Rocq and linked
into the library, replacing the hand written OCaml.

* The pieces

- =theories/Decrease.v= states the abstract argument: strict
  containment decreases a natural measure and the induced order is
  well founded.
- =theories/DecreaseChecker.v= carries the argument to an executable
  checker faithful to the real term shape: leaves keep their
  identity (variable names, scalar values) and nodes keep their
  labels. Both matter; a checker that conflated two variables or two
  label sets would accept rules that do not decrease. The file
  proves the boolean checker sound (a successful check is real
  containment) and proves the decrease theorem over it.
- =lib/extract.v= drives extraction into =decrease_extracted.ml=, a
  build artifact generated by dune, never committed.
- =lib/pattern.ml= converts a pattern into the checker's term shape
  and calls the extracted function.

* The trusted seam

Extraction does not remove trust, it narrows it. What remains
outside the proofs:

- the conversion from =Pattern.t= to the checker's terms, injective
  by construction: each leaf kind is distinct and records become
  labeled field lists in canonical order;
- the two equality functions handed to the checker, label equality
  and leaf equality, which are the standard equalities of their
  types;
- the admission logic around the check, and the engine itself.

The regression suite pins the sharp edge: a recursive rule whose
call argument is a fresh variable must be rejected, which fails on
any checker that conflates leaf identities.

* Building

The proofs compile as part of the default build through plain dune
rules that call =coqc= with a clean =OCAMLPATH= (the =coq.theory=
stanza clashes with the devshell's OCaml). The Rocq standard library
comes from =pkgs.coqPackages.stdlib=, packaged separately from Rocq
itself.