-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathAdministrativeNormalization.v
More file actions
135 lines (125 loc) · 5.28 KB
/
Copy pathAdministrativeNormalization.v
File metadata and controls
135 lines (125 loc) · 5.28 KB
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
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
From Stdlib Require Import Relations.Relation_Operators
Wellfounded Wellfounded.Inverse_Image.
Require Import AdministrativeMeasures.
Require Import AdministrativeReduction.
Require Import AdministrativeAlgebra.
Import SharedPrompts.
Import StructuralNormalization.StructuralReduction.
Import StructuralNormalization.WeightedNormalization.
Import StructuralNormalization.LetAssociationNormalization.
Lemma tail_step_to_measure_relation k x y :
tail_step k x y ->
tail_shift_step (ECont k x) (ECont k y) \/
abort_tail_step (ECont k x) (ECont k y).
Proof.
intro H. destruct (tail_step_shape k x y H)
as [[l [e [Hx [Hy Hocc]]]]|[l [e [Hx Hy]]]].
- subst x; subst y. left. apply CTS_ContTail. exact Hocc.
- subst x; subst y. right. apply AT_ContTail.
Qed.
Lemma admin_step_measure_classification :
(forall v v', admin_vstep v v' ->
let_shift_vstep v v' \/ let_assoc_vstep v v' \/
tail_shift_vstep v v' \/ abort_tail_vstep v v') /\
(forall e e', admin_step e e' ->
let_shift_step e e' \/ let_assoc_step e e' \/
tail_shift_step e e' \/ abort_tail_step e e').
Proof.
apply admin_mutind.
- intros e e' H IH. destruct IH as [IH|[IH|[IH|IH]]].
+ left; apply LSV_Lam; exact IH.
+ right; left; apply LAV_Lam; exact IH.
+ right; right; left; apply CTSV_Lam; exact IH.
+ right; right; right; apply ATV_Lam; exact IH.
- intros v v' H IH. destruct IH as [IH|[IH|[IH|IH]]].
+ left; apply LS_Val; exact IH.
+ right; left; apply LA_Val; exact IH.
+ right; right; left; apply CTS_Val; exact IH.
+ right; right; right; apply AT_Val; exact IH.
- intros v v' u H IH. destruct IH as [IH|[IH|[IH|IH]]].
+ left; apply LS_AppLeft; exact IH.
+ right; left; apply LA_AppLeft; exact IH.
+ right; right; left; apply CTS_AppLeft; exact IH.
+ right; right; right; apply AT_AppLeft; exact IH.
- intros v u u' H IH. destruct IH as [IH|[IH|[IH|IH]]].
+ left; apply LS_AppRight; exact IH.
+ right; left; apply LA_AppRight; exact IH.
+ right; right; left; apply CTS_AppRight; exact IH.
+ right; right; right; apply AT_AppRight; exact IH.
- intros a a' t H IH. destruct IH as [IH|[IH|[IH|IH]]].
+ left; apply LS_LetBinding; exact IH.
+ right; left; apply LA_LetBinding; exact IH.
+ right; right; left; apply CTS_LetBinding; exact IH.
+ right; right; right; apply AT_LetBinding; exact IH.
- intros a t t' H IH. destruct IH as [IH|[IH|[IH|IH]]].
+ left; apply LS_LetBody; exact IH.
+ right; left; apply LA_LetBody; exact IH.
+ right; right; left; apply CTS_LetBody; exact IH.
+ right; right; right; apply AT_LetBody; exact IH.
- intros e e' H IH. destruct IH as [IH|[IH|[IH|IH]]].
+ left; apply LS_ShiftBody; exact IH.
+ right; left; apply LA_ShiftBody; exact IH.
+ right; right; left; apply CTS_ShiftBody; exact IH.
+ right; right; right; apply AT_ShiftBody; exact IH.
- intros k e e' H IH. destruct IH as [IH|[IH|[IH|IH]]].
+ left; apply LS_ContBody; exact IH.
+ right; left; apply LA_ContBody; exact IH.
+ right; right; left; apply CTS_ContBody; exact IH.
+ right; right; right; apply AT_ContBody; exact IH.
- intros k e e' H. destruct (tail_step_to_measure_relation k e e' H)
as [Hd|Ha].
+ right; right; left; exact Hd.
+ right; right; right; exact Ha.
- intros e t. left. apply LS_Root.
- intros a u t. right; left. apply LA_Root.
Qed.
Lemma admin_step_rank_decreases e e' :
admin_step e e' ->
normalization_rank_lt (normalization_rank e') (normalization_rank e).
Proof.
intro H.
destruct (proj2 admin_step_measure_classification e e' H)
as [Hshift | [Hassoc | [Htail | Habort]]].
- unfold normalization_rank_lt, normalization_rank.
apply left_slex.
exact (weighted_let_shift_step_decreases Hshift).
- unfold normalization_rank_lt, normalization_rank.
rewrite (weighted_let_assoc_preserves_weighted_norm Hassoc).
apply right_slex. apply left_slex.
exact (let_assoc_potential_decreases Hassoc).
- exact (tail_shift_rank_decreases Htail).
- exact (abort_rank_decreases Habort).
Qed.
Theorem admin_step_well_founded :
well_founded (fun y x => admin_step x y).
Proof.
eapply wf_incl.
- intros y x H.
apply admin_step_rank_decreases. exact H.
- apply (wf_inverse_image expr
(nat * (nat * (nat * (nat * nat))))
normalization_rank_lt normalization_rank normalization_rank_well_founded).
Qed.
(* Value steps are the mutually recursive companion of [admin_step]. They do
not need a second termination measure: putting a value under [EVal] turns
every value step into an expression step. This is also useful when one
wants the usual mutual strong-normalisation statement, rather than only
the expression projection above. *)
Theorem admin_vstep_well_founded :
well_founded (fun y x => admin_vstep x y).
Proof.
eapply wf_incl.
- intros y x H.
apply AS_Val. exact H.
- apply (wf_inverse_image value expr
(fun y x => admin_step x y) (fun v => EVal v)
admin_step_well_founded).
Qed.
Definition admin_sn (e : expr) : Prop :=
Acc (fun y x => admin_step x y) e.
Theorem admin_strongly_normalizing e : admin_sn e.
Proof. apply admin_step_well_founded. Qed.
Definition admin_vsn (v : value) : Prop :=
Acc (fun y x => admin_vstep x y) v.
Theorem admin_values_strongly_normalizing v : admin_vsn v.
Proof. apply admin_vstep_well_founded. Qed.