blob: ceab91870bc57d099fa446b5512d6e5b33393edc (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
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.
|
