Library Flanguage

Require Import Omega.
Require Import Min.
Require Import Max.

Require Import set.
Require Import minmax.

Inductive term : Set :=
| Var (k : nat) (x : nat)
| Lam (k : nat) (a : term)
| App (k : nat) (a : term) (b : term)
| Pair (k : nat) (a : term) (b : term)
| Fst (k : nat) (a : term)
| Snd (k : nat) (a : term)



.
Definition Var_x := Var.
Hint Unfold Var_x.

Definition map_fuel (f : nat → nat) := fix g a :=
  match a with
    | Var k x ⇒ Var (f k) x
    | Lam k a ⇒ Lam (f k) (g a)
    | App k a b ⇒ App (f k) (g a) (g b)
    | Pair k a b ⇒ Pair (f k) (g a) (g b)
    | Fst k a ⇒ Fst (f k) (g a)
    | Snd k a ⇒ Snd (f k) (g a)
    
    
    
  end.

Definition unary_fuel f := fix g a :=
  match a with
    | Var k x ⇒ f k
    | Lam k a ⇒ f k ∧ g a
    | App k a b ⇒ f k ∧ g a ∧ g b
    | Pair k a b ⇒ f k ∧ g a ∧ g b
    | Fst k a ⇒ f k ∧ g a
    | Snd k a ⇒ f k ∧ g a
    
    
    
  end.

Definition binary_fuel f := fix g a b :=
  match a, b with
    | Var j x, Var k y ⇒ f j k ∧ x = y
    | Lam j a, Lam k b ⇒ f j k ∧ g a b
    | App j a1 a2, App k b1 b2 ⇒ f j k ∧ g a1 b1 ∧ g a2 b2
    | Pair j a1 a2, Pair k b1 b2 ⇒ f j k ∧ g a1 b1 ∧ g a2 b2
    | Fst j a, Fst k b ⇒ f j k ∧ g a b
    | Snd j a, Snd k b ⇒ f j k ∧ g a b
    
    
    
    | _, _ ⇒ False
  end.

Definition lessen k := map_fuel (fun j ⇒ min j k).
Definition le_term := binary_fuel le.
Definition term_le a k := unary_fuel (fun j ⇒ j ≤ k) a.
Definition term_lt a k := unary_fuel (fun j ⇒ j < k) a.
Definition term_ge a k := unary_fuel (fun j ⇒ j ≥ k) a.
Hint Unfold lessen le_term term_le term_lt term_ge.

Ltac destruct_binary a H :=
  destruct a; simpl in H; try (exfalso; exact H);
  match type of H with
    | _ ∧ _ ∧ _ ∧ _ ⇒ destruct H as [? [? [? ?]]]
| _ ∧ _ ∧ _ ⇒ destruct H as [? [? ?]]
| _ ∧ _ ⇒ destruct H
    | _ ⇒ idtac
  end.

Definition traverse f := fix g i a :=
  match a with
  | Var k x ⇒ f k x i
  | Lam k a ⇒ Lam k (g (1 + i) a)
  | App k a b ⇒ App k (g i a) (g i b)
  | Pair k a b ⇒ Pair k (g i a) (g i b)
  | Fst k a ⇒ Fst k (g i a)
  | Snd k a ⇒ Snd k (g i a)
  
  
  
  end.

Definition lift_idx d k x i := Var k (if le_gt_dec i x then d + x else x).
Definition lift d := traverse (lift_idx d).
Definition shift := lift 1.
Hint Unfold lift_idx lift shift.

Definition subst_idx b k x i :=
  match lt_eq_lt_dec x i with
    | inleft (left _) ⇒ Var k x
    | inleft (right _) ⇒ lessen k (lift x 0 b)
    | inright _ ⇒ Var k (x - 1)
  end.
Definition subst b := traverse (subst_idx b).
Hint Unfold subst_idx subst.

Definition set := @set term.

Inductive red : term → term → Prop :=
| RedCtxLam : ∀ k a a', red a a' → red (Lam (1 + k) a) (Lam k a')
| RedCtxApp1 : ∀ k a b a', red a a' → red (App (1 + k) a b) (App k a' b)
| RedCtxApp2 : ∀ k a b b', red b b' → red (App (1 + k) a b) (App k a b')
| RedCtxPair1 : ∀ k a b a', red a a' → red (Pair (1 + k) a b) (Pair k a' b)
| RedCtxPair2 : ∀ k a b b', red b b' → red (Pair (1 + k) a b) (Pair k a b')
| RedCtxFst : ∀ k a a', red a a' → red (Fst (1 + k) a) (Fst k a')
| RedCtxSnd : ∀ k a a', red a a' → red (Snd (1 + k) a) (Snd k a')





| RedApp : ∀ k k' a b, red (App (1 + k') (Lam (1 + k) a) b) (lessen (min k' k) (subst b 0 a))
| RedFst : ∀ k k' a b, red (Fst (1 + k') (Pair (1 + k) a b)) (lessen (min k' k) a)
| RedSnd : ∀ k k' a b, red (Snd (1 + k') (Pair (1 + k) a b)) (lessen (min k' k) b)


.

Definition N : set := fun a ⇒
  match a with
    | Var _ _ ⇒ True
    | App _ _ _ ⇒ True
    | Fst _ _ ⇒ True
    | Snd _ _ ⇒ True
    
    | Lam _ _ ⇒ False
    | Pair _ _ _ ⇒ False
    
    
  end.

Definition CN : set := fun a ⇒
  match a with
    | Lam _ _ ⇒ True
    | Pair _ _ _ ⇒ True
    
    
    | Var _ _ ⇒ False
    | App _ _ _ ⇒ False
    | Fst _ _ ⇒ False
    | Snd _ _ ⇒ False
    
  end.

Lemma N_dec : ∀ a, {CN a} + {N a}.
Proof. destruct a; simpl; auto. Qed.

Lemma CN_N : ∀ a, CN a → N a → False.
Proof. destruct a; auto. Qed.

Inductive Err : set :=
| ErrCtxLam : ∀ k e, Err e → Err (Lam k e)
| ErrCtxApp1 : ∀ k e a, Err e → Err (App k e a)
| ErrCtxApp2 : ∀ k e a, Err e → Err (App k a e)
| ErrCtxPair1 : ∀ k e a, Err e → Err (Pair k e a)
| ErrCtxPair2 : ∀ k e a, Err e → Err (Pair k a e)
| ErrCtxFst : ∀ k e, Err e → Err (Fst k e)
| ErrCtxSnd : ∀ k e, Err e → Err (Snd k e)

| ErrApp : ∀ k k' a1 a2 b, Err (App k (Pair k' a1 a2) b)
| ErrFst : ∀ k k' a, Err (Fst k (Lam k' a))
| ErrSnd : ∀ k k' a, Err (Snd k (Lam k' a))
.

Definition V : set := Cmp Err.
Hint Unfold V.

Definition NV : set := Inter N V.

Lemma V_Var : ∀ {k n}, V (Var k n).
Proof. intros k n Herr; inversion Herr. Qed.

Lemma NV_Var : ∀ {k n}, NV (Var k n).
Proof. split; [exact I|apply V_Var]. Qed.

Lemma V_Lam : ∀ {k a}, V a → V (Lam k a).
Proof. intros k a H Herr; inversion Herr; auto. Qed.

Lemma V_Pair : ∀ {k a b}, V a → V b → V (Pair k a b).
Proof. intros k a b Ha Hb Herr; inversion Herr; auto. Qed.

Lemma V_subst_N : ∀ a b, N b → ∀ i, V (subst b i a) → V a.
Proof.
intros a b Nb; induction a; intros i Va; try (intros Errb; inversion Errb; subst); try (
match goal with
  | IHa : ∀ _, _ → V ?a
    , Erra : Err ?a |- _ ⇒ eapply IHa; [|exact Erra]
end; intros Erra; apply Va; simpl; eauto using Err).
apply Va; apply ErrApp.
apply Va; apply ErrFst.
apply Va; apply ErrSnd.
Qed.

Ltac subst_lift_var := repeat (match goal with
    | |- context[subst_idx] ⇒ unfold subst_idx
    | |- context[lift_idx] ⇒ unfold lift_idx
    | |- context[lt_eq_lt_dec ?x ?y] ⇒ destruct (lt_eq_lt_dec x y) as [[?|?]|?]; try (exfalso; omega); simpl; auto
    | |- context[le_gt_dec ?x ?y] ⇒ destruct (le_gt_dec x y); try (exfalso; omega); simpl; auto
  end).

Lemma lift_0 : ∀ a i, lift 0 i a = a.
Proof. induction a; intros i; simpl; [subst_lift_var|..]; f_equal; auto. Qed.

Lemma unary_fuel_1 : ∀ (f g : nat → Prop), (∀ j, f j → g j) →
  ∀ a, unary_fuel f a → unary_fuel g a.
Proof.
intros f g fg; induction a; simpl; intros H;
repeat (match goal with
  | H : _ ∧ _ |- _ ⇒ destruct H
  | |- _ ∧ _ ⇒ split
end; auto); auto.
Qed.

Lemma unary_fuel_2 : ∀ (g f1 f2 : nat → Prop), (∀ j, f1 j → f2 j → g j) →
  ∀ a, unary_fuel f1 a → unary_fuel f2 a → unary_fuel g a.
Proof.
intros g f1 f2 fg; induction a; simpl; intros H1 H2;
repeat (match goal with
  | H : _ ∧ _ |- _ ⇒ destruct H
  | |- _ ∧ _ ⇒ split
end; auto); auto.
Qed.

Lemma unary_fuel_map : ∀ (f : nat → Prop) upd,
  (∀ k, f k → f (upd k)) →
  ∀ a, unary_fuel f a → unary_fuel f (map_fuel upd a).
Proof.
intros f upd fupd; induction a; intros H; simpl in *;
repeat (match goal with
  | H : _ ∧ _ |- _ ⇒ destruct H
  | |- _ ∧ _ ⇒ split
end; auto); auto.
Qed.

Lemma unary_fuel_map_trivial : ∀ (f : nat → Prop) upd,
  (∀ k, f (upd k)) → ∀ a, unary_fuel f (map_fuel upd a).
Proof.
intros f upd fupd; induction a; simpl in *;
repeat (match goal with
  | H : _ ∧ _ |- _ ⇒ destruct H
  | |- _ ∧ _ ⇒ split
end; auto); auto.
Qed.

Lemma map_fuel_lift : ∀ d f a i,
  map_fuel f (lift d i a) = lift d i (map_fuel f a).
Proof. intros d f a; induction a; intros i; simpl; f_equal; auto. Qed.

Lemma lessen_lift : ∀ d k a i,
  lessen k (lift d i a) = lift d i (lessen k a).
Proof. intros d k a i; apply map_fuel_lift. Qed.

Lemma lessen_lessen : ∀ k k' a, lessen k (lessen k' a) = lessen (min k' k) a.
Proof. induction a; simpl; f_equal; auto; rewrite min_assoc; reflexivity. Qed.

Lemma lessen_subst : ∀ b k a i,
  lessen k (subst b i a) = subst b i (lessen k a).
Proof.
intros b k a; induction a; intros i; simpl; f_equal; auto.
unfold subst_idx; destruct (lt_eq_lt_dec x i) as [[?|?]|?]; simpl; auto.
rewrite lessen_lessen; reflexivity.
Qed.

Lemma lift_lift : ∀ a d i j l, lift d (j + l) (lift (i + j) l a) = lift (i + d + j) l a.
Proof.
induction a; intros d i j l; simpl; auto; [| |f_equal; auto ..].
subst_lift_var; f_equal; omega.
f_equal; rewrite plus_n_Sm; apply IHa.
Qed.

Lemma lift_subst : ∀ a b d i j,
  lift d j (subst b (i + j) a) = subst b (i + d + j) (lift d j a).
Proof.
induction a; intros b d i j; simpl; auto; [| |f_equal; auto..].
  subst_lift_var; [|f_equal; omega].
  rewrite <- lessen_lift; f_equal.
  replace j with (j + 0) by omega; subst.
  rewrite lift_lift.
  f_equal; omega.
  f_equal; rewrite plus_n_Sm; rewrite IHa; f_equal; omega.
Qed.

Lemma subst_lift : ∀ a b d i l,
  subst b (i + l) (lift (d + 1 + i) l a) = lift (d + i) l a.
Proof.
induction a; intros b d i l; simpl; auto; [| |f_equal; auto..].
subst_lift_var; f_equal; omega.
f_equal; rewrite plus_n_Sm; rewrite IHa; auto.
Qed.

Lemma subst_lift_0 : ∀ a b, subst b 0 (lift 1 0 a) = a.
Proof. intros a b; pose proof (subst_lift a b 0 0 0); simpl in *; rewrite H; apply lift_0. Qed.

Lemma subst_subst : ∀ a b bd d i,
  subst bd (d + i) (subst b i a) = subst (subst bd d b) i (subst bd (1 + d + i) a).
Proof.
induction a; intros b bd d i; simpl; auto;
[| |f_equal; first [rewrite IHa|rewrite IHa1|rewrite IHa2]; reflexivity..].
  subst_lift_var.
    rewrite <- lessen_subst; f_equal.
    replace (subst bd d) with (subst bd (d + 0)) by (f_equal; omega).
    rewrite lift_subst; f_equal; omega.
    rewrite <- lessen_subst; f_equal.
    replace i with (i + 0) by omega.
    replace x with (d + 1 + i) by omega.
    rewrite subst_lift.
    f_equal; omega.
  f_equal.
  rewrite plus_n_Sm.
  rewrite IHa; reflexivity.
Qed.

Lemma subst_subst_0 : ∀ a b bd d,
  subst bd d (subst b 0 a) = subst (subst bd d b) 0 (subst bd (1 + d) a).
Proof.
intros.
replace d with (d + 0) by omega.
rewrite subst_subst; repeat f_equal; omega.
Qed.

Lemma subst_subst_0_0 : ∀ a b bd,
  subst bd 0 (subst b 0 a) = subst (subst bd 0 b) 0 (subst bd 1 a).
Proof. intros; rewrite subst_subst_0; repeat f_equal; omega. Qed.

Lemma binary_fuel_map : ∀ (op : nat → nat → Prop) upd' upd,
  (∀ k' k, op k' k → op (upd' k') (upd k)) →
  ∀ a' a, binary_fuel op a' a → binary_fuel op (map_fuel upd' a') (map_fuel upd a).
Proof.
intros op upd' upd H a'.
induction a'; intros; destruct_binary a H0; simpl; auto.
Qed.

Lemma binary_fuel_map_trivial : ∀ (op : nat → nat → Prop) upd,
  (∀ k, op (upd k) k) →
  ∀ a, binary_fuel op (map_fuel upd a) a.
Proof. intros op upd H a; induction a; simpl; auto. Qed.

Lemma binary_fuel_trans : ∀ (op : nat → nat → Prop),
  (∀ k1 k2 k3, op k1 k2 → op k2 k3 → op k1 k3) →
  ∀ a1 a2 a3, binary_fuel op a1 a2 → binary_fuel op a2 a3 → binary_fuel op a1 a3.
Proof.
intros op H a1.
induction a1; intros; destruct_binary a2 H0; destruct_binary a3 H1; simpl;
try split; first [omega|eauto].
Qed.

Lemma binary_fuel_refl : ∀ (op : nat → nat → Prop),
  (∀ k, op k k) → ∀ a, binary_fuel op a a.
Proof. intros op H a; induction a; simpl; try split; first [omega|eauto]. Qed.

Lemma le_term_lessen : ∀ k' k a' a, k' ≤ k → le_term a' a →
  le_term (lessen k' a') (lessen k a).
Proof. intros; apply binary_fuel_map; intros; auto; minmax. Qed.

Lemma le_term_lessen_trivial : ∀ k a, le_term (lessen k a) a.
Proof. intros; apply binary_fuel_map_trivial; intros; minmax. Qed.

Lemma binary_fuel_lift : ∀ op d a' a i, binary_fuel op a' a →
  binary_fuel op (lift d i a') (lift d i a).
Proof. induction a'; intros; destruct_binary a H; subst; simpl; auto. Qed.

Lemma le_term_subst : ∀ a' a b' b i, le_term b' b → le_term a' a →
  le_term (subst b' i a') (subst b i a).
Proof.
induction a'; intros; destruct_binary a H0; subst; simpl; auto.
  unfold subst_idx.
  destruct (lt_eq_lt_dec x0 i) as [[?|?]|?]; subst; simpl; auto.
  rewrite 2 lessen_lift.
  apply binary_fuel_lift.
  apply binary_fuel_map; auto.
  intros; minmax.
Qed.

Lemma le_term_red : ∀ a a' b', le_term a' a → red a' b' → ∃ b, red a b ∧ le_term b' b.
Proof.
intros a a' b' lea Hred'; generalize a lea; clear a lea.
induction Hred'; intros; destruct_binary a0 lea; try (
match goal with
  | [ H1 : ∀ _, le_term ?a _ → _
    , H2 : le_term ?a _ |- _ ] ⇒ destruct (H1 _ H2) as [? [? ?]]; clear H1 H2
end); try (
match goal with
  | [ H : S _ ≤ ?k |- _ ] ⇒ destruct k; [inversion H|]
end); try (
match goal with
  | [ _ : red ?a ?x |- ∃ _, red (Lam (S ?k) ?a) _ ∧ _ ] ⇒
    ∃ (Lam k x); split; [apply RedCtxLam; assumption|]
  | [ _ : red ?a ?x |- ∃ _, red (App (S ?k) ?a ?b) _ ∧ _ ] ⇒
    ∃ (App k x b); split; [apply RedCtxApp1; assumption|]
  | [ _ : red ?a ?x |- ∃ _, red (App (S ?k) ?b ?a) _ ∧ _ ] ⇒
    ∃ (App k b x); split; [apply RedCtxApp2; assumption|]
  | [ _ : red ?a ?x |- ∃ _, red (Pair (S ?k) ?a ?b) _ ∧ _ ] ⇒
    ∃ (Pair k x b); split; [apply RedCtxPair1; assumption|]
  | [ _ : red ?a ?x |- ∃ _, red (Pair (S ?k) ?b ?a) _ ∧ _ ] ⇒
    ∃ (Pair k b x); split; [apply RedCtxPair2; assumption|]
  | [ _ : red ?a ?x |- ∃ _, red (Fst (S ?k) ?a) _ ∧ _ ] ⇒
    ∃ (Fst k x); split; [apply RedCtxFst; assumption|]
  | [ _ : red ?a ?x |- ∃ _, red (Snd (S ?k) ?a) _ ∧ _ ] ⇒
    ∃ (Snd k x); split; [apply RedCtxSnd; assumption|]
end; simpl; try split; first [omega|auto]).
  destruct_binary a0_1 H0.
  destruct k1; [inversion H0|].
  ∃ (lessen (min k0 k1) (subst a0_2 0 a0_1)).
  split; [apply RedApp|].
  apply le_term_lessen; [minmax|].
  apply le_term_subst; assumption.
  destruct_binary a0 H0.
  destruct k1; [inversion H0|].
  ∃ (lessen (min k0 k1) a0_1).
  split; [apply RedFst|].
  apply le_term_lessen; [minmax|assumption].
  destruct_binary a0 H0.
  destruct k1; [inversion H0|].
  ∃ (lessen (min k0 k1) a0_2).
  split; [apply RedSnd|].
  apply le_term_lessen; [minmax; omega|assumption].
Qed.

Lemma term_ge_dec : ∀ a k, term_ge a (1 + k) → term_ge a k.
Proof.
intros a k H.
eapply unary_fuel_1; [|apply H].
simpl; intros; omega.
Qed.

Lemma term_ge_lessen : ∀ k k', k' ≥ k → ∀ a, term_ge a k → term_ge (lessen k' a) k.
Proof.
intros k k' kk' a H.
eapply unary_fuel_map; [|apply H].
intros; apply min_glb; omega.
Qed.

Lemma unary_fuel_traverse : ∀ (f : nat → Prop) g, (∀ k x i, f k → unary_fuel f (g k x i)) →
  ∀ a i, unary_fuel f a → unary_fuel f (traverse g i a).
Proof.
intros f g fg; induction a; intros i H; simpl in *;
repeat (match goal with
  | H : _ ∧ _ |- _ ⇒ destruct H
  | |- _ ∧ _ ⇒ split
  | |- _ ≥ _ ⇒ omega
end; auto); auto.
Qed.

Lemma unary_fuel_lift : ∀ f d a i, unary_fuel f a → unary_fuel f (lift d i a).
Proof.
intros f d a i H.
apply unary_fuel_traverse; [|apply H].
intros k x l fk; subst_lift_var.
Qed.

Lemma term_ge_lift : ∀ d a k i, term_ge a k → term_ge (lift d i a) k.
Proof. intros d a k i H; apply unary_fuel_lift; apply H. Qed.

Lemma unary_fuel_subst : ∀ (f : nat → Prop), (∀ j k, f j → f k → f (min j k)) →
  ∀ a b i, unary_fuel f a → unary_fuel f b → unary_fuel f (subst b i a).
Proof.
intros f Hf a b i Ha Hb.
apply unary_fuel_traverse; [|apply Ha].
intros k x l fk; subst_lift_var.
apply unary_fuel_map; auto.
apply unary_fuel_lift; apply Hb.
Qed.

Lemma term_ge_subst : ∀ a k b i, term_ge a k → term_ge b k → term_ge (subst b i a) k.
Proof.
intros a k b i Ha Hb.
apply unary_fuel_subst; auto.
intros j1 j2; apply min_glb.
Qed.

Lemma unary_fuel_red : ∀ (f g : nat → Prop),
  (∀ k, f (S k) → g k) → (∀ k, f k → g k) → (∀ j k, g j → g k → g (min j k)) →
  ∀ a b, red a b → unary_fuel f a → unary_fuel g b.
Proof.
intros f g HS Hinc Hmin a b Hred; induction Hred; simpl; intros Ha;
repeat (match goal with
  | H : unary_fuel f ?a |- unary_fuel g ?a ⇒ apply unary_fuel_1 with (f := f); [apply Hinc|apply H]
  | H : _ ∧ _ |- _ ⇒ destruct H
  | |- _ ∧ _ ⇒ split
  | |- _ ≥ _ ⇒ omega
end; auto); auto.
  apply unary_fuel_map; [|apply unary_fuel_subst]; auto; apply unary_fuel_1 with (f := f); auto.
apply unary_fuel_map; auto; apply unary_fuel_1 with (f := f); auto.
apply unary_fuel_map; auto; apply unary_fuel_1 with (f := f); auto.
Qed.

Lemma term_ge_red : ∀ a b k, red a b → term_ge a (1 + k) → term_ge b k.
Proof.
intros a b k Hred Ha.
eapply unary_fuel_red; [| | |apply Hred|apply Ha]; intros.
simpl in H; omega.
simpl in H; omega.
apply min_glb; omega.
Qed.

Lemma term_le_red : ∀ a b k, red a b → term_le a k → term_le b k.
Proof.
intros a b k Hred Ha.
eapply unary_fuel_red; [| | |apply Hred|apply Ha]; intros.
simpl in H; omega.
simpl in H; omega.
minmax.
Qed.

Lemma red_0 : ∀ a b, term_lt a 0 → red a b → False.
Proof.
intros a b H Hred; induction Hred; simpl in *;
repeat (match goal with
  | H : _ < 0 |- _ ⇒ inversion H
  | H : _ ∧ _ |- _ ⇒ destruct H
end; auto); auto.
Qed.

Lemma term_lt_red : ∀ a b k, red a b → term_lt a k → term_lt b k.
Proof.
intros a b k Hred Ha.
destruct k; [exfalso; eapply red_0; eauto|].
eapply unary_fuel_1; [|apply (term_le_red a b k Hred); eapply unary_fuel_1; [|apply Ha]];
instantiate; simpl; intros j H; omega.
Qed.

Lemma red_subst : ∀ a a' b, red a a' → ∀ i, red (subst b i a) (subst b i a').
Proof.
intros a a' b Hred; induction Hred; intros i; simpl; auto using red.
rewrite <- lessen_subst; rewrite subst_subst_0; apply RedApp.
rewrite <- lessen_subst; apply RedFst.
rewrite <- lessen_subst; apply RedSnd.
Qed.

Lemma subst_lessen : ∀ a b i k, subst (lessen k b) i (lessen k a) = subst b i (lessen k a).
Proof.
induction a; intros b i k0; simpl; [|f_equal; auto..].
  subst_lift_var.
  rewrite <- lessen_lift.
  rewrite lessen_lessen.
  f_equal.
  rewrite min_r; auto.
  apply le_min_r.
Qed.

Lemma red_lessen : ∀ a b k, red a b →
  ∃ b', red (lessen (1 + k) a) b' ∧ le_term (lessen k b) b'.
Proof.
intros a b k Hred; induction Hred; simpl lessen;
try (destruct IHHred as [? [? ?]];
match goal with
  | [ _ : red (lessen _ _) ?x |- ∃ _, red (Lam (S ?j) _) _ ∧ _ ] ⇒
    ∃ (Lam j x); simpl; split; [apply RedCtxLam|]
  | [ _ : red (lessen _ ?a) ?x |- ∃ _, red (App (S ?j) (lessen _ ?a) ?b) _ ∧ _ ] ⇒
    ∃ (App j x b); simpl; split; [apply RedCtxApp1|split; [|split]]
| [ _ : red (lessen _ ?a) ?x |- ∃ _, red (App (S ?j) ?b (lessen _ ?a)) _ ∧ _ ] ⇒
    ∃ (App j b x); simpl; split; [apply RedCtxApp2|split; [|split]]
| [ _ : red (lessen _ ?a) ?x |- ∃ _, red (Pair (S ?j) (lessen _ ?a) ?b) _ ∧ _ ] ⇒
    ∃ (Pair j x b); simpl; split; [apply RedCtxPair1|split; [|split]]
| [ _ : red (lessen _ ?a) ?x |- ∃ _, red (Pair (S ?j) ?b (lessen _ ?a)) _ ∧ _ ] ⇒
    ∃ (Pair j b x); simpl; split; [apply RedCtxPair2|split; [|split]]
| [ _ : red (lessen _ ?a) ?x |- ∃ _, red (Fst (S ?j) (lessen _ ?a)) _ ∧ _ ] ⇒
    ∃ (Fst j x); simpl; split; [apply RedCtxFst|]
  | [ _ : red (lessen _ ?a) ?x |- ∃ _, red (Snd (S ?j) (lessen _ ?a)) _ ∧ _ ] ⇒
    ∃ (Snd j x); simpl; split; [apply RedCtxSnd|]
end; auto; try (apply le_term_lessen; auto; apply binary_fuel_refl; auto));
eexists;
[ split; [apply RedApp|]
| split; [apply RedFst|]
| split; [apply RedSnd|] ]; instantiate;
[rewrite subst_lessen; rewrite <- lessen_subst| |];
rewrite 2 lessen_lessen;
(apply le_term_lessen; [|apply binary_fuel_refl; auto]); minmax.
Qed.

Lemma term_le_lessen : ∀ a k, term_le a k → a = lessen k a.
Proof.
induction a; intros ? H; simpl in *;
repeat (match goal with
  | |- context [min _ _] ⇒ rewrite min_l
  | H1 : _ ∧ _ |- _ ⇒ destruct H1
  | IHa : ∀ _,_ → _ = _ |- _ ⇒ rewrite <- IHa; clear IHa
end; auto); auto.
Qed.

Lemma term_le_max : ∀ a k j, term_le a k → term_le a (max j k).
Proof.
intros; eapply unary_fuel_1; [|apply H]; instantiate; simpl; intros.
eapply le_trans; [apply H0|]; minmax.
Qed.

Lemma term_le_exists : ∀ a, ∃ k, term_le a k.
Proof.
induction a; repeat (match goal with
  | IHa : ∃ _, term_le _ _ |- _ ⇒ destruct IHa; clear IHa end).
∃ k; simpl; auto.
  ∃ (max k x); simpl; split; [minmax|].
  apply term_le_max; assumption.
  ∃ (max k (max x x0)); simpl; split; [|split].
  minmax.
  repeat (apply term_le_max); assumption.
  apply term_le_max; rewrite max_comm.
  apply term_le_max; assumption.
  ∃ (max k (max x x0)); simpl; split; [|split].
  apply le_max_l.
  repeat (apply term_le_max); assumption.
  apply term_le_max; rewrite max_comm.
  apply term_le_max; assumption.
  ∃ (max k x); simpl; split.
  apply le_max_l.
  apply term_le_max; assumption.
  ∃ (max k x); simpl; split.
  apply le_max_l.
  apply term_le_max; assumption.
Qed.

Lemma term_lt_exists : ∀ a, ∃ k, term_lt a k.
Proof.
intros a; destruct (term_le_exists a).
∃ (1 + x).
eapply unary_fuel_1; [|apply H].
simpl; intros j ?; omega.
Qed.

Lemma term_le_min : ∀ a k j, term_le a j → term_le a k → term_le a (min j k).
Proof.
intros a k j aj ak; eapply unary_fuel_2; [|apply aj|apply ak]; instantiate; simpl; intros.
apply min_glb; assumption.
Qed.

Lemma term_lt_min : ∀ a k j, term_lt a j → term_lt a k → term_lt a (min j k).
Proof.
intros a k j aj ak; eapply unary_fuel_2; [|apply aj|apply ak]; instantiate; simpl; intros.
apply min_glb; assumption.
Qed.

Lemma binary_fuel_unary : ∀ (op : nat → nat → Prop) (f : nat → Prop),
  (∀ j k, op j k → f k → f j) →
  ∀ a b, binary_fuel op a b → unary_fuel f b → unary_fuel f a.
Proof.
intros op f opf; induction a; intros b ab fb; destruct_binary b ab; subst; simpl in *;
repeat (match goal with
  | H : _ ∧ _ |- _ ⇒ destruct H
  | |- _ ∧ _ ⇒ split
  | Hop : op ?j ?k, Hf : f ?k |- f ?j ⇒ apply (opf _ _ Hop Hf)
  | IHa : ∀ _, _ → _ → _ _ ?a
    , Hop : binary_fuel op ?a ?b
    , Hf : unary_fuel f ?b
    |- unary_fuel f ?a ⇒ apply (IHa b Hop Hf)
end; auto); auto.
Qed.

Lemma le_term_le : ∀ a b k, le_term a b → term_le b k → term_le a k.
Proof.
intros a b k ab bk; eapply binary_fuel_unary; [|apply ab|apply bk].
intros; omega.
Qed.

Lemma le_term_lt : ∀ a b k, le_term a b → term_lt b k → term_lt a k.
Proof.
intros a b k ab bk; eapply binary_fuel_unary; [|apply ab|apply bk].
intros; omega.
Qed.

Lemma lt_term_le : ∀ a j k, term_lt a j → j ≤ k → term_lt a k.
Proof.
intros a j k aj jk; eapply unary_fuel_1; [|apply aj].
simpl; intros; omega.
Qed.

Lemma term_lt_0 : ∀ a, term_lt a 0 → False.
Proof.
destruct a; simpl; intros; repeat
match goal with
  | H : _ ∧ _ |- _ ⇒ destruct H
  | H : ?k < 0 |- _ ⇒ inversion H
end.
Qed.