Library EnumInt

Require Import Lists Equality Nat Enum.

Definition AppCross := R (.\"aC", "A", "B";
  "A" !Nil (.\"a", "A"; !Append ("aC" "A" "B") (!Map (.\"x"; !App "a" "x") "B"))).



Definition tlenc := @lenc term tenc.

Hint Unfold tlenc.


Lemma tlenc_lam B : lambda (tlenc B).

Proof.

  eapply lenc_lam.

Qed.


Lemma tlenc_cls B : closed (tlenc B).

Proof.

  eapply lenc_cls, tenc_cls.

Qed.


Hint Unfold Nil Cons : cbv.


Hint Resolve tlenc_lam tlenc_cls : cbv.

Hint Rewrite tlenc_cls : cbv.


Lemma AppCross_Nil B : AppCross Nil (tlenc B) == Nil.

Proof.

  crush.

Qed.


Lemma AppCross_Cons a A B : AppCross (tlenc (a::A)) (tlenc B) == Append ((lam (AppCross #0)) (tlenc A) (tlenc B)) (Map (lam (App (tenc a) #0)) (tlenc B)).

Proof.

  crush.

Qed.


Lemma AppCross_correct A B : AppCross (tlenc A) (tlenc B) == tlenc(appCross A B).

Proof.

  induction A.

  - now rewrite AppCross_Nil.

  - rewrite AppCross_Cons.
simpl.
    rewrite !Eta, IHA; value.
unfold tlenc; rewrite Map_correct; eauto with cbv.
    + rewrite Append_correct; eauto with cbv.

    + split; value.

      intros; rewrite <- App_correct.
crush.
Qed.


Definition Exh_size := R (.\ "Es", "s";
  "s" !I (.\ "s", "t"; !Add (!Add !(enc 1) ("Es" "s")) ("Es" "t")) (.\ "s"; (!Succ ("Es" "s")))).


Hint Unfold Exh_size : cbv.


Lemma Exh_size_var n : Exh_size (tenc #n) == enc n.

Proof.

  crush.

Qed.


Lemma Exh_size_app (s t : term) : Exh_size (tenc (s t))
   == Add (Add (enc 1) ((lam (Exh_size #0)) (tenc s))) ((lam (Exh_size #0)) (tenc t)).

Proof.

  crush.

Qed.


Lemma Exh_size_lam s : Exh_size (tenc (lam s)) == Succ ((lam(Exh_size #0)) (tenc s)).

Proof.

  crush.

Qed.


Lemma Exh_size_correct s : Exh_size (tenc s) == enc(exh_size s).

Proof.

  induction s.

  - now rewrite Exh_size_var.

  - now rewrite Exh_size_app, !Eta, IHs1, IHs2, !Add_correct; value.

  - now rewrite Exh_size_lam, !Eta, IHs, Succ_correct; value.

Qed.


Definition TT := R (.\ "TT", "n";
  "n" !(tlenc([#0]))
      (.\"n"; (!Append
              (!Append ("TT" "n") (!Cons (!Var (!Succ "n")) !Nil))
             (!Filter (.\"x"; (!Not (!(El Eq) "x" ("TT" "n"))))
               (!Append (!Map !Lam ("TT" "n"))
                       (!AppCross ("TT" "n") ("TT" "n"))
               )))
     )
).


Lemma TT_0 : TT (enc 0) == tlenc([#0]).

Proof.

  crush.

Qed.


Lemma TT_S n : TT (enc (S n)) == Append (Append ((lam(TT #0)) (enc n)) (Cons (Var (Succ (enc n))) Nil)) (Filter (lam(Not (El Eq #0 ((lam(TT #0)) (enc n))))) (Append (Map Lam ((lam(TT #0)) (enc n))) (AppCross ((lam(TT #0)) (enc n)) ((lam(TT #0)) (enc n))))).

Proof.

  crush.

Qed.


Lemma TT_correct n : TT (enc n) == tlenc(T n).

Proof with value; eauto with cbv; unfold tlenc.

  induction n...

  - now rewrite TT_0.

  - rewrite TT_S;
    rewrite Eta at 1; value.

    repeat rewrite Eta at 2; value.

    rewrite !IHn, AppCross_correct...

    rewrite (@Map_correct _ tenc tenc_lam tenc_cls lam)...

    rewrite Append_correct...

    remember (λ Not ((El Eq #0) ((λ TT #0) (enc n)))) as P.

    rewrite (@Filter_correct _ tenc tenc_lam tenc_cls P (fun x : term => ~ x el T n)); subst...

    rewrite Succ_correct, Var_correct.
change (Nil) with (tlenc nil)...
    rewrite Cons_correct...

    rewrite !Append_correct...
now rewrite <- app_assoc.
    + intros x.

      destruct El_correct with (s := x) (A := T n) (enc := tenc) (Eq := Eq)...

      * intros; decide (s = t); [left | right]; intuition; now eapply Eq_correct.

      * right; intuition.

        transitivity (Not (El Eq (tenc x) (TT (enc n)))).

        transitivity (Not (El Eq (tenc x) ((lam (TT #0)) (enc n)))).
crush.
        rewrite Eta, IHn, H0; value.
crush. rewrite IHn, H0. crush.
      * left; intuition.

        transitivity (Not (El Eq (tenc x) (TT (enc n)))).

        transitivity (Not (El Eq (tenc x) ((lam (TT #0)) (enc n)))).
crush.
        rewrite Eta, IHn, H0; value.
crush. rewrite IHn, H0. crush.
    + split; value.

      intros x.
eapply Lam_correct.
Qed.


Definition U : term := .\"n";
  (!Nth (!TT "n") "n") !I !(tenc #0).


Hint Unfold U : cbv.


Lemma U_correct n : U (enc n) == tenc(g_inv n).

Proof.

  transitivity (Nth (TT (enc n)) (enc n) I (tenc #0)).
crush.
  rewrite TT_correct.
unfold tlenc.
  rewrite Nth_correct; value.

  unfold g_inv, elAt, oenc.

  destruct (nth_error (T n) n); crush.

  intros; value.
intros; value.
Qed.