Library Lsoundness

Require Import List.

Require Import mxx.
Require Import list.
Require Import Flanguage.
Require Import Fsemantics.
Require Import Ftypesystem.
Require Import Fsoundness.
Require Import Llanguage.
Require Import Ltypesystem.

Fixpoint OKstep k a :=
  match k with
    | O ⇒ V a
    | S k ⇒ V a ∧ ∀ b, red a b → OKstep k b
  end.

CoInductive OK a : Prop :=
| OK_ : V a → (∀ b, red a b → OK b) → OK a.

Lemma OKOKstep : ∀ a, (∀ k, OKstep k a) → OK a.
Proof.
cofix.
intros a Ha.
apply OK_; [apply (Ha 0)|].
intros b Hred.
apply OKOKstep; intros k.
pose proof (Ha (1 + k)) as [_ Hrec]; auto.
Qed.

Lemma OKstepOK : ∀ a, OK a → ∀ k, OKstep k a.
Proof.
intros a Ha k.
generalize a Ha; clear a Ha.
induction k; intros a Ha; inversion Ha; auto.
split; auto.
Qed.

Lemma term_ge_OK : ∀ k a, term_ge a k → Fsemantics.OK a → OKstep k (drop a).
Proof.
induction k; simpl; intros a ak OKa; [|split]; [apply V_drop; apply OKV; auto..|].
intros b Hred.
destruct (drop_red_exists _ _ _ ak Hred) as [? [? ?]]; subst.
apply IHk.
apply term_ge_red with (a := a); auto.
apply (Pred_OK); ∃ a; auto.
Qed.

Lemma jterm_aux : ∀ {M H Z G a t}, jterm M H Z G a t →
  ∀ Fa, drop Fa = a → Ftypesystem.jterm M H Z G Fa t.
Proof.
intros M H Z G a t HGat; induction HGat; intros Fa Faa;
destruct Fa; inversion Faa; eauto using Ftypesystem.jterm.
Qed.

Lemma jterm_aux_rev : ∀ {M H Z G a t},
  Ftypesystem.jterm M H Z G a t → jterm M H Z G (drop a) t.
Proof. intros M H Z G a t HGat; induction HGat; simpl; eauto using jterm. Qed.

Lemma jterm_sound : ∀ {H Z G a t}, jterm 2 H Z G a t → OK a.
Proof.
intros H Z G a t HZGat; apply OKOKstep; intros k.
pose proof (jterm_extract_jterm_env M12 HZGat) as HZG.
pose proof (jterm_env_extract_jerasable_env M12 HZG) as HZ.
pose proof (jterm_aux HZGat (fill k a) (drop_fill k a)) as HZGfat.
rewrite <- (drop_fill k a).
apply term_ge_OK; [apply term_ge_fill|].
pose proof (jerasable_env_sound HZ) as [h Hh]; auto.
pose proof (jterm_sound HZGfat h Hh) as Jfat.
pose proof (jterm_extract_jtype M12 HZGat) as Ht.
pose proof (C_CE (jtype_sound Ht h Hh)) as Cht.
eapply Pok_EJudg; [|apply Cht|apply Jfat].
apply (Forall_impl _ CEexp).
apply (jterm_env_sound HZG); auto.
Qed.

Print Assumptions jterm_sound.