Library Fsemantics

Require Import Omega.
Require Import Min.
Require Import List.

Require Import ext.
Require Import set.
Require Import minmax.
Require Import Flanguage.
Require Import Fnormalization.

Definition Dec (R : set) : set := fun b ⇒ ∃ a, R a ∧ le_term b a.
Hint Unfold Dec.

Definition Red (R : set) : set := fun b ⇒ ∃ a, R a ∧ red a b.
Hint Unfold Red.

Definition Exp (P : set) (R : set) : set := fun a ⇒ P a ∧ ∀ b, red a b → R b.
Hint Unfold Exp.

Ltac Exp := let Hred := fresh "Hred" in split; [|intros ? Hred; inversion Hred].

Definition ExpFix (P : set) (a : term) (R : ∀ b, red a b → Prop) : Prop :=
  P a ∧ ∀ b (H : red a b), R b H.

Lemma DecN : Inc (Dec N) N.
Proof.
intros b [a [Na ba]].
destruct b; destruct a; simpl in ba; try (exfalso; exact ba); try exact I; inversion Na.
Qed.

Lemma DecCN : Inc (Dec CN) CN.
Proof.
intros b [a [CNa ba]].
destruct b; destruct a; simpl in ba; try (exfalso; exact ba); try exact I; inversion CNa.
Qed.

Lemma RedCN : Inc (Red CN) CN.
Proof.
intros b [a [CNa Hred]].
inversion Hred; subst; inversion CNa; auto.
Qed.

Definition DecV : Inc (Dec V) V.
Proof.
intros b [a [Va ba]] Eb; apply Va; clear Va; generalize a ba Eb; clear a ba Eb.
induction b; intros a ba Eb; destruct_binary a ba; inversion Eb; subst; auto using Err.
destruct_binary a1 H0; apply ErrApp.
destruct_binary a H0; apply ErrFst.
destruct_binary a H0; apply ErrSnd.
Qed.

Lemma DecNV : Inc (Dec NV) NV.
Proof.
intros b [a [[Na Va] ba]].
split; [apply DecN|apply DecV]; ∃ a; auto.
Qed.

Definition OK : set := Fix _ (ExpFix V).

Lemma OK_def : OK = Exp V OK.
Proof.
apply extEq; split; intros a Ha.
  unfold OK, Fix in Ha.
  rewrite Init.Wf.Fix_eq in Ha; [exact Ha|intros].
  f_equal.
  apply functional_extensionality_dep; intros.
  apply functional_extensionality_dep; intros.
  apply H.
  unfold OK, Fix.
  rewrite Init.Wf.Fix_eq; [exact Ha|intros].
  f_equal.
  apply functional_extensionality_dep; intros.
  apply functional_extensionality_dep; intros.
  apply H.
Qed.

Lemma fold_OK : ∀ a, Exp V OK a → OK a.
Proof. intros; rewrite OK_def; auto. Qed.

Lemma unfold_OK : ∀ a, OK a → Exp V OK a.
Proof. intros; rewrite <- OK_def; auto. Qed.

Definition Cl (R : set) : set := Fix _ (fun a ClR ⇒ R a ∨ ExpFix NV a ClR).

Lemma Cl_def : ∀ R, Cl R = Union R (Exp NV (Cl R)).
Proof.
intros R; apply extEq; split; intros a Ha.
  unfold Cl, Fix in Ha.
  rewrite Init.Wf.Fix_eq in Ha; [exact Ha|intros].
  repeat f_equal.
  apply functional_extensionality_dep; intros.
  apply functional_extensionality_dep; intros.
  apply H.
  unfold Cl, Fix.
  rewrite Init.Wf.Fix_eq; [exact Ha|intros].
  repeat f_equal.
  apply functional_extensionality_dep; intros.
  apply functional_extensionality_dep; intros.
  apply H.
Qed.

Lemma fold_Cl : ∀ R a, (R a ∨ Exp NV (Cl R) a) → Cl R a.
Proof. intros; rewrite Cl_def; auto. Qed.

Lemma unfold_Cl : ∀ R a, Cl R a → (R a ∨ Exp NV (Cl R) a).
Proof. intros; rewrite Cl_def in H; auto. Qed.

Lemma Cl_monotone : ∀ (R S : set), (∀ a, R a → S a) → ∀ a, Cl R a → Cl S a.
Proof.
intros R S RS a.
induction_red a; rewrite Cl_def; intros [Ha|[NVa Expa]]; rewrite Cl_def; [left|right]; auto.
Qed.

Definition Pcn R := Inc R CN.
Definition Pok R := Inc R OK.
Definition Pdec R := Inc (Dec R) R.
Definition Pred R := Inc (Red R) R.
Definition Pexp R := Inc (Exp NV R) R.
Hint Unfold Pcn Pok Pdec Pred Pexp.

Record C (R : set) : Prop := C_ {
  Cok : Pok R ;
  Cdec : Pdec R ;
  Cred : Pred R }.
Arguments Cok [R] _ _ _.
Arguments Cdec [R] _ _ _.
Arguments Cred [R] _ _ _.

Record CT (R : set) : Prop := CT_ {
  CTcn : Pcn R ;
  CTok : Pok R ;
  CTdec : Pdec R ;
  CTred : Pred R }.
Arguments CTcn [R] _ _ _.
Arguments CTok [R] _ _ _.
Arguments CTdec [R] _ _ _.
Arguments CTred [R] _ _ _.

Record CE (R : set) : Prop := CE_ {
  CEok : Pok R ;
  CEdec : Pdec R ;
  CEred : Pred R ;
  CEexp : Pexp R }.
Arguments CEok [R] _ _ _.
Arguments CEdec [R] _ _ _.
Arguments CEred [R] _ _ _.
Arguments CEexp [R] _ _ _.

Lemma CT_CPcn : ∀ R, Pcn R → C R → CT R.
Proof.
intros R PR CR; apply CT_.
apply PR.
apply (Cok CR).
apply (Cdec CR).
apply (Cred CR).
Qed.

Lemma CE_CPexp : ∀ R, Pexp R → C R → CE R.
Proof.
intros R PR CR; apply CE_.
apply (Cok CR).
apply (Cdec CR).
apply (Cred CR).
apply PR.
Qed.

Lemma C_CT : ∀ {R}, CT R → C R.
Proof. intros ? [? ? ? ?]; apply C_; auto. Qed.

Lemma C_CE : ∀ {R}, CE R → C R.
Proof. intros ? [? ? ? ?]; apply C_; auto. Qed.

Lemma Pdec_OK : Pdec OK.
Proof.
intros b; intros [a [OKa ba]].
generalize b OKa ba; clear b OKa ba; induction_red a; intros b OKa ba.
rewrite OK_def in OKa; rewrite OK_def.
destruct OKa as [Va Expa].
split; [apply DecV; ∃ a; auto|intros b' redb].
destruct (le_term_red _ _ _ ba redb) as [a' [? ?]].
apply IHa with (b := a'); auto.
Qed.

Lemma Pred_OK : Pred OK.
Proof.
intros b [a [OKa Hred]].
rewrite OK_def in OKa.
destruct OKa as [_ Expa].
apply Expa; auto.
Qed.

Lemma Pexp_OK : Pexp OK.
Proof. intros a [[Na Va] Expa]; rewrite OK_def; auto. Qed.

Lemma OKV : ∀ a, OK a → V a.
Proof. intros a OKa; rewrite OK_def in OKa; destruct OKa; assumption. Qed.

Lemma Cv : ∀ {R a}, Pok R → R a → V a.
Proof. intros R a CR Ra; apply OKV; apply CR; assumption. Qed.

Lemma Pexp_Cl : ∀ R, Pexp (Cl R).
Proof. intros R a Ha; rewrite Cl_def; right; exact Ha. Qed.

Lemma C_Cl : ∀ {R}, C R → C (Cl R).
Proof.
intros R CR; apply C_.
  intros a; induction_red a.
  intros Cla; rewrite Cl_def in Cla.
  destruct Cla as [Pa|[[Na Va] Expa]].
apply (Cok CR); exact Pa.
    rewrite OK_def.
    split; [exact Va|intros b Hred].
    apply IHa; [|apply Expa]; assumption.
  intros b; induction_red b. intros [a [Cla ba]].
  rewrite Cl_def in Cla; rewrite Cl_def.
  destruct Cla as [Pa|[NVa Expa]]; [left|right].
    apply (Cdec CR); ∃ a; split; assumption.
    split; [apply DecNV; ∃ a; split; assumption|].
    intros; apply IHb; try assumption.
    destruct (le_term_red _ _ _ ba H) as [a0 [? ?]].
    ∃ a0; auto.
  intros b [a [Cla Hred]]; rewrite Cl_def in Cla.
  destruct Cla as [Pa|[[Na Va] Expa]]; auto.
  rewrite Cl_def; left; apply (Cred CR); ∃ a; auto.
Qed.

Lemma CE_Cl : ∀ {R}, C R → CE (Cl R).
Proof.
intros R CR.
pose proof (C_Cl CR) as [? ? ?].
apply CE_; auto.
apply Pexp_Cl.
Qed.

Lemma destruct_Cl_CN : ∀ R a, CN a → Cl R a → R a.
Proof.
intros R a CNa Ha; apply unfold_Cl in Ha as [Ha|[[Na _] _]]; auto.
exfalso; apply (CN_N a); auto.
Qed.

Lemma destruct_Cl_N : ∀ R a, Pcn R → N a → Cl R a → Exp NV (Cl R) a.
Proof.
intros R a PR Na Ha; apply unfold_Cl in Ha as [Ha|Expa]; auto.
exfalso; apply (CN_N a); auto.
Qed.

Lemma split_Cl : ∀ (R : set) a, (CN a → R a) → (N a → Exp NV (Cl R) a) → Cl R a.
Proof. intros R a H1 H2; destruct (N_dec a); apply fold_Cl; [left|right]; auto. Qed.

Lemma Cl_CE : ∀ R, CE R → Cl R = R.
Proof.
intros R CR; apply extEq; split; intros a Ha; [|rewrite Cl_def; left; auto].
generalize Ha; clear Ha; induction_red a; intros Ha.
destruct (N_dec a); [apply destruct_Cl_CN; auto|].
apply (CEexp CR).
repeat split; auto; [apply (Cv (Cok (C_Cl (C_CE CR)))); auto|].
intros b Hred.
apply IHa; auto.
apply (Cred (C_Cl (C_CE CR))).
∃ a; auto.
Qed.

Definition Lc R := Inter CN R.
Hint Unfold Lc.

Lemma CT_Lc : ∀ {Q}, C Q → CT (Lc Q).
Proof.
intros Q CQ; apply CT_.
intros a [? ?]; auto.
intros a [? ?]; apply (Cok CQ); auto.
  intros b [a [[? ?] ?]].
  split; [apply DecCN|apply (Cdec CQ)]; ∃ a; auto.
  intros b [a [[? ?] ?]].
  split; [apply RedCN|apply (Cred CQ)]; ∃ a; auto.
Qed.

Lemma Lc_Cl : ∀ R, CT R → Lc (Cl R) = R.
Proof.
intros R CR; apply extEq; split; intros a Ha.
  destruct Ha; apply destruct_Cl_CN; auto.
  split; [apply (CTcn CR); auto|].
  apply fold_Cl; left; auto.
Qed.

Lemma Cl_Lc : ∀ Q, CE Q → Cl (Lc Q) = Q.
Proof.
intros Q CQ; apply extEq; split; intros a.
  induction_red a; intros Ha.
  apply unfold_Cl in Ha as [[? ?]|[? ?]]; auto.
  apply (CEexp CQ); auto.
  induction_red a; intros Ha; apply split_Cl; intros; auto.
  pose proof (OKV a (CEok CQ a Ha)).
  repeat split; auto.
  intros b Hred.
  apply IHa; auto.
  apply (CEred CQ); ∃ a; auto.
Qed.

Definition PArr (R S : set) : set := fun lam ⇒
  ∃ k a, lam = Lam k a ∧ OK a ∧
  (k > 0 → ∀ b, R (lessen (k - 1) b) → S (lessen (k - 1) (subst b 0 a))).
Definition EArr (R S : set) : set := Cl (PArr R S).
Definition TArr (R S : set) : set := PArr (Cl R) (Cl S).
Hint Unfold PArr EArr TArr.

Definition PProd (R S : set) : set := fun pair ⇒
  ∃ k a b, pair = Pair k a b ∧ (OK a ∧ OK b) ∧
  (k > 0 → (R (lessen (k - 1) a) ∧ S (lessen (k - 1) b))).
Definition EProd (R S : set) : set := Cl (PProd R S).
Definition TProd (R S : set) : set := PProd (Cl R) (Cl S).
Hint Unfold PProd EProd TProd.

Lemma OK_Var : ∀ k n, OK (Var k n).
Proof. intros k n; rewrite OK_def; Exp; apply V_Var. Qed.

Lemma R_Var : ∀ {R k n}, Pexp R → R (Var k n).
Proof. intros R k n CR; apply CR; Exp; apply NV_Var. Qed.

Lemma OK_Lam : ∀ {k a}, OK a → OK (Lam k a).
Proof.
intros k a; induction_red a.
rewrite OK_def; intros [Va Expa].
Exp; [apply V_Lam; exact Va|subst].
apply Pdec_OK.
∃ (Lam (S k0) a'); split; [apply IHa; auto|].
simpl; split; auto.
apply binary_fuel_refl; auto.
Qed.

Lemma OK_Pair : ∀ {k a b}, OK a → OK b → OK (Pair k a b).
Proof.
intros k a; induction_red a; intros b; induction_red b.
intros OKa OKb; generalize OKa OKb; rewrite OK_def; intros [Va Expa] [Vb Expb].
Exp; [apply V_Pair; assumption|subst..]; apply Pdec_OK;
repeat (match goal with
  | |- Dec OK (Pair ?k ?a ?b) ⇒ ∃ (Pair (S k) a b)
  | |- _ ∧ _ ⇒ split
  | |- OK (Pair _ _ _) ⇒ first [apply IHa|apply IHb]
  | |- le_term _ _ ⇒ simpl; split; [|split]
  | |- le_term ?x ?x ⇒ apply binary_fuel_refl
end; auto).
Qed.

Lemma R_lessen : ∀ R a k, Pdec R → R a → R (lessen k a).
Proof.
intros R a k CR Ra.
apply CR.
∃ a; split; auto.
apply le_term_lessen_trivial.
Qed.

Lemma OK_subst_Var : ∀ a i x, OK (subst (Var 0 x) i a) → OK a.
Proof.
intros a; induction_red a; intros i x OKa.
apply fold_OK.
pose proof (unfold_OK _ OKa) as [Va Expa].
split; [apply V_subst_N with (b := Var 0 x) (i := i); simpl; auto|].
intros b Hred; eapply IHa; [assumption|].
apply Expa; apply red_subst; assumption.
Qed.

Lemma C_PArr : ∀ {R S}, C R → C S → C (PArr R S).
Proof.
intros R S CR CS.
apply C_.
  intros lam [k [a [Heq [Hok Hsub]]]]; subst.
  apply OK_Lam; auto.
  intros a' [lam [[k [a [Heq [Hok Hsub]]]] lea]]; subst.
  destruct_binary a' lea.
  rename k0 into k'; ∃ k'; ∃ a'; split; [reflexivity|split].
    apply Pdec_OK; ∃ a; auto.
    intros Hk' b Rb.
    rewrite lessen_subst; rewrite <- subst_lessen; rewrite <- lessen_subst.
    apply (Cdec CS); ∃ (lessen (k - 1) (subst (lessen (k' - 1) b) 0 a)).
    split; [apply Hsub; [omega|]|].
      rewrite lessen_lessen.
      rewrite Min.min_l; auto; omega.
      apply le_term_lessen; [omega|].
      apply le_term_subst; [apply binary_fuel_refl|]; auto.
  intros a' [lam [[k [a [Heq [Hok Hsub]]]] Hred]]; subst.
  inversion Hred; subst; rename a'0 into a', k0 into k.
  ∃ k; ∃ a'; split; [reflexivity|split].
    apply Pred_OK; ∃ a; auto.
    intros Hk b Rb.
    rewrite lessen_subst; rewrite <- subst_lessen; rewrite <- lessen_subst.
    destruct k; [inversion Hk|clear Hk]; simpl in ×.
    pose proof (red_subst _ _ (lessen k b) H2 0).
    pose proof (red_lessen _ _ k H) as [? [? ?]].
    rewrite <- minus_n_O in ×.
    apply (Cdec CS).
    ∃ x; split; auto.
    apply (Cred CS).
    eexists; split; [|eassumption].
    apply Hsub; [omega|].
    rewrite lessen_lessen.
    rewrite Min.min_l; auto; omega.
Qed.

Lemma Pcn_PArr : ∀ R S, Pcn (PArr R S).
Proof. intros R S lam [k [a [Heq _]]]; subst; exact I. Qed.

Lemma CT_TArr : ∀ {R S}, C R → C S → CT (TArr R S).
Proof.
intros; apply CT_CPcn.
apply Pcn_PArr.
apply C_PArr; apply C_Cl; auto.
Qed.

Lemma CE_EArr : ∀ {R S}, C R → C S → CE (EArr R S).
Proof.
intros; apply CE_Cl.
apply C_PArr; auto.
Qed.

Lemma Push_right_Arr : ∀ R' S' R S, C S' → Pexp R → Inc (EArr R' S') (EArr R S) → Inc S' S.
Proof.
intros R' S' R S CS' CR Hinc a S'a.
destruct (term_le_exists a) as [k ak].
remember (Lam (1 + k) (shift 0 a)) as a'.
assert (EArr R S a').
- apply Hinc.
  subst; apply fold_Cl; left.
  ∃ (1 + k), (shift 0 a); repeat split; auto.
    apply OK_subst_Var with 0 0.
    unfold shift; rewrite subst_lift_0.
    apply (Cok CS'); auto.
  simpl; intros Hk b Rb; rewrite <- minus_n_O in ×.
  unfold shift; rewrite subst_lift_0.
  apply (Cdec CS'); ∃ a; repeat split; auto.
  apply le_term_lessen_trivial.
- subst.
  unfold EArr in H; apply destruct_Cl_CN in H; simpl; auto.
  destruct H as [? [? [Heq [Hok Hsub]]]]; inversion Heq; clear Heq; subst.
  simpl in *; rewrite <- minus_n_O in ×.
  rewrite (term_le_lessen a k); auto.
  unfold shift in Hsub; rewrite <- (subst_lift_0 a (Var 0 0)).
  apply Hsub; try omega.
  apply R_Var.
  apply CR.
Qed.

Lemma C_PProd : ∀ {R S}, C R → C S → C (PProd R S).
Proof.
intros R S CR CS.
apply C_.
  intros pair [k [a [b [Heq [[Hoka Hokb] Hproj]]]]]; subst.
  apply OK_Pair; auto.
  intros a' [pair [[k [a [b [Heq [[Hoka Hokb] Hproj]]]]] lea]]; subst.
  destruct_binary a' lea.
  rename k0 into k', a'1 into a', a'2 into b'; ∃ k'; ∃ a'; ∃ b';
  split; [reflexivity|split].
split; apply Pdec_OK; [∃ a|∃ b]; split; auto.
    intros Hk'; assert (k > 0) as Hk by omega; destruct (Hproj Hk).
    split; [apply (Cdec CR); ∃ (lessen (k - 1) a)|apply (Cdec CS); ∃ (lessen (k - 1) b)];
    split; auto; apply le_term_lessen; first [omega|auto].
  intros a' [pair [[k [a [b [Heq [[Hoka Hokb] Hproj]]]]] Hred]]; subst.
  inversion Hred; subst; [rename a'0 into a'|]; rename k0 into k;
  ∃ k; [∃ a'; ∃ b|∃ a; ∃ b']; (split; [reflexivity|split]).
      split; auto; apply Pred_OK; ∃ a; split; auto.
      intros Hk; assert (1 + k > 0) as Hk' by omega; destruct (Hproj Hk').
      destruct k; [inversion Hk|clear Hk]; simpl in *; rewrite <- minus_n_O.
      split; [apply (Cdec CR)|apply (Cdec CS)].
        pose proof (red_lessen _ _ k H3) as [? [? ?]].
        ∃ x; split; auto.
        apply (Cred CR); eexists; eauto.
        ∃ (lessen (1 + k) b); split; auto.
        apply le_term_lessen; auto.
        apply binary_fuel_refl; auto.
      split; auto; apply Pred_OK; ∃ b; split; auto.
      intros Hk; assert (1 + k > 0) as Hk' by omega; destruct (Hproj Hk').
      destruct k; [inversion Hk|clear Hk]; simpl in *; rewrite <- minus_n_O.
      split; [apply (Cdec CR)|apply (Cdec CS)].
        ∃ (lessen (1 + k) a); split; auto.
        apply le_term_lessen; auto.
        apply binary_fuel_refl; auto.
        pose proof (red_lessen _ _ k H3) as [? [? ?]].
        ∃ x; split; auto.
        apply (Cred CS); eexists; eauto.
Qed.

Lemma Pcn_PProd : ∀ R S, Pcn (PProd R S).
Proof. intros R S pair [k [a [b [Heq _]]]]; subst; exact I. Qed.

Lemma CT_TProd : ∀ {R S}, C R → C S → CT (TProd R S).
Proof.
intros; apply CT_CPcn.
apply Pcn_PProd.
apply C_PProd; apply C_Cl; auto.
Qed.

Lemma CE_EProd : ∀ {R S}, C R → C S → CE (EProd R S).
Proof.
intros; apply CE_Cl.
apply C_PProd; auto.
Qed.

Definition For I (cond : I → Prop) (func : ∀ i, cond i → set) : set := fun a ⇒
  ∀ i H, func i H a.
Definition For_preserve P := ∀ Ix cond func, (∃ i, cond i) →
  (∀ i H, P (func i H)) → P (For Ix cond func).
Hint Unfold For For_preserve.

Lemma C_For : For_preserve C.
Proof.
intros Ix cond func [wit cwit] Hfor; apply C_.
intros a Ha; apply (Cok (Hfor wit cwit)); apply Ha; apply cwit.
  intros a Ha i ci; apply (Cdec (Hfor i ci)).
  destruct Ha as [? [? ?]]; ∃ x; split; auto.
  intros b [a [Ha Hred]] i ci; apply (Cred (Hfor i ci)); ∃ a;
  split; [apply Ha; apply ci|apply Hred].
Qed.

Lemma Pcn_For : For_preserve Pcn.
Proof.
intros Ix cond func [wit cwit] Hfor a Ha.
apply (Hfor wit cwit a (Ha wit cwit)).
Qed.

Lemma CT_For : For_preserve CT.
Proof.
intros Ix cond func wit Hfor.
apply CT_CPcn.
apply Pcn_For; auto; intros; apply CTcn; auto.
apply C_For; auto; intros; apply C_CT; auto.
Qed.

Lemma Pexp_For : For_preserve Pexp.
Proof.
intros Ix cond func [wit cwit] Hfor a [NVa Expa] i ci.
apply (Hfor i ci); split; auto; intros b Hred.
apply (Expa b Hred i ci).
Qed.

Lemma CE_For : For_preserve CE.
Proof.
intros Ix cond func wit Hfor.
apply CE_CPexp.
apply Pexp_For; auto; intros; apply CEexp; auto.
apply C_For; auto; intros; apply C_CE; auto.
Qed.

Definition TExi I (cond : I → Prop) (func : ∀ i, cond i → set) : set :=
  fun a ⇒ ∃ i H, func i H a.
Definition TExi_preserve P := ∀ Ix cond func,
  (∀ i H, P (func i H)) → P (TExi Ix cond func).
Definition EExi I cond func := Cl (TExi I cond func).
Definition EExi_preserve P Q := ∀ Ix cond func,
  (∀ i H, P (func i H)) → Q (EExi Ix cond func).
Hint Unfold TExi EExi TExi_preserve EExi_preserve.

Lemma C_TExi : TExi_preserve C.
Proof.
intros Ix cond func Hfor; apply C_.
intros a [i [Ci Ha]]; apply (Cok (Hfor i Ci)); apply Ha.
  intros b [a [[i [Ci Hb]] ba]]; ∃ i, Ci.
  apply (Cdec (Hfor i Ci)); ∃ a; auto.
  intros b [a [[i [Ci Hb]] ba]]; ∃ i, Ci.
  apply (Cred (Hfor i Ci)); ∃ a; auto.
Qed.

Lemma Pcn_TExi : TExi_preserve Pcn.
Proof.
intros Ix cond func Hexi a [i [Ci Ha]].
apply (Hexi i Ci a Ha).
Qed.

Lemma CT_TExi : TExi_preserve CT.
Proof.
intros Ix cond func Hexi.
apply CT_CPcn.
apply Pcn_TExi; auto; intros; apply CTcn; auto.
apply C_TExi; auto; intros; apply C_CT; auto.
Qed.

Lemma Pexp_EExi : EExi_preserve (fun _ ⇒ True) Pexp.
Proof.
intros Ix cond func Hexi a [NVa Expa].
apply fold_Cl; right; auto.
Qed.

Lemma CE_EExi : EExi_preserve C CE.
Proof.
intros Ix cond func Hexi.
apply CE_CPexp.
apply Pexp_EExi; auto.
apply C_Cl; apply C_TExi; auto.
Qed.

Definition TTop : set := TExi set CT (fun R _ ⇒ R).
Definition ETop : set := EExi set CE (fun R _ ⇒ R).

Lemma CE_ETop : CE ETop.
Proof. apply CE_EExi; intros i H; apply C_CE; auto. Qed.

Lemma C_ETop : C ETop.
Proof. apply C_CE; apply CE_ETop. Qed.

Lemma CT_TTop : CT TTop.
Proof. apply CT_TExi; intros i H; auto. Qed.

Lemma C_TTop : C TTop.
Proof. apply C_CT; apply CT_TTop. Qed.

Definition TBot : set := For set CT (fun R _ ⇒ R).
Definition EBot : set := For set CE (fun R _ ⇒ R).

Lemma CE_EBot : CE EBot.
Proof.
apply CE_For.
∃ ETop; apply CE_ETop.
intros i H; exact H.
Qed.

Lemma C_EBot : C EBot.
Proof. apply C_CE; apply CE_EBot. Qed.

Lemma CT_TBot : CT TBot.
Proof.
apply CT_For.
∃ TTop; apply CT_TTop.
intros i H; exact H.
Qed.

Lemma C_TBot : C TBot.
Proof. apply C_CT; apply CT_TBot. Qed.

Fixpoint iter (F : set → set) k X : set :=
  match k with
    | O ⇒ X
    | S k ⇒ F (iter F k X)
  end.

Lemma iter_preserve : ∀ P F X, P X → (∀ Y, P Y → P (F Y)) → ∀ k, P (iter F k X).
Proof. intros P F X PX PF k; induction k; [exact PX|apply (PF _ IHk)]. Qed.

Lemma iter_dec : ∀ F X k, iter F (1 + k) X = iter F k (F X).
Proof. intros F X k; induction k; simpl in *; [|rewrite IHk]; reflexivity. Qed.

Lemma iter_le : ∀ F X k j, j ≤ k → iter F k X = iter F j (iter F (k - j) X).
Proof.
intros F X k; induction k; intros j Hjk; [inversion Hjk; reflexivity|simpl in *].
destruct j as [|j]; [reflexivity|].
rewrite (IHk j); [reflexivity|omega].
Qed.

Definition Mu Bot (F : set → set) : set := fun a ⇒
  ∀ k, term_lt a k → iter F k Bot a.
Definition EMu := Mu EBot.
Definition TMu := Mu TBot.
Hint Unfold Mu EMu TMu.

Definition Mu' Bot (F : set → set) : set := fun a ⇒
  ∃ k, term_lt a k ∧ iter F k Bot a.

Definition approx (R : set) k : set := fun a ⇒ term_lt a k ∧ R a.
Hint Unfold approx.

Lemma approx_unfold : ∀ k R a, approx R k a → R a.
Proof. intros R k a [Hk Ha]; exact Ha. Qed.

Lemma approx_fold : ∀ (R : set) k a, R a → term_lt a k → approx R k a.
Proof. intros R k a Ha ak; auto. Qed.

Lemma approx_approx : ∀ R j k, j ≤ k → approx R j = approx (approx R k) j.
Proof.
intros R j k jk.
apply extEq; split; intros a [? ?]; repeat split; auto.
  eapply unary_fuel_1; [|apply H].
  simpl; intros; omega.
  destruct H0; auto.
Qed.

Lemma approx_min : ∀ R j k, approx (approx R k) j = approx R (min j k).
Proof.
intros R j k.
apply extEq; split; intros a [? ?]; repeat split; auto.
destruct H0; apply term_lt_min; auto.
destruct H0; auto.
apply lt_term_le with (min j k); auto.
minmax.
apply lt_term_le with (min j k); auto.
minmax.
Qed.

Lemma approx_swap : ∀ R j k, approx (approx R k) j = approx (approx R j) k.
Proof.
intros R j k.
apply extEq; split; intros a [? [? ?]]; repeat split; auto.
Qed.

Lemma approx0 : ∀ R S, Inc (approx R 0) (approx S 0).
Proof. intros R S a [? ?]; exfalso; apply (term_lt_0 a); auto. Qed.

Lemma approx0_eq : ∀ R S, approx R 0 = approx S 0.
Proof. intros R S; apply extEq; split; intros a Ha; apply (approx0 _ _ a Ha). Qed.

Lemma approx_inc : ∀ R S, (∀ k a, approx R k a → approx S k a) → ∀ a, R a → S a.
Proof.
intros R S H a Ra.
destruct (term_lt_exists a) as [k ak].
apply approx_unfold with (k := k); auto.
Qed.

Lemma approx_eq : ∀ R S, (∀ k, approx R k = approx S k) → R = S.
Proof.
intros R S H.
apply extEq; split; intros a Ha; (eapply approx_inc; [|apply Ha]); intros.
rewrite <- H; auto.
rewrite H; auto.
Qed.

Lemma Cl_approx : ∀ R k a, approx (Cl R) k a → Cl (approx R k) a.
Proof.
intros R k a.
induction_red a; intros [ak Ha].
apply unfold_Cl in Ha as [Ha|[NVa Expa]]; apply fold_Cl; [left|right]; auto.
split; auto; intros b Hred.
apply IHa; auto; split; auto.
apply term_lt_red with (a := a); auto.
Qed.

Lemma Cl_approx_eq : ∀ R k, approx (Cl R) k = approx (Cl (approx R k)) k.
Proof.
intros R k; apply extEq; split.
  intros a [ak Ha]; split; auto.
  apply Cl_approx; auto.
  intros a; induction_red a; intros [ak Ha].
  split; auto.
  apply unfold_Cl in Ha as [[_ Ha]|[NVa Expa]]; apply fold_Cl; [left|right]; auto.
  split; auto; intros b Hred.
  apply IHa; auto; split; auto.
  apply term_lt_red with (a := a); auto.
Qed.

Lemma Inc_approx : ∀ R k a, approx R k a → R a.
Proof. intros; apply (approx_unfold k); auto. Qed.

Definition CST (F : set → set) : Prop := ∃ C, ∀ R, F R = C.

Definition WFj j (F : set → set) : Prop :=
  ∀ R k, approx (F R) k = approx (F (approx R (k - j))) k.

Definition WF F :=
  ∀ R k, approx (F R) (1 + k) = approx (F (approx R k)) (1 + k).

Definition NE := WFj 0.

Definition CF (P : set → Prop) (F : set → set) : Prop := ∀ R, P R → P (F R).

Hint Unfold CST WFj WF NE CF.

Lemma WF_CST : ∀ F, CST F → ∀ j, WFj j F.
Proof. intros F [C HF] j R k; rewrite 2 HF; reflexivity. Qed.

Lemma CST_WF : ∀ F, (∀ j, WFj j F) → CST F.
Proof.
intros F HF; ∃ (F EBot); intros R.
apply approx_eq; intros k.
rewrite (HF k R k).
rewrite (HF k EBot k).
replace (k - k) with 0 by omega.
rewrite approx0_eq with (S := EBot).
reflexivity.
Qed.

Lemma WFj_dec : ∀ F ij j, ij ≥ j → WFj ij F → WFj j F.
Proof.
intros F ij j Hij HF R k.
rewrite (HF R k).
rewrite (HF (approx R (k - j)) k).
rewrite <- (approx_approx R (k - ij) (k - j)); [|omega].
reflexivity.
Qed.

Lemma WFj_WF : ∀ F, WFj 1 F ↔ WF F.
Proof.
intros; split; intros ? R k.
  rewrite (H R (1 + k)).
  destruct k; simpl; auto.
  destruct k; simpl; [apply approx0_eq|].
  replace (k - 0) with k by omega.
  apply H.
Qed.

Lemma WFj_ : ∀ j F, WFj j F → ∀ R k, approx (F R) (j + k) = approx (F (approx R k)) (j + k).
Proof.
intros.
rewrite (H R (j + k)).
replace (j + k - j) with k by omega.
reflexivity.
Qed.

Lemma NE_id : ∀ F, (∀ R, F R = R) → NE F.
Proof. intros F H R k; repeat rewrite H; rewrite <- approx_approx; auto; omega. Qed.

Lemma WF_swap : ∀ F R S k, WF F → approx (iter F k R) k = approx (iter F k S) k.
Proof.
intros F R S k WFF; induction k.
  apply extEq; split; simpl; apply approx0; assumption.
  rewrite (WFF (iter F k R)); rewrite (WFF (iter F k S)); simpl.
  replace (k - 0) with k by omega.
  rewrite IHk; reflexivity.
Qed.

Lemma C_approx : ∀ R k, C R → C (approx R k).
Proof.
intros R k CR.
apply C_.
intros a [_ Ha]; apply (Cok CR); auto.
  intros b [a [[ak Ha] ba]].
  split; [apply le_term_lt with a; auto|].
  apply (Cdec CR); ∃ a; auto.
  intros b [a [[ak Ha] Hred]].
  split; [apply term_lt_red with a; auto|].
  apply (Cred CR); ∃ a; auto.
Qed.

Lemma Pcn_approx : ∀ R k, Pcn R → Pcn (approx R k).
Proof. intros R k CR a [_ Ha]; auto. Qed.

Lemma CT_approx : ∀ R k, CT R → CT (approx R k).
Proof.
intros R k CR.
apply CT_CPcn.
apply Pcn_approx; apply (CTcn CR).
apply C_approx; apply (C_CT CR).
Qed.

Lemma CF_iter_F : ∀ P F R, CF P F → P R → ∀ k, P (iter F k R).
Proof.
intros P F R CFF CR k; induction k; auto.
apply (CFF (iter F k R)); apply IHk.
Qed.

Lemma WF_approx_le : ∀ F R j k, WF F → j ≤ k →
  approx (iter F k R) j = approx (iter F j R) j.
Proof.
intros F R j k WFF Hjk.
rewrite iter_le with (j := j) (k := k); [|exact Hjk].
apply WF_swap; auto.
Qed.

Lemma WF_iter_lt : ∀ F R j k a, WF F → term_lt a k → term_lt a j →
  iter F j R a → iter F k R a.
Proof.
intros F R j k a WFF ak aj Fja.
remember (min k j) as x.
assert (x ≤ k); [subst; apply le_min_l|].
assert (x ≤ j); [subst; apply le_min_r|].
apply (approx_unfold x).
rewrite WF_approx_le; auto.
rewrite <- WF_approx_le with (k := j); auto.
apply approx_fold; auto; subst.
apply term_lt_min; assumption.
Qed.

Lemma CE_EMu : ∀ F, CF CE F → WF F → CE (EMu F).
Proof.
pose proof CE_EBot as CEBot.
intros F CFF WFF; apply CE_.
  intros a Ha.
  destruct (term_lt_exists a).
  pose proof (Ha x H).
  apply (CEok (CF_iter_F CE F EBot CFF CEBot x)); assumption.
  intros b [a [Ha ba]] j bj.
  destruct (term_lt_exists a) as [k ak].
  pose proof (le_term_lt b a k ba ak) as bk.
  apply WF_iter_lt with (j := k); auto.
  apply CEdec; [apply CF_iter_F; auto|].
  ∃ a; split; auto.
  intros b [a [Ha Hred]] j bj.
  destruct (term_lt_exists a) as [k ak].
  pose proof (term_lt_red a b k Hred ak) as bk.
  apply WF_iter_lt with (j := k); auto.
  apply CEred; [apply CF_iter_F; auto|].
  ∃ a; split; auto.
  intros a [NVa Expa] j aj.
  apply CEexp; [apply CF_iter_F; auto|].
  split; auto; intros b Hred.
  apply (Expa b Hred).
  apply term_lt_red with a; auto.
Qed.

Lemma CT_TMu : ∀ F, CF CT F → WF F → CT (TMu F).
Proof.
pose proof CT_TBot as CTBot.
intros F CFF WFF; apply CT_.
  intros a Ha.
  destruct (term_lt_exists a) as [k ak].
  pose proof (Ha k ak).
  apply (CTcn (CF_iter_F CT F TBot CFF CTBot k)); assumption.
  intros a Ha.
  destruct (term_lt_exists a).
  pose proof (Ha x H).
  apply (CTok (CF_iter_F CT F TBot CFF CTBot x)); assumption.
  intros b [a [Ha ba]] j bj.
  destruct (term_lt_exists a) as [k ak].
  pose proof (le_term_lt b a k ba ak) as bk.
  apply WF_iter_lt with (j := k); auto.
  apply CTdec; [apply CF_iter_F; auto|].
  ∃ a; split; auto.
  intros b [a [Ha Hred]] j bj.
  destruct (term_lt_exists a) as [k ak].
  pose proof (term_lt_red a b k Hred ak) as bk.
  apply WF_iter_lt with (j := k); auto.
  apply CTred; [apply CF_iter_F; auto|].
  ∃ a; split; auto.
Qed.

Lemma Mu_approx_iter : ∀ F k Bot, WF F → approx (Mu Bot F) k = approx (iter F k Bot) k.
Proof.
intros F k Bot WFF; apply extEq; split; intros a [ak Ha]; split; auto.
intros j aj.
eapply WF_iter_lt; auto; [apply ak|apply Ha].
Qed.

Lemma Mu_unfold : ∀ F Bot, WF F → Inc (Mu Bot F) (F (Mu Bot F)).
Proof.
intros F Bot WFF a Ha.
destruct (term_lt_exists a) as [k ak].
assert (term_lt a (1 + k)); [eapply unary_fuel_1; [|apply ak]; instantiate; simpl; intros j H; omega|clear ak].
apply approx_unfold with (k := 1 + k).
rewrite WFF.
rewrite Mu_approx_iter; [|assumption].
rewrite <- WFF.
apply approx_fold; auto.
apply (Ha (1 + k)); auto.
Qed.

Lemma Mu_fold : ∀ F Bot, WF F → Inc (F (Mu Bot F)) (Mu Bot F).
Proof.
intros F Bot WFF a Ha k ak.
destruct k; [exfalso; apply (term_lt_0 a ak)|].
apply approx_unfold with (k := 1 + k); simpl.
rewrite WFF.
rewrite <- Mu_approx_iter; [|assumption].
rewrite <- WFF.
apply approx_fold; auto.
Qed.

Lemma Mu_Mu' : ∀ F Bot, WF F → Mu Bot F = Mu' Bot F.
Proof.
intros F Bot WFF; apply extEq; split; intros a Ha.
  destruct (term_lt_exists a) as [k ak].
  ∃ k; auto.
  destruct Ha as [k [ak Ha]].
  intros j aj.
  apply WF_iter_lt with k; auto.
Qed.

Lemma WF_PArr : ∀ R S k,
  approx (PArr R S) (1 + k) = approx (PArr (approx R k) (approx S k)) (1 + k).
Proof.
intros R S k; apply extEq; split; intros a [ak Ha]; split; auto.
  generalize ak Ha; clear ak Ha; induction_red a; intros ak Ha.
  destruct Ha as [j [a' [Heq [Hok Hsub]]]].
  rename a into lam, a' into a; ∃ j; ∃ a; split; [|split]; auto; subst lam.
  intros Hj b Rb.
  split; destruct ak as [jk ak].
    apply unary_fuel_map_trivial; intros.
    destruct (lt_dec k0 (j - 1)); [rewrite min_l|rewrite min_r]; omega.
    apply Hsub; auto.
    apply (Inc_approx R k); auto.
  generalize ak Ha; clear ak Ha; induction_red a; intros ak Ha.
  destruct Ha as [j [a' [Heq [Hok Hsub]]]].
  rename a into lam, a' into a; ∃ j; ∃ a; split; [|split]; auto; subst lam.
  intros Hj b Rb; destruct ak as [jk ak].
  apply Hsub; auto.
  split; auto.
  apply unary_fuel_map_trivial; intros.
  destruct (lt_dec k0 (j - 1)); [rewrite min_l|rewrite min_r]; omega.
Qed.

Lemma WF_EArr : ∀ R S k,
  approx (EArr R S) (1 + k) = approx (EArr (approx R k) (approx S k)) (1 + k).
Proof.
intros R S k.
unfold EArr.
rewrite Cl_approx_eq.
rewrite WF_PArr.
rewrite <- Cl_approx_eq.
reflexivity.
Qed.

Lemma WFj_EArr : ∀ R S k,
  approx (EArr R S) k = approx (EArr (approx R (k - 1)) (approx S (k - 1))) k.
Proof.
intros R S k.
destruct k; [apply approx0_eq|]; simpl; rewrite <- minus_n_O.
apply WF_EArr.
Qed.

Lemma WF_TArr : ∀ R S k,
  approx (TArr R S) (1 + k) = approx (TArr (approx R k) (approx S k)) (1 + k).
Proof.
intros R S k.
unfold TArr.
rewrite WF_PArr.
rewrite (Cl_approx_eq R).
rewrite (Cl_approx_eq S).
rewrite <- WF_PArr.
reflexivity.
Qed.

Lemma WF_PProd : ∀ R S k,
  approx (PProd R S) (1 + k) = approx (PProd (approx R k) (approx S k)) (1 + k).
Proof.
intros R S k; apply extEq; split; intros a [ak Ha]; split; auto.
  generalize ak Ha; clear ak Ha; induction_red a; intros ak Ha.
  destruct Ha as [j [a' [b' [Heq [Hok Hproj]]]]].
  rename a into pair, a' into a, b' into b; ∃ j, a, b; split; [|split]; auto; subst pair.
  intros Hj; split.
    split; destruct ak as [jk [ak bk]]; [|apply Hproj; auto].
    apply unary_fuel_map_trivial; intros.
    destruct (lt_dec k0 (j - 1)); [rewrite min_l|rewrite min_r]; omega.
    split; destruct ak as [jk [ak bk]]; [|apply Hproj; auto].
    apply unary_fuel_map_trivial; intros.
    destruct (lt_dec k0 (j - 1)); [rewrite min_l|rewrite min_r]; omega.
  generalize ak Ha; clear ak Ha; induction_red a; intros ak Ha.
  destruct Ha as [j [a' [b' [Heq [Hok Hproj]]]]].
  rename a into pair, a' into a, b' into b; ∃ j, a, b; split; [|split]; auto; subst pair.
  intros Hj; destruct ak as [jk [ak bk]].
  split; apply Hproj; auto.
Qed.

Lemma WF_EProd : ∀ R S k,
  approx (EProd R S) (1 + k) = approx (EProd (approx R k) (approx S k)) (1 + k).
Proof.
intros R S k.
unfold EProd.
rewrite Cl_approx_eq.
rewrite WF_PProd.
rewrite <- Cl_approx_eq.
reflexivity.
Qed.

Lemma WFj_EProd : ∀ R S k,
  approx (EProd R S) k = approx (EProd (approx R (k - 1)) (approx S (k - 1))) k.
Proof.
intros R S k.
destruct k; [apply approx0_eq|]; simpl; rewrite <- minus_n_O.
apply WF_EProd.
Qed.

Lemma WF_TProd : ∀ R S k,
  approx (TProd R S) (1 + k) = approx (TProd (approx R k) (approx S k)) (1 + k).
Proof.
intros R S k.
unfold TProd.
rewrite WF_PProd.
rewrite (Cl_approx_eq R).
rewrite (Cl_approx_eq S).
rewrite <- WF_PProd.
reflexivity.
Qed.

Lemma WFj_For : ∀ j F Ix cond func, (∀ i H, WFj j (fun X ⇒ func X i H)) →
  (∀ X, F X = For Ix cond (func X)) → WFj j F.
Proof.
intros j F Ix cond func H HF R k; repeat rewrite HF.
apply extEq; split; intros a [ak Ha]; split; auto; intros i ci.
  apply approx_unfold with k.
  rewrite <- H.
  apply approx_fold; auto.
  apply approx_unfold with k.
  rewrite H.
  apply approx_fold; auto.
Qed.

Lemma WFj_TExi : ∀ j F Ix cond func, (∀ i H, WFj j (fun X ⇒ func X i H)) →
  (∀ X, F X = TExi Ix cond (func X)) → WFj j F.
Proof.
intros j F Ix cond func H HF R k; repeat rewrite HF.
apply extEq; split; intros a [ak [i [ci Ha]]]; split; auto; ∃ i, ci.
  apply approx_unfold with k.
  rewrite <- H.
  apply approx_fold; auto.
  apply approx_unfold with k.
  rewrite H.
  apply approx_fold; auto.
Qed.

Lemma WFj_EExi : ∀ j F Ix cond func, (∀ i H, WFj j (fun X ⇒ func X i H)) →
  (∀ X, F X = EExi Ix cond (func X)) → WFj j F.
Proof.
intros j F Ix cond func H HF R k; repeat rewrite HF.
apply extEq; split; intros a [ak Ha]; split; auto.
  generalize ak Ha; clear ak Ha; induction_red a; intros ak Ha.
  unfold EExi in Ha; apply unfold_Cl in Ha as [?|[? ?]]; apply fold_Cl; [left|right].
    apply approx_unfold with k.
    rewrite <- (WFj_TExi j (fun X ⇒ TExi Ix cond (func X)) Ix cond func); auto.
    split; auto; intros b Hred.
    apply IHa; auto.
    apply term_lt_red with a; auto.
  generalize ak Ha; clear ak Ha; induction_red a; intros ak Ha.
  unfold EExi in Ha; apply unfold_Cl in Ha as [?|[? ?]]; apply fold_Cl; [left|right].
    apply approx_unfold with k.
    rewrite (WFj_TExi j (fun X ⇒ TExi Ix cond (func X)) Ix cond func); auto.
    split; auto; intros b Hred.
    apply IHa; auto.
    apply term_lt_red with a; auto.
Qed.

Lemma WFj_min : ∀ F R jk k, WFj (jk - k) F →
  approx (F R) jk = approx (F (approx R k)) jk.
Proof.
intros F R jk k HF.
destruct (le_gt_dec jk k).
  replace (jk - k) with 0 in HF by omega.
  rewrite HF.
  rewrite (HF (approx R k)).
  replace (jk - 0) with jk by omega.
  rewrite (approx_approx R jk k); auto.
  rewrite HF.
  replace (jk - (jk - k)) with k by omega.
  reflexivity.
Qed.

Lemma WFj_Mu : ∀ j F Bot, (∀ X, WF (F X)) →
  (∀ Y, WFj j (fun X ⇒ F X Y)) →
  WFj j (fun X ⇒ (Mu Bot (fun Y ⇒ F X Y))).
Proof.
intros j F Bot HX HY R k.
rewrite 2 Mu_approx_iter; auto.
assert (∀ i,
  approx (iter (fun Y : set ⇒ F R Y) k Bot) k =
  approx (iter (fun Y : set ⇒ F (approx R (i + (k - j))) Y) k Bot) k); [|apply (H 0)].
induction k; intros i; [apply approx0_eq|].
destruct (le_gt_dec j k).
  replace (i + (S k - j)) with (1 + i + (k - j)) by omega.
  simpl; rewrite HX; simpl.
  rewrite IHk with (1 + i); simpl.
  rewrite <- HX; simpl.
  apply (WFj_min (fun X ⇒ F X _) R).
  apply WFj_dec with j; auto; omega.
  replace (i + (S k - j)) with i by omega.
  simpl; rewrite HX; simpl.
  rewrite IHk with i.
  replace (i + (k - j)) with i by omega.
  rewrite <- HX; simpl.
  apply (WFj_min (fun X ⇒ F X _) R).
  apply WFj_dec with j; auto; omega.
Qed.

Lemma WF_period : ∀ F R S, WF F → R = F R → S = F S → R = S.
Proof.
intros F R S WFF HR HS.
apply approx_eq; intros k.
induction k; [apply approx0_eq|].
rewrite HR; rewrite HS.
rewrite WFF; rewrite IHk; rewrite <- WFF; reflexivity.
Qed.

Lemma Mu_sub : ∀ Bot F G, WF F → WF G →
  (∀ R S, Inc R S → Inc (F R) (G S)) → Inc (Mu Bot F) (Mu Bot G).
Proof.
intros Bot F G WFF WFG Hinc a Ha.
destruct (term_lt_exists a) as [k ak].
apply approx_unfold with k.
apply (approx_fold _ k a) in Ha; auto.
generalize a Ha; clear a ak Ha; induction k;
  intros a [ak Ha]; [exfalso; apply term_lt_0 with a; auto|].
rewrite Mu_approx_iter; auto; simpl.
rewrite WFG.
apply approx_fold; auto.
apply (Hinc (approx (iter F k Bot) k)).
  clear a Ha ak.
  intros a Ha.
  rewrite <- Mu_approx_iter; auto.
  apply IHk.
  rewrite Mu_approx_iter; auto.
apply approx_unfold with (1 + k).
rewrite <- WFF.
replace (F (iter F k Bot)) with (iter F (1 + k) Bot) by reflexivity.
rewrite <- Mu_approx_iter; auto.
Qed.

Lemma EMu_sub : ∀ F G, CF CE F → CF CE G → WF F → WF G →
  (∀ R S, CE R → CE S → (∀ a, R a → S a) → ∀ a, F R a → G S a) →
  ∀ a, EMu F a → EMu G a.
Proof.
intros F G CFF CFG WFF WFG Hinc a Ha.
pose proof (CF_iter_F CE F EBot CFF CE_EBot) as CiF.
pose proof (CF_iter_F CE G EBot CFG CE_EBot) as CiG.
destruct (term_lt_exists a) as [k ak].
apply approx_unfold with k.
apply (approx_fold _ k a) in Ha; auto.
generalize a Ha; clear a ak Ha.
unfold EMu; repeat rewrite Mu_approx_iter; auto.
induction k; intros a [ak Ha]; [exfalso; apply term_lt_0 with a; auto|].
simpl; rewrite WFG.
rewrite <- (Cl_CE (iter G k EBot)); auto.
rewrite Cl_approx_eq.
simpl; rewrite <- WFG.
split; auto.
apply Hinc with (Cl (approx (iter F k EBot) k)); auto;
  try (apply CE_Cl; apply C_approx; apply C_CE; auto).
apply Cl_monotone; auto.
apply approx_unfold with (1 + k).
rewrite WFF.
rewrite <- Cl_approx_eq.
rewrite <- WFF.
rewrite Cl_CE; auto.
Qed.


Definition Subst (R S : set) : set := fun a ⇒ ∀ b, R b → S (subst b 0 a).
Hint Unfold Subst Subst.

Fixpoint EJudg (G : list set) (S : set) : set :=
  match G with
    | nil ⇒ S
    | cons R G ⇒ Subst (EJudg G R) (EJudg G S)
  end.

Fixpoint TJudg (G : list set) (S : set) : set :=
  match G with
    | nil ⇒ Cl S
    | cons R G ⇒ Subst (TJudg G R) (TJudg G S)
  end.

Lemma Pdec_EJudg : ∀ G S, C S → Pdec (EJudg G S).
Proof.
induction G as [|R G]; intros S CS a' [a [Ha ba]]; simpl in ×.
  apply (Cdec CS); ∃ a; auto.
  intros b Hb; apply IHG; auto.
  ∃ (subst b 0 a); split; auto.
  apply le_term_subst; auto.
  apply binary_fuel_refl; auto.
Qed.

Lemma Pred_EJudg : ∀ G S, C S → Pred (EJudg G S).
Proof.
induction G as [|R G]; intros S CS a' [a [Ha ba]]; simpl in ×.
  apply (Cred CS); ∃ a; auto.
  intros b Hb; apply IHG; auto.
  ∃ (subst b 0 a); split; auto.
  apply red_subst; auto.
Qed.

Lemma EJudg_Var : ∀ G S, Pexp S → EJudg G S (Var 0 (length G + 1)).
Proof.
intros G S CS; induction G; simpl.
apply R_Var; auto.
  intros b Hb.
  simpl; subst_lift_var.
  rewrite <- minus_n_O.
  apply IHG.
Qed.

Lemma Pok_EJudg : ∀ G S, Forall Pexp G → C S → Pok (EJudg G S).
Proof.
induction G as [|R G]; intros S CG CS a Ha; simpl in ×.
  apply (Cok CS); auto.
  apply OK_subst_Var with (x := (length G + 1)) (i := 0).
  inversion CG; subst.
  apply (IHG S H2 CS _).
  apply Ha; apply EJudg_Var; auto.
Qed.

Lemma C_EJudg : ∀ G S, Forall Pexp G → C S → C (EJudg G S).
Proof.
intros G S CG CS; apply C_.
apply Pok_EJudg; auto.
apply Pdec_EJudg; auto.
apply Pred_EJudg; auto.
Qed.

Lemma Pdec_TJudg : ∀ G S, C S → Pdec (TJudg G S).
Proof.
induction G as [|R G]; intros S CS a' [a [Ha ba]]; simpl in ×.
  apply (Cdec (C_Cl CS)); ∃ a; auto.
  intros b Hb; apply IHG; auto.
  ∃ (subst b 0 a); split; auto.
  apply le_term_subst; auto.
  apply binary_fuel_refl; auto.
Qed.

Lemma Pred_TJudg : ∀ G S, C S → Pred (TJudg G S).
Proof.
induction G as [|R G]; intros S CS a' [a [Ha ba]]; simpl in ×.
  apply (Cred (C_Cl CS)); ∃ a; auto.
  intros b Hb; apply IHG; auto.
  ∃ (subst b 0 a); split; auto.
  apply red_subst; auto.
Qed.

Lemma TJudg_Var : ∀ G S, TJudg G S (Var 0 (length G + 1)).
Proof.
intros G S; induction G; simpl.
apply R_Var; apply Pexp_Cl.
  intros b Hb.
  simpl; subst_lift_var.
  rewrite <- minus_n_O.
  apply IHG.
Qed.

Lemma Pok_TJudg : ∀ G S, C S → Pok (TJudg G S).
Proof.
induction G as [|R G]; intros S CS a Ha; simpl in ×.
  apply (Cok (C_Cl CS)); auto.
  apply OK_subst_Var with (x := (length G + 1)) (i := 0).
  apply (IHG S CS _).
  apply Ha; apply TJudg_Var; auto.
Qed.

Lemma C_TJudg : ∀ G S, C S → C (TJudg G S).
Proof.
intros G S CS; apply C_.
apply Pok_TJudg; auto.
apply Pdec_TJudg; auto.
apply Pred_TJudg; auto.
Qed.

Lemma EVar_sem : ∀ R k x G, Forall C G →
  nth x G ETop = R →
  EJudg G R (Var k x).
Proof.
induction x; intros G CG Hx;
(destruct G as [|R0 G]; simpl in *; subst; [apply R_Var; apply Pexp_Cl|]).
  intros b Rb; simpl; subst_lift_var; rewrite lift_0.
  inversion CG; subst.
  apply Pdec_EJudg; auto.
  eexists; split; [apply Rb|].
  apply le_term_lessen_trivial.
  inversion CG; subst.
  intros b0 Rb0.
  simpl; subst_lift_var; rewrite <- minus_n_O.
  apply IHx; auto.
Qed.

Lemma TVar_sem : ∀ R k x G, Forall C G →
  nth x G TTop = R →
  TJudg G R (Var k x).
Proof.
induction x; intros G CG Hx;
(destruct G as [|R0 G]; simpl in *; subst; [apply R_Var; apply Pexp_Cl|]).
  intros b Rb; simpl; subst_lift_var; rewrite lift_0.
  inversion CG; subst.
  apply Pdec_TJudg; auto.
  eexists; split; [apply Rb|].
  apply le_term_lessen_trivial.
  inversion CG; subst.
  intros b0 Rb0.
  simpl; subst_lift_var; rewrite <- minus_n_O.
  apply IHx; auto.
Qed.

Lemma ELam_sem : ∀ G R S k a, Pexp R → C S →
  EJudg (R :: G) S a →
  EJudg G (EArr R S) (Lam k a).
Proof.
induction G as [|R0 G]; intros R S k a CR CS Ha; simpl in ×.
  apply fold_Cl; left.
  ∃ k; ∃ a; split; [|split]; auto.
    apply OK_subst_Var with 0 0.
    apply (Cok CS); apply Ha; apply R_Var; auto.
    intros Hk b Rb.
    rewrite lessen_subst; rewrite <- subst_lessen; rewrite <- lessen_subst.
    apply (Cdec CS).
    ∃ (subst (lessen (k - 1) b) 0 a).
    split; [apply Ha; auto|].
    apply le_term_lessen_trivial.
  intros b0 Rb0; subst; simpl.
  apply IHG; auto.
  intros b Rb.
  replace b with (subst b0 0 (shift 0 b)); [|apply subst_lift_0].
  rewrite <- subst_subst_0; apply Ha; auto.
  intros ? ?; rewrite subst_lift_0; auto.
Qed.

Lemma TLam_sem : ∀ G R S k a, C S →
  TJudg (R :: G) S a →
  TJudg G (TArr R S) (Lam k a).
Proof.
induction G as [|R0 G]; intros R S k a CS Ha; simpl in ×.
  apply fold_Cl; left.
  ∃ k; ∃ a; split; [|split]; auto.
    apply OK_subst_Var with 0 0.
    apply (Cok (C_Cl CS)); apply Ha; apply R_Var; apply Pexp_Cl.
    intros Hk b Rb.
    rewrite lessen_subst; rewrite <- subst_lessen; rewrite <- lessen_subst.
    apply (Cdec (C_Cl CS)).
    ∃ (subst (lessen (k - 1) b) 0 a).
    split; [apply Ha; auto|].
    apply le_term_lessen_trivial.
  intros b0 Rb0; subst; simpl.
  apply IHG; auto.
  intros b Rb.
  replace b with (subst b0 0 (shift 0 b)); [|apply subst_lift_0].
  rewrite <- subst_subst_0; apply Ha; auto.
  intros ? ?; rewrite subst_lift_0; auto.
Qed.

Lemma EApp_sem : ∀ G R S k a b, C R → CE S →
  EJudg G (EArr R S) a →
  EJudg G R b →
  EJudg G S (App k a b).
Proof.
induction G as [|R0 G]; intros R S k a b CR CS Ha Hb; simpl in ×.
  generalize Ha b Hb k; clear Ha b Hb k; induction_red a; intros Ha b; induction_red b; intros Hb k.
  apply (CEexp CS); split; [split|]; simpl; auto.
    intros Errab.
    inversion Errab; subst.
generalize H0; apply (Cv (CEok (CE_EArr CR (C_CE CS)))); auto.
generalize H0; apply (Cv (Cok CR)); auto.
      unfold EArr in Ha; apply unfold_Cl in Ha.
      destruct Ha.
destruct H as [? [? [? ?]]]; inversion H.
destruct H as [[? ?] ?]; inversion H.
    intros b0 Hred; inversion Hred.
apply IHa; auto; apply (CEred (CE_EArr CR (C_CE CS))); ∃ a; auto.
apply IHb; auto; apply (Cred CR); ∃ b; auto.
      subst.
      unfold EArr in Ha; apply unfold_Cl in Ha as [[? [? [? [? ?]]]]|Expa]; subst.
        inversion H; clear H; subst; simpl in ×.
        rewrite <- minus_n_O in H1.
        apply (CEdec CS); auto.
        ∃ (lessen k0 (subst b 0 x0)); split; [apply H1; auto; [omega|]|].
          apply (Cdec CR).
          ∃ b; split; auto.
          apply le_term_lessen_trivial.
apply le_term_lessen; [|apply binary_fuel_refl; auto]; minmax.
        destruct Expa as [[? ?] ?].
        inversion H.
  intros b0 Rb0; simpl.
  apply (IHG R S); auto.
Qed.

Lemma TApp_sem : ∀ G R S k a b, C R → C S →
  TJudg G (TArr R S) a →
  TJudg G R b →
  TJudg G S (App k a b).
Proof.
induction G as [|R0 G]; intros R S k a b CR CS Ha Hb; simpl in ×.
  generalize Ha b Hb k; clear Ha b Hb k; induction_red a; intros Ha b; induction_red b; intros Hb k.
  apply (Pexp_Cl S); split; [split|]; simpl; auto.
    intros Errab.
    inversion Errab; subst.
generalize H0; apply (Cv (Cok (C_Cl (C_PArr (C_Cl CR) (C_Cl CS))))); auto.
generalize H0; apply (Cv (Cok (C_Cl CR))); auto.
      unfold TArr in Ha; apply unfold_Cl in Ha.
      destruct Ha.
destruct H as [? [? [? ?]]]; inversion H.
destruct H as [[? ?] ?]; inversion H.
    intros b0 Hred; inversion Hred.
apply IHa; auto;
                     apply (Cred (C_Cl (C_PArr (C_Cl CR) (C_Cl CS)))); ∃ a; auto.
apply IHb; auto; apply (Cred (C_Cl CR)); ∃ b; auto.
      subst.
      unfold TArr in Ha; apply unfold_Cl in Ha as [[? [? [? [? ?]]]]|Expa]; subst.
        inversion H; clear H; subst; simpl in ×.
        rewrite <- minus_n_O in H1.
        apply (Cdec (C_Cl CS)); auto.
        ∃ (lessen k0 (subst b 0 x0)); split; [apply H1; auto; [omega|]|].
          apply (Cdec (C_Cl CR)).
          ∃ b; split; auto.
          apply le_term_lessen_trivial.
apply le_term_lessen; [|apply binary_fuel_refl; auto]; minmax.
        destruct Expa as [[? ?] ?].
        inversion H.
  intros b0 Rb0; simpl.
  apply (IHG R S); auto.
Qed.

Lemma EPair_sem : ∀ G R S k a b, C R → C S →
  EJudg G R a →
  EJudg G S b →
  EJudg G (EProd R S) (Pair k a b).
Proof.
induction G as [|R0 G]; intros R S k a b CR CS Ha Hb; simpl in ×.
  apply fold_Cl; left.
  ∃ k, a, b; split; [|split]; auto.
    split; [apply (Cok CR)|apply (Cok CS)]; auto.
    intros Hk; split; [apply (Cdec CR); ∃ a|apply (Cdec CS); ∃ b];
    split; auto; apply le_term_lessen_trivial.
  intros b0 Rb0; simpl; apply IHG; auto.
Qed.

Lemma TPair_sem : ∀ G R S k a b, C R → C S →
  TJudg G R a →
  TJudg G S b →
  TJudg G (TProd R S) (Pair k a b).
Proof.
induction G as [|R0 G]; intros R S k a b CR CS Ha Hb; simpl in ×.
  apply fold_Cl; left.
  ∃ k, a, b; split; [|split]; auto.
    split; [apply (Cok (C_Cl CR))|apply (Cok (C_Cl CS))]; auto.
    intros Hk; split; [apply (Cdec (C_Cl CR)); ∃ a|apply (Cdec (C_Cl CS)); ∃ b];
    split; auto; apply le_term_lessen_trivial.
  intros b0 Rb0; simpl; apply IHG; auto.
Qed.

Lemma EFst_sem : ∀ G R S k a, CE R → C S →
  EJudg G (EProd R S) a →
  EJudg G R (Fst k a).
Proof.
induction G as [|R0 G]; intros R S k a CR CS Ha; simpl in ×.
  generalize Ha k; clear Ha k; induction_red a; intros Ha k.
  apply (CEexp CR); split; [split|]; simpl; auto.
    intros Errab.
    inversion Errab; subst.
generalize H0; apply (Cv (CEok (CE_EProd (C_CE CR) CS))); auto.
      unfold EProd in Ha; apply unfold_Cl in Ha.
      destruct Ha.
destruct H as [? [? [? [? _]]]]; inversion H.
destruct H as [[? ?] ?]; inversion H.
    intros b0 Hred; inversion Hred.
apply IHa; auto; apply (CEred (CE_EProd (C_CE CR) CS)); ∃ a; auto.
      subst.
      unfold EProd in Ha; apply unfold_Cl in Ha as [[? [? [? [? [? ?]]]]]|Expa]; subst.
        inversion H; clear H; subst; simpl in ×.
        rewrite <- minus_n_O in H1.
        apply (CEdec CR); auto.
        ∃ (lessen k0 x0); split; [apply H1; auto; omega|].
        apply le_term_lessen; [|apply binary_fuel_refl; auto]; minmax.
        destruct Expa as [[? ?] ?]; inversion H.
  intros b0 Rb0; simpl.
  apply (IHG R S); auto.
Qed.

Lemma TFst_sem : ∀ G R S k a, C R → C S →
  TJudg G (TProd R S) a →
  TJudg G R (Fst k a).
Proof.
induction G as [|R0 G]; intros R S k a CR CS Ha; simpl in ×.
  generalize Ha k; clear Ha k; induction_red a; intros Ha k.
  apply (Pexp_Cl R); split; [split|]; simpl; auto.
    intros Errab.
    inversion Errab; subst.
generalize H0; apply (Cv (Cok (C_Cl (C_PProd (C_Cl CR) (C_Cl CS))))); auto.
      unfold TProd in Ha; apply unfold_Cl in Ha.
      destruct Ha.
destruct H as [? [? [? [? _]]]]; inversion H.
destruct H as [[? ?] ?]; inversion H.
    intros b0 Hred; inversion Hred.
apply IHa; auto; apply (Cred (C_Cl (C_PProd (C_Cl CR) (C_Cl CS)))); ∃ a; auto.
      subst.
      unfold TProd in Ha; apply unfold_Cl in Ha as [[? [? [? [? [? ?]]]]]|Expa]; subst.
        inversion H; clear H; subst; simpl in ×.
        rewrite <- minus_n_O in H1.
        apply (Cdec (C_Cl CR)); auto.
        ∃ (lessen k0 x0); split; [apply H1; auto; omega|].
        apply le_term_lessen; [|apply binary_fuel_refl; auto]; minmax.
        destruct Expa as [[? ?] ?]; inversion H.
  intros b0 Rb0; simpl.
  apply (IHG R S); auto.
Qed.

Lemma ESnd_sem : ∀ G R S k a, C R → CE S →
  EJudg G (EProd R S) a →
  EJudg G S (Snd k a).
Proof.
induction G as [|R0 G]; intros R S k a CR CS Ha; simpl in ×.
  generalize Ha k; clear Ha k; induction_red a; intros Ha k.
  apply (CEexp CS); split; [split|]; simpl; auto.
    intros Errab.
    inversion Errab; subst.
generalize H0; apply (Cv (CEok (CE_EProd CR (C_CE CS)))); auto.
      unfold EProd in Ha; apply unfold_Cl in Ha.
      destruct Ha.
destruct H as [? [? [? [? _]]]]; inversion H.
destruct H as [[? ?] ?]; inversion H.
    intros b0 Hred; inversion Hred.
apply IHa; auto; apply (CEred (CE_EProd CR (C_CE CS))); ∃ a; auto.
      subst.
      unfold EProd in Ha; apply unfold_Cl in Ha as [[? [? [? [? [? ?]]]]]|Expa]; subst.
        inversion H; clear H; subst; simpl in ×.
        rewrite <- minus_n_O in H1.
        apply (CEdec CS); auto.
        ∃ (lessen k0 x1); split; [apply H1; auto; omega|].
        apply le_term_lessen; [|apply binary_fuel_refl; auto]; minmax.
        destruct Expa as [[? ?] ?]; inversion H.
  intros b0 Rb0; simpl.
  apply (IHG R S); auto.
Qed.

Lemma TSnd_sem : ∀ G R S k a, C R → C S →
  TJudg G (TProd R S) a →
  TJudg G S (Snd k a).
Proof.
induction G as [|R0 G]; intros R S k a CR CS Ha; simpl in ×.
  generalize Ha k; clear Ha k; induction_red a; intros Ha k.
  apply (Pexp_Cl S); split; [split|]; simpl; auto.
    intros Errab.
    inversion Errab; subst.
generalize H0; apply (Cv (Cok (C_Cl (C_PProd (C_Cl CR) (C_Cl CS))))); auto.
      unfold TProd in Ha; apply unfold_Cl in Ha.
      destruct Ha.
destruct H as [? [? [? [? _]]]]; inversion H.
destruct H as [[? ?] ?]; inversion H.
    intros b0 Hred; inversion Hred.
apply IHa; auto; apply (Cred (C_Cl (C_PProd (C_Cl CR) (C_Cl CS)))); ∃ a; auto.
      subst.
      unfold TProd in Ha; apply unfold_Cl in Ha as [[? [? [? [? [? ?]]]]]|Expa]; subst.
        inversion H; clear H; subst; simpl in ×.
        rewrite <- minus_n_O in H1.
        apply (Cdec (C_Cl CS)); auto.
        ∃ (lessen k0 x1); split; [apply H1; auto; omega|].
        apply le_term_lessen; [|apply binary_fuel_refl; auto]; minmax.
        destruct Expa as [[? ?] ?]; inversion H.
  intros b0 Rb0; simpl.
  apply (IHG R S); auto.
Qed.

Lemma ECoer_sem : ∀ G R S, Inc R S → ∀ a, EJudg G R a → EJudg G S a.
Proof.
induction G as [|R0 G]; intros R S RS a Ha; simpl in *; auto.
intros b0 Rb0.
apply (IHG R S); auto.
Qed.

Lemma TCoer_sem : ∀ G R S, Inc R S → ∀ a, TJudg G R a → TJudg G S a.
Proof.
induction G as [|R0 G]; intros R S RS a Ha; simpl in *; auto.
apply Cl_monotone with R; auto.
intros b0 Rb0.
apply (IHG R S); auto.
Qed.

Lemma Edistrib : ∀ I cond func G a,
  (∃ i, cond i) → (∀ i H, CE (func i H)) →
  For I cond (fun i H ⇒ EJudg G (func i H)) a →
  EJudg G (For I cond func) a.
Proof.
induction G as [|R G]; intros a Hexi CEfunc H; auto; simpl.
intros b0 Rb0; match goal with | |- ?J _ _ _ ⇒ replace J with EJudg by reflexivity end.
apply IHG; auto; intros i Hi; apply H; auto.
Qed.

Lemma Cl_For : ∀ Ix cond func (R : set),
  (∃ i, cond i) → (∀ i H, C (func i H)) →
  (∀ a, For Ix cond func a → R a) →
  ∀ a, For Ix cond (fun i H ⇒ Cl (func i H)) a → Cl R a.
Proof.
intros Ix cond func R Hexi Cfunc Hinc a.
induction_red a; intros Ha.
destruct (N_dec a); apply fold_Cl; [left|right].
  apply Hinc.
  intros i ci.
  apply (destruct_Cl_CN _ _ c (Ha i ci)).
  repeat split; auto.
    destruct Hexi as [i ci].
    apply (Cv (Cok (C_Cl (Cfunc i ci)))); auto.
    intros b Hred.
    apply IHa; auto.
    intros i ci.
    apply (Cred (C_Cl (Cfunc i ci))).
    ∃ a; auto.
Qed.

Lemma approx_For : ∀ Ix cond func (R : set) k,
  (∀ a, For Ix cond (fun i H ⇒ approx (func i H) k) a → approx R k a) →
  ∀ a, term_lt a k → For Ix cond func a → R a.
Proof.
intros Ix cond func R k Hinc a ak Ha.
apply approx_unfold with k; auto.
Qed.

Lemma For_approx : ∀ Ix cond func (R : set) k,
  (∃ i, cond i) →
  (∀ a, term_lt a k → For Ix cond func a → R a) →
  ∀ a, For Ix cond (fun i H ⇒ approx (func i H) k) a → approx R k a.
Proof.
intros Ix cond func R k [i ci] Hinc a Ha.
destruct (Ha i ci) as [ak _].
split; auto.
apply Hinc; auto.
clear i ci; intros i ci.
apply approx_unfold with k; auto.
Qed.

Lemma Cl_approx_For : ∀ Ix cond func (R : set) k,
  (∃ i, cond i) → (∀ i H, C (func i H)) →
  (∀ a, term_lt a k → For Ix cond func a → R a) →
  ∀ a, term_lt a k → For Ix cond (fun i H ⇒ Cl (func i H)) a → Cl R a.
Proof.
intros Ix cond func R k Hexi Cfunc Hinc a.
induction_red a; intros ak Ha.
destruct (N_dec a); apply fold_Cl; [left|right].
  apply Hinc; auto.
  intros i ci.
  apply (destruct_Cl_CN _ _ c (Ha i ci)).
  repeat split; auto.
    destruct Hexi as [i ci].
    apply (Cv (Cok (C_Cl (Cfunc i ci)))); auto.
    intros b Hred.
    apply IHa; auto; [apply term_lt_red with a; auto|].
    intros i ci.
    apply (Cred (C_Cl (Cfunc i ci))).
    ∃ a; auto.
Qed.