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

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

Lemma red_measure : a b, red a bmeasure b < measure a.
intros a b Hred; induction Hred; simpl; auto;
repeat match goal with
         | H : _ _ |- _destruct H
match goal with
  | |- measure (lessen ?k ?a) < _
    apply le_trans with (m := S k); auto; pose proof (measure_lessen k a); minmax

Lemma wf_der : well_founded der.
eapply wf_incl; [|apply wf_inverse_image with (f := measure); apply lt_wf].
intros b a Hred; apply red_measure; auto.

Definition Fix := @Coq.Init.Wf.Fix term der wf_der.

Lemma ind_red : a (P : termProp),
  ( a, ( b, red a bP 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.