blob: 17ce70d0ad6c80ec0647cfdf9d17e8cb4c2cc067 (
plain) (
tree)
|
|
#+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.
|
