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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
(* The executable admission checker, proven and extracted.
Decrease.v states the abstract argument: strict containment
decreases a well founded measure. This file carries the argument
over to an executable checker faithful to lib/pattern.ml: terms
keep their labels and leaf identities, the checker is a boolean
function, and its soundness is proven, so extraction can replace
the hand written OCaml. The equality functions supplied by the
host and the conversion from Pattern.t are the remaining trusted
seam. *)
From Stdlib Require Import Arith Lia Bool Wf_nat.
Section Checker.
Variables (L A : Type).
Variables (eqL : L -> L -> bool) (eqA : A -> A -> bool).
(* Terms as the checker sees them: leaves carry their identity
(variable name, scalar value), nodes carry labeled fields in
canonical order. Mirrors Pattern.t through an injective
conversion. *)
Inductive term : Type :=
| Leaf : A -> term
| Node : fields -> term
with fields : Type :=
| FNil : fields
| FCons : L -> term -> fields -> fields.
Scheme term_mut := Induction for term Sort Prop
with fields_mut := Induction for fields Sort Prop.
Combined Scheme term_fields_mut from term_mut, fields_mut.
Fixpoint term_eqb (x y : term) : bool :=
match x, y with
| Leaf a, Leaf b => eqA a b
| Node f, Node g => fields_eqb f g
| _, _ => false
end
with fields_eqb (f g : fields) : bool :=
match f, g with
| FNil, FNil => true
| FCons l t r, FCons l' t' r' =>
eqL l l' && term_eqb t t' && fields_eqb r r'
| _, _ => false
end.
(* Strict containment: [sub] occurs somewhere inside the fields of
[t], at depth one or more. *)
Fixpoint contains (sub t : term) : bool :=
match t with
| Leaf _ => false
| Node f => fields_contain sub f
end
with fields_contain (sub : term) (f : fields) : bool :=
match f with
| FNil => false
| FCons _ t r => term_eqb t sub || contains sub t || fields_contain sub r
end.
Fixpoint size (t : term) : nat :=
match t with
| Leaf _ => 1
| Node f => S (fields_size f)
end
with fields_size (f : fields) : nat :=
match f with
| FNil => 0
| FCons _ t r => size t + fields_size r
end.
Hypothesis eqL_sound : forall x y, eqL x y = true -> x = y.
Hypothesis eqA_sound : forall x y, eqA x y = true -> x = y.
Lemma eqb_sound_all :
(forall x, forall y, term_eqb x y = true -> x = y)
/\ (forall f, forall g, fields_eqb f g = true -> f = g).
Proof.
apply term_fields_mut.
- intros a y H; destruct y; simpl in H; [ f_equal; auto | discriminate ].
- intros f IH y H; destruct y; simpl in H; [ discriminate | f_equal; auto ].
- intros g H; destruct g; [ reflexivity | discriminate ].
- intros l t IHt r IHr g H; destruct g; simpl in H; [ discriminate | ].
rewrite !andb_true_iff in H; destruct H as [[Hl Ht] Hr].
f_equal; auto.
Qed.
Definition term_eqb_sound := proj1 eqb_sound_all.
Lemma contains_size_all :
(forall t, forall sub, contains sub t = true -> size sub < size t)
/\ (forall f, forall sub, fields_contain sub f = true -> size sub <= fields_size f).
Proof.
apply term_fields_mut.
- intros a sub H; simpl in H; discriminate.
- intros f IH sub H; simpl in H; simpl.
specialize (IH _ H); lia.
- intros sub H; simpl in H; discriminate.
- intros l t IHt r IHr sub H; simpl in H; simpl.
rewrite !orb_true_iff in H; destruct H as [[He | Hc] | Hr].
+ apply term_eqb_sound in He; subst; lia.
+ specialize (IHt _ Hc); lia.
+ specialize (IHr _ Hr); lia.
Qed.
Definition contains_decreases := proj1 contains_size_all.
(* The checker's acceptance order is well founded: any chain of
recursive unfoldings whose argument the checker accepts is
finite. This is what admission buys at runtime. *)
Definition decrease (b a : term) : Prop := contains b a = true.
Theorem decrease_well_founded : well_founded decrease.
Proof.
apply well_founded_lt_compat with (f := size).
intros x y H; apply contains_decreases; exact H.
Qed.
End Checker.
|
