diff options
| -rw-r--r-- | .gitignore | 3 | ||||
| -rw-r--r-- | dune-project | 2 | ||||
| -rw-r--r-- | flake.nix | 1 | ||||
| -rw-r--r-- | sol.opam | 2 | ||||
| -rw-r--r-- | theories/.lia.cache | bin | 0 -> 268 bytes | |||
| -rw-r--r-- | theories/Decrease.v | 61 | ||||
| -rw-r--r-- | theories/Decrease.vok | 0 | ||||
| -rw-r--r-- | theories/Decrease.vos | 0 | ||||
| -rw-r--r-- | theories/dune | 13 |
9 files changed, 80 insertions, 2 deletions
@@ -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) @@ -57,6 +57,7 @@ ocamlPackages.menhir # Rocq, for the verified checkers and their extraction pkgs.coq + pkgs.coqPackages.stdlib ]; }; }); @@ -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 Binary files differnew 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)) |