Library Fnormalization
Require Import Inclusion. (* wf_incl *)
Require Import Inverse_Image. (* wf_inverse_image *)
Require Import Wf_nat.
Require Import Omega.
Require Import Min.
Require Import minmax.
Require Import Flanguage.
Inductive Fnormalization_v := .
Require Import Inverse_Image. (* wf_inverse_image *)
Require Import Wf_nat.
Require Import Omega.
Require Import Min.
Require Import minmax.
Require Import Flanguage.
Inductive Fnormalization_v := .
We define a very simple measure on indexed terms. The measure of a
term is its top-level index.
Definition measure a :=
match a with
| Var k _ ⇒ k
| Lam k _ ⇒ k
| App k _ _ ⇒ k
| Unit k ⇒ k
| Pair k _ _ ⇒ k
| Fst k _ ⇒ k
| Snd k _ ⇒ k
| Absurd k _ ⇒ k
| Inl k _ ⇒ k
| Inr k _ ⇒ k
| Match k _ _ _ ⇒ k
| Gen k _ ⇒ k
| Inst k _ ⇒ k
end.
match a with
| Var k _ ⇒ k
| Lam k _ ⇒ k
| App k _ _ ⇒ k
| Unit k ⇒ k
| Pair k _ _ ⇒ k
| Fst k _ ⇒ k
| Snd k _ ⇒ k
| Absurd k _ ⇒ k
| Inl k _ ⇒ k
| Inr k _ ⇒ k
| Match k _ _ _ ⇒ k
| Gen k _ ⇒ k
| Inst k _ ⇒ k
end.
The measure strictly decreases by reduction. This is the key of
the proof.
Lemma red_measure : ∀ a b, red a b → measure b < measure a.
Proof.
intros a b Hred; induction Hred; [destruct c|..]; simpl; auto;
repeat match goal with
| H : _ ∧ _ |- _ ⇒ destruct H
end;
match goal with
| |- measure (lower ?k ?a) < _ ⇒
apply le_trans with (m := S k); auto; pose proof (measure_lower k a); minmax
end.
Qed.
Proof.
intros a b Hred; induction Hred; [destruct c|..]; simpl; auto;
repeat match goal with
| H : _ ∧ _ |- _ ⇒ destruct H
end;
match goal with
| |- measure (lower ?k ?a) < _ ⇒
apply le_trans with (m := S k); auto; pose proof (measure_lower k a); minmax
end.
Qed.
The reduction of the untyped indexed calculus is strongly
normalizing.
Lemma wf_der : well_founded der.
Proof.
eapply wf_incl; [|apply wf_inverse_image with (f := measure); apply lt_wf].
intros b a Hred; apply red_measure; auto.
Qed.
Definition Fix := @Coq.Init.Wf.Fix term der wf_der.
Proof.
eapply wf_incl; [|apply wf_inverse_image with (f := measure); apply lt_wf].
intros b a Hred; apply red_measure; auto.
Qed.
Definition Fix := @Coq.Init.Wf.Fix term der wf_der.
Since all indexed term are strongly normalizing, we may prove
properties by induction on the reduction of some indexed term.
Lemma ind_red : ∀ a (P : term → Prop),
(∀ a, (∀ b, red a b → P b) → P a) → P a.
Proof. intros a P F; induction (wf_der a); apply F; apply H0. Qed.
Ltac induction_red a := let IHa := fresh "IH" a in
apply (ind_red a); clear a; intros a IHa.
(∀ a, (∀ b, red a b → P b) → P a) → P a.
Proof. intros a P F; induction (wf_der a); apply F; apply H0. Qed.
Ltac induction_red a := let IHa := fresh "IH" a in
apply (ind_red a); clear a; intros a IHa.