Library Llanguage
Require Import Omega.
Require Import Min.
Require Import Max.
Require Import set.
Require Import Flanguage.
Inductive term : Set :=
| Var (x : nat)
| Lam (a : term)
| App (a : term) (b : term)
| Pair (a : term) (b : term)
| Fst (a : term)
| Snd (a : term)
.
Definition Var_x := Var.
Hint Unfold Var_x.
Definition traverse f := fix g i a :=
match a with
| Var x ⇒ f x i
| Lam a ⇒ Lam (g (1 + i) a)
| App a b ⇒ App (g i a) (g i b)
| Pair a b ⇒ Pair (g i a) (g i b)
| Fst a ⇒ Fst (g i a)
| Snd a ⇒ Snd (g i a)
end.
Definition lift_idx d x i := Var (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 x i :=
match lt_eq_lt_dec x i with
| inleft (left _) ⇒ Var x
| inleft (right _) ⇒ lift x 0 b
| inright _ ⇒ Var (x - 1)
end.
Definition subst b := traverse (subst_idx b).
Hint Unfold subst_idx subst.
Fixpoint drop a :=
match a with
| Flanguage.Var _ x ⇒ Var x
| Flanguage.Lam _ a ⇒ Lam (drop a)
| Flanguage.App _ a b ⇒ App (drop a) (drop b)
| Flanguage.Pair _ a b ⇒ Pair (drop a) (drop b)
| Flanguage.Fst _ a ⇒ Fst (drop a)
| Flanguage.Snd _ a ⇒ Snd (drop a)
end.
Lemma drop_lessen : ∀ k a, drop (lessen k a) = drop a.
Proof.
induction a; simpl;
repeat (match goal with
| IH : drop (lessen _ _) = _ |- _ ⇒ rewrite IH; clear IH
end); auto.
Qed.
Lemma drop_lift : ∀ x a i, drop (Flanguage.lift x i a) = lift x i (drop a).
Proof.
induction a; simpl; intros i;
repeat (match goal with
| IH : ∀ _, drop (Flanguage.lift _ _ _) = _ |- _ ⇒ rewrite IH; clear IH
end); auto.
Qed.
Lemma drop_subst : ∀ b a i, drop (Flanguage.subst b i a) = subst (drop b) i (drop a).
Proof.
induction a; simpl; intros i;
repeat (match goal with
| IH : ∀ _, drop (Flanguage.subst _ _ _) = _ |- _ ⇒ rewrite IH; clear IH
end); auto.
subst_lift_var; unfold subst_idx;
destruct (lt_eq_lt_dec x i) as [[?|?]|?]; try (exfalso; omega); auto.
rewrite drop_lessen.
apply drop_lift.
Qed.
Definition fill k := fix f a :=
match a with
| Var x ⇒ Flanguage.Var k x
| Lam a ⇒ Flanguage.Lam k (f a)
| App a b ⇒ Flanguage.App k (f a) (f b)
| Pair a b ⇒ Flanguage.Pair k (f a) (f b)
| Fst a ⇒ Flanguage.Fst k (f a)
| Snd a ⇒ Flanguage.Snd k (f a)
end.
Lemma term_ge_fill : ∀ k a, term_ge (fill k a) k.
Proof. induction a; simpl; auto. Qed.
Lemma drop_fill : ∀ k a, drop (fill k a) = a.
Proof. induction a; simpl; f_equal; auto. Qed.
Definition set := @set.set term.
Inductive red : term → term → Prop :=
| RedCtxLam : ∀ a a', red a a' → red (Lam a) (Lam a')
| RedCtxApp1 : ∀ a b a', red a a' → red (App a b) (App a' b)
| RedCtxApp2 : ∀ a b b', red b b' → red (App a b) (App a b')
| RedCtxPair1 : ∀ a b a', red a a' → red (Pair a b) (Pair a' b)
| RedCtxPair2 : ∀ a b b', red b b' → red (Pair a b) (Pair a b')
| RedCtxFst : ∀ a a', red a a' → red (Fst a) (Fst a')
| RedCtxSnd : ∀ a a', red a a' → red (Snd a) (Snd a')
| RedApp : ∀ a b, red (App (Lam a) b) (subst b 0 a)
| RedFst : ∀ a b, red (Fst (Pair a b)) a
| RedSnd : ∀ a b, red (Snd (Pair a b)) b
.
Lemma red_drop : ∀ a b, Flanguage.red a b → red (drop a) (drop b).
Proof.
intros a b Hred; induction Hred; simpl in *;
repeat (match goal with | H : _ ∧ _ |- _ ⇒ destruct H end);
auto using red.
rewrite drop_lessen; rewrite drop_subst; apply RedApp.
rewrite drop_lessen; apply RedFst.
rewrite drop_lessen; apply RedSnd.
Qed.
Lemma drop_red_exists : ∀ k a b', term_ge a (1 + k) → red (drop a) b' →
∃ b, b' = drop b ∧ Flanguage.red a b.
Proof.
intros k a b' ak Hred; remember (drop a) as a'.
generalize a ak Heqa'; clear a ak Heqa'; induction Hred; try (rename a into a0); intros a ak Heqa';
destruct a; inversion Heqa'; simpl in ak; subst;
[repeat (match goal with
| H : ?k ≥ S _ |- _ ⇒ is_var k; destruct k; [inversion H|]
| H : _ ∧ _ |- _ ⇒ destruct H
| H : term_ge ?a (S k),
IH : ∀ _, _ → drop ?a = _ → _
|- _ ⇒ destruct (IH a H eq_refl) as [? [? ?]]; clear IH
end); subst; eexists; split; [|eauto using Flanguage.red]; instantiate; simpl; auto..| | |].
inversion Heqa'; destruct a1; inversion H1; subst.
destruct ak as [? [[? ?] ?]]; destruct k0; [inversion H|]; destruct k1; [inversion H2|].
∃ (lessen (min k0 k1) (Flanguage.subst a2 0 a1)); simpl; split; auto using Flanguage.red.
rewrite <- drop_subst; rewrite drop_lessen; reflexivity.
destruct a; inversion H0; subst.
destruct ak as [? [? ?]]; destruct k0; [inversion H|]; destruct k1; [inversion H1|].
∃ (lessen (min k0 k1) a1); simpl; split; auto using Flanguage.red.
rewrite drop_lessen; reflexivity.
destruct a; inversion H0; subst.
destruct ak as [? [? ?]]; destruct k0; [inversion H|]; destruct k1; [inversion H1|].
∃ (lessen (min k0 k1) a2); simpl; split; auto using Flanguage.red.
rewrite drop_lessen; reflexivity.
Qed.
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.
Lemma N_drop : ∀ a, Flanguage.N a ↔ N (drop a).
Proof. induction a; split; intros Ha; simpl; auto. Qed.
Inductive Err : set :=
| ErrCtxLam : ∀ e, Err e → Err (Lam e)
| ErrCtxApp1 : ∀ e a, Err e → Err (App e a)
| ErrCtxApp2 : ∀ e a, Err e → Err (App a e)
| ErrCtxPair1 : ∀ e a, Err e → Err (Pair e a)
| ErrCtxPair2 : ∀ e a, Err e → Err (Pair a e)
| ErrCtxFst : ∀ e, Err e → Err (Fst e)
| ErrCtxSnd : ∀ e, Err e → Err (Snd e)
| ErrApp : ∀ a1 a2 b, Err (App (Pair a1 a2) b)
| ErrFst : ∀ a, Err (Fst (Lam a))
| ErrSnd : ∀ a, Err (Snd (Lam a))
.
Lemma Err_drop : ∀ a, Flanguage.Err a ↔ Err (drop a).
Proof.
split; induction a; intros Ha; inversion Ha; subst; simpl in *; auto using Err, Flanguage.Err.
destruct a1; inversion H0; subst; apply Flanguage.ErrApp.
destruct a; inversion H0; subst; apply Flanguage.ErrFst.
destruct a; inversion H0; subst; apply Flanguage.ErrSnd.
Qed.
Definition V : set := Cmp Err.
Hint Unfold V.
Lemma V_drop : ∀ a, Flanguage.V a ↔ V (drop a).
Proof. induction a; split; intros Ha Erra; apply Err_drop in Erra; auto. Qed.
Inductive SN : set := SN_ : ∀ a, (∀ b, red a b → SN b) → SN a.
Lemma ExpSN : ∀ a, SN a → ∀ b, red a b → SN b.
Proof. intros; destruct H; auto. 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 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].
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.
replace (subst bd d) with (subst bd (d + 0)) by (f_equal; omega).
rewrite lift_subst; f_equal; omega.
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 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 subst_subst_0; apply RedApp.
Qed.
Fixpoint value v a :=
match a with
| Var _ ⇒ True
| Lam a ⇒ v ∧ value True a
| App a b ⇒ value False a ∧ value True b
| Pair a b ⇒ v ∧ value True a ∧ value True b
| Fst a ⇒ value False a
| Snd a ⇒ value False a
end.
Definition irred a := ∀ b, red a b → False.
Lemma prevalue_is_value : ∀ a, value False a → value True a.
Proof.
induction a; simpl; intros; auto;
repeat (match goal with
| H1 : _ ∧ _ |- _ ⇒ destruct H1
end; auto).
Qed.
Lemma CNvalue_is_prevalue : ∀ a, value True a → N a → value False a.
Proof.
induction a; simpl; intros; auto;
repeat (match goal with
| H1 : _ ∧ _ |- _ ⇒ destruct H1
end; auto).
Qed.
Ltac progre_aux :=
match goal with
| |- irred _ ⇒ intros b Hred;
match goal with
| H1 : irred ?Ta , H2 : red ?a ?b
|- _ ⇒ match Ta with context f[a] ⇒ let x := context f[b] in apply (H1 x) end
end; auto using red
| H1 : V _ |- V _ ⇒ intros Erra; apply H1; auto using Err
end.
Lemma progre : ∀ a, irred a → V a → value True a.
Proof.
induction a; intros ia Va; repeat split; auto.
apply IHa; progre_aux.
apply CNvalue_is_prevalue; [apply IHa1; progre_aux|].
destruct a1; simpl; auto.
eapply ia; auto using red.
apply Va; auto using Err.
apply IHa2; progre_aux.
apply IHa1; progre_aux.
apply IHa2; progre_aux.
apply CNvalue_is_prevalue; [apply IHa; progre_aux|].
destruct a; simpl; auto.
apply Va; auto using Err.
eapply ia; auto using red.
apply CNvalue_is_prevalue; [apply IHa; progre_aux|].
destruct a; simpl; auto.
apply Va; auto using Err.
eapply ia; auto using red.
Qed.
Lemma irred_value : ∀ a, value True a → irred a.
Proof.
intros a vala b Hred.
induction Hred; simpl in *;
repeat (match goal with
| H1 : _ ∧ _ |- _ ⇒ destruct H1
| H1 : value False ?a
, Hx : value True ?a → _
|- _ ⇒ pose proof (Hx (prevalue_is_value a H1)); clear Hx
end; auto).
Qed.
Lemma V_value : ∀ a, value True a → V a.
Proof.
intros a vala Erra.
induction Erra; simpl in *;
repeat (match goal with
| H1 : _ ∧ _ |- _ ⇒ destruct H1
| H1 : value False ?a
, Hx : value True ?a → _
|- _ ⇒ pose proof (Hx (prevalue_is_value a H1)); clear Hx
end; auto).
Qed.
Require Import Min.
Require Import Max.
Require Import set.
Require Import Flanguage.
Inductive term : Set :=
| Var (x : nat)
| Lam (a : term)
| App (a : term) (b : term)
| Pair (a : term) (b : term)
| Fst (a : term)
| Snd (a : term)
.
Definition Var_x := Var.
Hint Unfold Var_x.
Definition traverse f := fix g i a :=
match a with
| Var x ⇒ f x i
| Lam a ⇒ Lam (g (1 + i) a)
| App a b ⇒ App (g i a) (g i b)
| Pair a b ⇒ Pair (g i a) (g i b)
| Fst a ⇒ Fst (g i a)
| Snd a ⇒ Snd (g i a)
end.
Definition lift_idx d x i := Var (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 x i :=
match lt_eq_lt_dec x i with
| inleft (left _) ⇒ Var x
| inleft (right _) ⇒ lift x 0 b
| inright _ ⇒ Var (x - 1)
end.
Definition subst b := traverse (subst_idx b).
Hint Unfold subst_idx subst.
Fixpoint drop a :=
match a with
| Flanguage.Var _ x ⇒ Var x
| Flanguage.Lam _ a ⇒ Lam (drop a)
| Flanguage.App _ a b ⇒ App (drop a) (drop b)
| Flanguage.Pair _ a b ⇒ Pair (drop a) (drop b)
| Flanguage.Fst _ a ⇒ Fst (drop a)
| Flanguage.Snd _ a ⇒ Snd (drop a)
end.
Lemma drop_lessen : ∀ k a, drop (lessen k a) = drop a.
Proof.
induction a; simpl;
repeat (match goal with
| IH : drop (lessen _ _) = _ |- _ ⇒ rewrite IH; clear IH
end); auto.
Qed.
Lemma drop_lift : ∀ x a i, drop (Flanguage.lift x i a) = lift x i (drop a).
Proof.
induction a; simpl; intros i;
repeat (match goal with
| IH : ∀ _, drop (Flanguage.lift _ _ _) = _ |- _ ⇒ rewrite IH; clear IH
end); auto.
Qed.
Lemma drop_subst : ∀ b a i, drop (Flanguage.subst b i a) = subst (drop b) i (drop a).
Proof.
induction a; simpl; intros i;
repeat (match goal with
| IH : ∀ _, drop (Flanguage.subst _ _ _) = _ |- _ ⇒ rewrite IH; clear IH
end); auto.
subst_lift_var; unfold subst_idx;
destruct (lt_eq_lt_dec x i) as [[?|?]|?]; try (exfalso; omega); auto.
rewrite drop_lessen.
apply drop_lift.
Qed.
Definition fill k := fix f a :=
match a with
| Var x ⇒ Flanguage.Var k x
| Lam a ⇒ Flanguage.Lam k (f a)
| App a b ⇒ Flanguage.App k (f a) (f b)
| Pair a b ⇒ Flanguage.Pair k (f a) (f b)
| Fst a ⇒ Flanguage.Fst k (f a)
| Snd a ⇒ Flanguage.Snd k (f a)
end.
Lemma term_ge_fill : ∀ k a, term_ge (fill k a) k.
Proof. induction a; simpl; auto. Qed.
Lemma drop_fill : ∀ k a, drop (fill k a) = a.
Proof. induction a; simpl; f_equal; auto. Qed.
Definition set := @set.set term.
Inductive red : term → term → Prop :=
| RedCtxLam : ∀ a a', red a a' → red (Lam a) (Lam a')
| RedCtxApp1 : ∀ a b a', red a a' → red (App a b) (App a' b)
| RedCtxApp2 : ∀ a b b', red b b' → red (App a b) (App a b')
| RedCtxPair1 : ∀ a b a', red a a' → red (Pair a b) (Pair a' b)
| RedCtxPair2 : ∀ a b b', red b b' → red (Pair a b) (Pair a b')
| RedCtxFst : ∀ a a', red a a' → red (Fst a) (Fst a')
| RedCtxSnd : ∀ a a', red a a' → red (Snd a) (Snd a')
| RedApp : ∀ a b, red (App (Lam a) b) (subst b 0 a)
| RedFst : ∀ a b, red (Fst (Pair a b)) a
| RedSnd : ∀ a b, red (Snd (Pair a b)) b
.
Lemma red_drop : ∀ a b, Flanguage.red a b → red (drop a) (drop b).
Proof.
intros a b Hred; induction Hred; simpl in *;
repeat (match goal with | H : _ ∧ _ |- _ ⇒ destruct H end);
auto using red.
rewrite drop_lessen; rewrite drop_subst; apply RedApp.
rewrite drop_lessen; apply RedFst.
rewrite drop_lessen; apply RedSnd.
Qed.
Lemma drop_red_exists : ∀ k a b', term_ge a (1 + k) → red (drop a) b' →
∃ b, b' = drop b ∧ Flanguage.red a b.
Proof.
intros k a b' ak Hred; remember (drop a) as a'.
generalize a ak Heqa'; clear a ak Heqa'; induction Hred; try (rename a into a0); intros a ak Heqa';
destruct a; inversion Heqa'; simpl in ak; subst;
[repeat (match goal with
| H : ?k ≥ S _ |- _ ⇒ is_var k; destruct k; [inversion H|]
| H : _ ∧ _ |- _ ⇒ destruct H
| H : term_ge ?a (S k),
IH : ∀ _, _ → drop ?a = _ → _
|- _ ⇒ destruct (IH a H eq_refl) as [? [? ?]]; clear IH
end); subst; eexists; split; [|eauto using Flanguage.red]; instantiate; simpl; auto..| | |].
inversion Heqa'; destruct a1; inversion H1; subst.
destruct ak as [? [[? ?] ?]]; destruct k0; [inversion H|]; destruct k1; [inversion H2|].
∃ (lessen (min k0 k1) (Flanguage.subst a2 0 a1)); simpl; split; auto using Flanguage.red.
rewrite <- drop_subst; rewrite drop_lessen; reflexivity.
destruct a; inversion H0; subst.
destruct ak as [? [? ?]]; destruct k0; [inversion H|]; destruct k1; [inversion H1|].
∃ (lessen (min k0 k1) a1); simpl; split; auto using Flanguage.red.
rewrite drop_lessen; reflexivity.
destruct a; inversion H0; subst.
destruct ak as [? [? ?]]; destruct k0; [inversion H|]; destruct k1; [inversion H1|].
∃ (lessen (min k0 k1) a2); simpl; split; auto using Flanguage.red.
rewrite drop_lessen; reflexivity.
Qed.
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.
Lemma N_drop : ∀ a, Flanguage.N a ↔ N (drop a).
Proof. induction a; split; intros Ha; simpl; auto. Qed.
Inductive Err : set :=
| ErrCtxLam : ∀ e, Err e → Err (Lam e)
| ErrCtxApp1 : ∀ e a, Err e → Err (App e a)
| ErrCtxApp2 : ∀ e a, Err e → Err (App a e)
| ErrCtxPair1 : ∀ e a, Err e → Err (Pair e a)
| ErrCtxPair2 : ∀ e a, Err e → Err (Pair a e)
| ErrCtxFst : ∀ e, Err e → Err (Fst e)
| ErrCtxSnd : ∀ e, Err e → Err (Snd e)
| ErrApp : ∀ a1 a2 b, Err (App (Pair a1 a2) b)
| ErrFst : ∀ a, Err (Fst (Lam a))
| ErrSnd : ∀ a, Err (Snd (Lam a))
.
Lemma Err_drop : ∀ a, Flanguage.Err a ↔ Err (drop a).
Proof.
split; induction a; intros Ha; inversion Ha; subst; simpl in *; auto using Err, Flanguage.Err.
destruct a1; inversion H0; subst; apply Flanguage.ErrApp.
destruct a; inversion H0; subst; apply Flanguage.ErrFst.
destruct a; inversion H0; subst; apply Flanguage.ErrSnd.
Qed.
Definition V : set := Cmp Err.
Hint Unfold V.
Lemma V_drop : ∀ a, Flanguage.V a ↔ V (drop a).
Proof. induction a; split; intros Ha Erra; apply Err_drop in Erra; auto. Qed.
Inductive SN : set := SN_ : ∀ a, (∀ b, red a b → SN b) → SN a.
Lemma ExpSN : ∀ a, SN a → ∀ b, red a b → SN b.
Proof. intros; destruct H; auto. 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 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].
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.
replace (subst bd d) with (subst bd (d + 0)) by (f_equal; omega).
rewrite lift_subst; f_equal; omega.
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 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 subst_subst_0; apply RedApp.
Qed.
Fixpoint value v a :=
match a with
| Var _ ⇒ True
| Lam a ⇒ v ∧ value True a
| App a b ⇒ value False a ∧ value True b
| Pair a b ⇒ v ∧ value True a ∧ value True b
| Fst a ⇒ value False a
| Snd a ⇒ value False a
end.
Definition irred a := ∀ b, red a b → False.
Lemma prevalue_is_value : ∀ a, value False a → value True a.
Proof.
induction a; simpl; intros; auto;
repeat (match goal with
| H1 : _ ∧ _ |- _ ⇒ destruct H1
end; auto).
Qed.
Lemma CNvalue_is_prevalue : ∀ a, value True a → N a → value False a.
Proof.
induction a; simpl; intros; auto;
repeat (match goal with
| H1 : _ ∧ _ |- _ ⇒ destruct H1
end; auto).
Qed.
Ltac progre_aux :=
match goal with
| |- irred _ ⇒ intros b Hred;
match goal with
| H1 : irred ?Ta , H2 : red ?a ?b
|- _ ⇒ match Ta with context f[a] ⇒ let x := context f[b] in apply (H1 x) end
end; auto using red
| H1 : V _ |- V _ ⇒ intros Erra; apply H1; auto using Err
end.
Lemma progre : ∀ a, irred a → V a → value True a.
Proof.
induction a; intros ia Va; repeat split; auto.
apply IHa; progre_aux.
apply CNvalue_is_prevalue; [apply IHa1; progre_aux|].
destruct a1; simpl; auto.
eapply ia; auto using red.
apply Va; auto using Err.
apply IHa2; progre_aux.
apply IHa1; progre_aux.
apply IHa2; progre_aux.
apply CNvalue_is_prevalue; [apply IHa; progre_aux|].
destruct a; simpl; auto.
apply Va; auto using Err.
eapply ia; auto using red.
apply CNvalue_is_prevalue; [apply IHa; progre_aux|].
destruct a; simpl; auto.
apply Va; auto using Err.
eapply ia; auto using red.
Qed.
Lemma irred_value : ∀ a, value True a → irred a.
Proof.
intros a vala b Hred.
induction Hred; simpl in *;
repeat (match goal with
| H1 : _ ∧ _ |- _ ⇒ destruct H1
| H1 : value False ?a
, Hx : value True ?a → _
|- _ ⇒ pose proof (Hx (prevalue_is_value a H1)); clear Hx
end; auto).
Qed.
Lemma V_value : ∀ a, value True a → V a.
Proof.
intros a vala Erra.
induction Erra; simpl in *;
repeat (match goal with
| H1 : _ ∧ _ |- _ ⇒ destruct H1
| H1 : value False ?a
, Hx : value True ?a → _
|- _ ⇒ pose proof (Hx (prevalue_is_value a H1)); clear Hx
end; auto).
Qed.