Library Fnormalization

Require Import Inclusion. Require Import Inverse_Image. Require Import Wf_nat.
Require Import Omega.
Require Import Min.

Require Import minmax.
Require Import Flanguage.

Definition der b a := red a b.

Definition measure a :=
  match a with
    | Var k _ ⇒ k
    | Lam k _ ⇒ k
    | App k _ _ ⇒ k
    | Pair k _ _ ⇒ k
    | Fst k _ ⇒ k
    | Snd k _ ⇒ k
  end.

Lemma measure_lessen : ∀ k a, measure (lessen k a) ≤ k.
Proof. induction a; simpl; minmax. Qed.

Lemma red_measure : ∀ a b, red a b → measure b < measure a.
Proof.
intros a b Hred; induction Hred; simpl; auto;
repeat match goal with
         | H : _ ∧ _ |- _ ⇒ destruct H
       end;
match goal with
  | |- measure (lessen ?k ?a) < _ ⇒
    apply le_trans with (m := S k); auto; pose proof (measure_lessen k a); minmax
end.
Qed.

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.

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.