rocq proof: structural decrease is well founded

9 files changed, 80 insertions, 2 deletions

diff --git a/.gitignore b/.gitignore
index 5059366..c7c6422 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,6 @@ _build/
 *.install
 .direnv/
 result
+*.vo
+*.glob
+*.aux
diff --git a/dune-project b/dune-project
index 0a36d26..4ba98c7 100644
--- a/dune-project
+++ b/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.7)
+(lang dune 3.17)
 
 (name sol)
 
diff --git a/flake.nix b/flake.nix
index 77264eb..8a52938 100644
--- a/flake.nix
+++ b/flake.nix
@@ -57,6 +57,7 @@
               ocamlPackages.menhir
               # Rocq, for the verified checkers and their extraction
               pkgs.coq
+              pkgs.coqPackages.stdlib
             ];
           };
         });
diff --git a/sol.opam b/sol.opam
index 9f46a1c..c2dc35f 100644
--- a/sol.opam
+++ b/sol.opam
@@ -7,7 +7,7 @@ maintainer: ["Marcos Magueta <maguetamarcos@gmail.com>"]
 authors: ["Marcos Magueta"]
 license: "AGPL-3.0-only"
 depends: [
-  "dune" {>= "3.7"}
+  "dune" {>= "3.17"}
   "ocaml" {>= "5.1"}
   "zarith"
   "menhir" {build}
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))