# 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 : natnat) := fix g a :=
match a with
| Var k xVar (f k) x
| Lam k aLam (f k) (g a)
| App k a bApp (f k) (g a) (g b)
| Pair k a bPair (f k) (g a) (g b)
| Fst k aFst (f k) (g a)
| Snd k aSnd (f k) (g a)

end.

Definition unary_fuel f := fix g a :=
match a with
| Var k xf k
| Lam k af k g a
| App k a bf k g a g b
| Pair k a bf k g a g b
| Fst k af k g a
| Snd k af k g a

end.

Definition binary_fuel f := fix g a b :=
match a, b with
| Var j x, Var k yf j k x = y
| Lam j a, Lam k bf j k g a b
| App j a1 a2, App k b1 b2f j k g a1 b1 g a2 b2
| Pair j a1 a2, Pair k b1 b2f j k g a1 b1 g a2 b2
| Fst j a, Fst k bf j k g a b
| Snd j a, Snd k bf j k g a b

| _, _False
end.

Definition lessen k := map_fuel (fun jmin j k).
Definition le_term := binary_fuel le.
Definition term_le a k := unary_fuel (fun jj k) a.
Definition term_lt a k := unary_fuel (fun jj < k) a.
Definition term_ge a k := unary_fuel (fun jj 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 xf k x i
| Lam k aLam k (g (1 + i) a)
| App k a bApp k (g i a) (g i b)
| Pair k a bPair k (g i a) (g i b)
| Fst k aFst k (g i a)
| Snd k aSnd 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 : termtermProp :=
| 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 aN aFalse.
Proof. destruct a; auto. Qed.

Inductive Err : set :=
| ErrCtxLam : k e, Err eErr (Lam k e)
| ErrCtxApp1 : k e a, Err eErr (App k e a)
| ErrCtxApp2 : k e a, Err eErr (App k a e)
| ErrCtxPair1 : k e a, Err eErr (Pair k e a)
| ErrCtxPair2 : k e a, Err eErr (Pair k a e)
| ErrCtxFst : k e, Err eErr (Fst k e)
| ErrCtxSnd : k e, Err eErr (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 aV (Lam k a).
Proof. intros k a H Herr; inversion Herr; auto. Qed.

Lemma V_Pair : {k a b}, V aV bV (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 : natProp), ( j, f jg j) →
a, unary_fuel f aunary_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 : natProp), ( j, f1 jf2 jg j) →
a, unary_fuel f1 aunary_fuel f2 aunary_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 : natProp) upd,
( k, f kf (upd k)) →
a, unary_fuel f aunary_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 : natProp) 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 : natnatProp) upd' upd,
( k' k, op k' kop (upd' k') (upd k)) →
a' a, binary_fuel op a' abinary_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 : natnatProp) 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 : natnatProp),
( k1 k2 k3, op k1 k2op k2 k3op k1 k3) →
a1 a2 a3, binary_fuel op a1 a2binary_fuel op a2 a3binary_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 : natnatProp),
( 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' kle_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' ble_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' ared 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 kterm_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 : natProp) g, ( k x i, f kunary_fuel f (g k x i)) →
a i, unary_fuel f aunary_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 aunary_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 kterm_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 : natProp), ( j k, f jf kf (min j k)) →
a b i, unary_fuel f aunary_fuel f bunary_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 kterm_ge b kterm_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 : natProp),
( k, f (S k) → g k) → ( k, f kg k) → ( j k, g jg kg (min j k)) →
a b, red a bunary_fuel f aunary_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 ?aapply 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 bterm_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 bterm_le a kterm_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 bFalse.
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 bterm_lt a kterm_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 ka = 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 kterm_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 jterm_le a kterm_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 jterm_lt a kterm_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 : natnatProp) (f : natProp),
( j k, op j kf kf j) →
a b, binary_fuel op a bunary_fuel f bunary_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 ?japply (opf _ _ Hop Hf)
| IHa : _, ___ _ ?a
, Hop : binary_fuel op ?a ?b
, Hf : unary_fuel f ?b
|- unary_fuel f ?aapply (IHa b Hop Hf)
end; auto); auto.
Qed.

Lemma le_term_le : a b k, le_term a bterm_le b kterm_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 bterm_lt b kterm_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 jj kterm_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.