rocq proof: structural decrease is well founded

5 files changed, 74 insertions, 0 deletions

diff --git a/theories/.lia.cache b/theories/.lia.cache
new file mode 100644
index 0000000..03484cb
--- /dev/null
+++ b/theories/.lia.cache
diff --git a/theories/Decrease.v b/theories/Decrease.v
new file mode 100644
index 0000000..ceab918
--- /dev/null
+++ b/theories/Decrease.v
@@ -0,0 +1,61 @@
+(* The core claim of the admission checker (decision 10, rung one):
+   a rule whose recursive call argument is strictly contained in the
+   head argument terminates, because strict containment decreases a
+   natural measure and the induced order is well founded.
+
+   Terms are abstracted to what the measure sees: scalars and
+   variables are leaves, records are nodes over their attribute
+   values. Labels do not matter to the measure, so they are erased
+   here; the OCaml checker walks the same tree shape. *)
+
+From Stdlib Require Import List Arith Lia Wf_nat.
+Import ListNotations.
+
+Inductive term : Type :=
+| Leaf : term
+| Node : list term -> term.
+
+Fixpoint size (t : term) : nat :=
+  match t with
+  | Leaf => 1
+  | Node ts => S (fold_right (fun u acc => size u + acc) 0 ts)
+  end.
+
+(* Strict containment: the argument sits somewhere inside the record
+   structure, at depth one or more. This mirrors
+   Pattern.strictly_contains in lib/pattern.ml. *)
+Inductive strictly_contains : term -> term -> Prop :=
+| sc_child : forall ts t,
+    In t ts -> strictly_contains (Node ts) t
+| sc_deeper : forall ts u t,
+    In u ts -> strictly_contains u t -> strictly_contains (Node ts) t.
+
+Lemma in_size_le :
+  forall ts t, In t ts ->
+    size t <= fold_right (fun u acc => size u + acc) 0 ts.
+Proof.
+  induction ts as [| a ts IH]; simpl; intros t H.
+  - contradiction.
+  - destruct H as [-> | H].
+    + lia.
+    + specialize (IH _ H). lia.
+Qed.
+
+Theorem strict_containment_decreases :
+  forall a b, strictly_contains a b -> size b < size a.
+Proof.
+  intros a b H; induction H as [ts t Hin | ts u t Hin Hsc IH]; simpl.
+  - pose proof (in_size_le _ _ Hin). lia.
+  - pose proof (in_size_le _ _ Hin). lia.
+Qed.
+
+(* The decrease order: b below a when a strictly contains b. Well
+   founded via the size measure, so any chain of admitted recursive
+   unfoldings is finite. *)
+Definition decrease (b a : term) : Prop := strictly_contains a b.
+
+Theorem decrease_well_founded : well_founded decrease.
+Proof.
+  apply well_founded_lt_compat with (f := size).
+  intros x y H. apply strict_containment_decreases. exact H.
+Qed.
diff --git a/theories/Decrease.vok b/theories/Decrease.vok
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/theories/Decrease.vok
diff --git a/theories/Decrease.vos b/theories/Decrease.vos
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/theories/Decrease.vos
diff --git a/theories/dune b/theories/dune
new file mode 100644
index 0000000..895fc92
--- /dev/null
+++ b/theories/dune
@@ -0,0 +1,13 @@
+; Checked with rocq's coqc directly: the coq.theory stanza trips on
+; the devshell's OCaml findlib path, and a plain rule with a clean
+; environment is enough to keep the proofs in the default build.
+(rule
+ (targets Decrease.vo Decrease.glob)
+ (deps Decrease.v)
+ (action
+  (setenv OCAMLPATH ""
+   (run coqc -q Decrease.v))))
+
+(alias
+ (name default)
+ (deps Decrease.vo))