path: root/theories/Decrease.v

(* 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.