Library examples

Require Import Llanguage.
Require Import typesystem.
Require Import typesystemequiv.
Require Import Ltypesystem.
Require Import Lsoundness.

Definition term_id := Lam (Var_x 0).
Definition type_id := For 1 (Scons (Spair 0 (Var_a 0) Top) Snil) (Arr (Var_a 0) (Var_a 0)).

Definition term_delta := Lam (App (Var_x 0) (Var_x 0)).
Definition type_delta := For 1 Snil (Mu (Arr (Var_a 0) (Var_a 1))).

Definition term_omega := App term_delta term_delta.
Definition type_omega := For 1 Snil (Var_a 0).

Ltac help := simpl;
  repeat (simpl; match goal with
    | |- 1 ≤ 0 → _ ⇒ let H := fresh "H" in intros H; inversion H
  end; auto); auto.

Lemma jterm_0_id : jterm 0 0 nil nil term_id type_id.
Proof.
apply JCoer with 1 (cons (Var_a 0, Top) nil) (Arr (Var_a 0) (Var_a 0)); help.
  apply JCGen with (Scons Top Snil) (cons Top nil); help; repeat constructor.
  apply JLam; simpl; [intros _; apply JTVar|apply JVar]; help.
Qed.

Lemma jterm_env_1 : jterm_env 1 0 nil nil.
Proof. split; [intros _; apply JEnil|constructor]. Qed.

Lemma jterm_2_id : jterm 2 0 nil nil term_id type_id.
Proof. apply jterm_up_2; apply jterm_up_1; [apply jterm_0_id|apply jterm_env_1]. Qed.

Lemma OK_term_id : OK term_id.
Proof. apply (jterm_sound jterm_2_id). Qed.

Lemma jwf_delta : jwf 0 (Arr (Var_a 0) (Var_a 1)) WF.
Proof. apply WFArr; [apply WFVar|apply WFne]; apply WFwf with (Var_a 0); auto. Qed.

Lemma jterm_0_delta : jterm 0 0 nil nil term_delta type_delta.
Proof.
remember (Mu (Arr (Var_a 0) (Var_a 1))) as mu.
pose proof jwf_delta.
assert (jtype 0 1 nil mu)
  by (unfold jtype; subst mu; apply JTMu; help; apply JTArr; apply JTVar).
apply JCoer with 1 nil (Arr mu (Var_a 0)); help.
  apply (JCTrans _ 0 1 _ nil nil) with mu.
simpl.
    replace (Arr mu (Var_a 0)) with (subst1 mu 0 (Arr (Var_a 0) (Var_a 1))) by (subst mu; reflexivity).
    subst mu; apply JCFold; auto.
    subst mu; apply JCGen with (Scons Top Snil) (cons Top nil); help; repeat constructor.
  apply JLam; auto.
  remember (cons mu nil) as G.
  apply JApp with mu.
    apply JCoer with 0 nil mu; help.
      subst mu; apply JCUnfold; help.
      subst G; apply JVar; tryomega.
    subst G; apply JVar; tryomega.
Qed.

Lemma jterm_2_delta : jterm 2 0 nil nil term_delta type_delta.
Proof. apply jterm_up_2; apply jterm_up_1; [apply jterm_0_delta|apply jterm_env_1]. Qed.

Lemma term_omega_red : red term_omega term_omega.
Proof. apply RedApp. Qed.