Require Export Eagerlet.
Require Export CBV.
Import CommaNotation.

Tactic Notation "asimpl" := CBV.auto_unfold; Syntax.auto_unfold; CBV.asimpl'; Syntax.asimpl'; CBV.auto_fold; Syntax.auto_fold.

Tactic Notation "asimpl" "in" hyp(H) := revert H; asimpl; intros H.

Scheme Value_ind_2 := Induction for Value Sort Prop
  with Exp_ind_2 := Induction for Exp Sort Prop.

Combined Scheme ExpVal_ind from Exp_ind_2, Value_ind_2.

Definition ctx_cbv (n : nat) := fin n -> type.

Reserved Notation "Gamma ⊩v V : A" (at level 80, V at level 99).
Reserved Notation "Gamma ⊢v V : A" (at level 80, V at level 99).

Inductive has_typeV : forall {n} (Gamma : ctx_cbv n), Value n -> type -> Type :=
| typeVarV n (Gamma : ctx_cbv n) x : Gamma ⊩v var_Value x : Gamma x
| typeOne n (Gamma : ctx_cbv n) : Gamma ⊩v One : Unit
| typeLam n (Gamma : ctx_cbv n) M A B : A .: Gamma ⊢v M : B -> Gamma ⊩v Lam M : Arr A B
| typePair n (Gamma : ctx_cbv n) V1 V2 A B : Gamma ⊩v V1 : A -> Gamma ⊩v V2 : B -> Gamma ⊩v Pair V1 V2 : Cross A B
| typeInjL n (Gamma : ctx_cbv n) b V A B : Gamma ⊩v V : (match b with |true => A |_ => B end) -> Gamma ⊩v Inj b V : Plus A B
where "Gamma ⊩v V : A" := (has_typeV Gamma V A)
with has_typeE : forall {n} (Gamma : ctx_cbv n), Exp n -> type -> Type :=
| typeVal n (Gamma : ctx_cbv n) V A : Gamma ⊩v V : A -> Gamma ⊢v Val V : A
| typeApp n (Gamma : ctx_cbv n) M N A B : Gamma ⊢v M : Arr A B -> Gamma ⊢v N: A -> Gamma ⊢v App M N : B
| typeCaseS n (Gamma : ctx_cbv n) M N1 N2 A B C : Gamma ⊢v M : Plus A B ->
    A, Gamma ⊢v N1 : C ->
    B, Gamma ⊢v N2 : C ->
                  Gamma ⊢v CaseS M N1 N2 : C
| typeCaseP n (Gamma : ctx_cbv n) M N A B C:
    Gamma ⊢v M : Cross A B ->
    B, A, Gamma ⊢v N : C ->
Gamma ⊢v CaseP M N : C
where "Gamma ⊢v E : A" := (has_typeE Gamma E A).

Fixpoint eval_ty (A : type) : valtype :=
  match A with
  | Unit => one
  | Arr A B => U (arrow (eval_ty A) (F (eval_ty B)))
  | Cross A B => cross (eval_ty A) (eval_ty B)
  | Plus A B => Sigma (eval_ty A) (eval_ty B)
  end.

Notation up_ren := (var_zero .: shift >> shift).
Notation up2_ren := (var_zero .: (shift (var_zero) .: shift >> shift >> shift)).

Fixpoint eval_val {n: nat} (V : Value n) : value n :=
  match V with
  | One => u
  | var_Value x => var_value x
  | Lam M => thunk (lambda (eval_exp M))
  | Pair V1 V2 => pair (eval_val V1) (eval_val V2)
  | Inj b V => inj b (eval_val V)
  end
with eval_exp {n: nat} (M: Exp n) : comp n :=
  match M with
  | Val V => ret (eval_val V)
  | App M N => $$ <- eval_exp M;
              $$ <- (eval_exp N)⟨↑⟩;
              app (force (var_value (shift var_zero))) (var_value var_zero)
  | CaseS M N1 N2 => $$ <- eval_exp M;
                      caseS (var_value var_zero) ((eval_exp N1)⟨up_ren⟩) ((eval_exp N2)⟨up_ren⟩)
  | CaseP M N => $$ <- eval_exp M;
                  caseP (var_value var_zero) ((eval_exp N)⟨up2_ren⟩)
  end.

Fixpoint typingVal_pres {n} (Gamma : ctx_cbv n) V A (H : Gamma ⊩v V : A) :
  value_typing (Gamma >> eval_ty) (eval_val V) (eval_ty A)
with typingExp_pres {n} (Gamma : ctx_cbv n) M A (H: Gamma ⊢v M : A) :
  computation_typing (Gamma >> eval_ty) (eval_exp M) (F (eval_ty A)).
Proof.
  - destruct H; cbn; try (now (repeat constructor)).
    + constructor.
      constructor. specialize (typingExp_pres _ _ _ _ h).
      now asimpl in *.
    + constructor; now apply typingVal_pres.
    + constructor.
    destruct b; now apply typingVal_pres.
  - destruct H; cbn.
    + specialize (typingVal_pres _ _ _ _ h).
      constructor. assumption.
    + simpl.
      eapply eagerlet_ty; eauto.
      eapply eagerlet_ty; eauto using comp_typepres_renaming.
      econstructor.
      * cbv; eauto.
      * cbv; eauto.
    + eapply eagerlet_ty; eauto.
      econstructor; cbn; eauto; simpl.
      * cbv; eauto.
      * eapply comp_typepres_renaming; eauto.
        auto_case.
      * eapply comp_typepres_renaming; eauto.
        auto_case.
    + eapply eagerlet_ty; eauto.
      econstructor; eauto.
      * cbv; eauto.
      * eapply comp_typepres_renaming; eauto.
        auto_case.
Qed.

Lemma trans_ren_val':
  forall m,
    (forall (M: Exp m), forall n (xi : fin m -> fin n), eval_exp (M⟨xi⟩) = (eval_exp M)⟨xi⟩)
    /\ (forall (V: Value m), forall n (xi : fin m -> fin n), eval_val (V⟨xi⟩) = (eval_val V)⟨xi⟩).
Proof.
  apply ExpVal_ind; intros; simpl; asimpl; try congruence.
  + rewrite H, H0, !eagerlet_rencomp.
    now asimpl.
  + rewrite H, H0, H1, !eagerlet_rencomp.
    now asimpl.
  + rewrite H, H0, !eagerlet_rencomp.
    now asimpl.
Qed.

Lemma trans_ren_val :
  forall m,
    (forall (V: Value m), forall n (xi : fin m -> fin n), eval_val (V⟨xi⟩) = (eval_val V)⟨xi⟩).
Proof. now apply trans_ren_val'. Qed.

Lemma trans_ren_exp :
  forall m,
    (forall (M: Exp m), forall n (xi : fin m -> fin n), eval_exp (M⟨xi⟩) = (eval_exp M)⟨xi⟩).
Proof. now apply trans_ren_val'. Qed.

Lemma trans_subst_val':
  forall m,
    (forall (M: Exp m), forall n (sigma : fin m -> Value n), eval_exp (M[sigma]) = (eval_exp M)[sigma >> eval_val])
    /\ (forall (V: Value m), forall n (sigma : fin m -> Value n), eval_val (V[sigma]) = (eval_val V)[sigma >> eval_val]).
Proof.
  apply ExpVal_ind; intros; simpl; asimpl; try congruence.
  + reflexivity.
  + repeat f_equal. rewrite H.
    asimpl. repeat f_equal.
    fext. intros x. apply trans_ren_val.
  + rewrite H, H0, !eagerlet_substcomp.
    now asimpl.
  + rewrite H, H0, H1, !eagerlet_substcomp.
    asimpl. repeat f_equal.
    * fext. intros x. unfold funcomp. rewrite trans_ren_val. now asimpl.
    * fext. intros x. unfold funcomp. rewrite trans_ren_val. now asimpl.
  + rewrite H, H0, !eagerlet_substcomp.
    asimpl; repeat f_equal.
    fext. intros x. unfold funcomp. simpl. rewrite trans_ren_val. now asimpl.
Qed.

Lemma trans_subst_val:
  forall m,
    (forall (V: Value m), forall n (sigma : fin m -> Value n), eval_val (V[sigma]) = (eval_val V)[sigma >> eval_val]).
Proof.
  apply trans_subst_val'.
Qed.

Lemma trans_subst_exp:
  forall m,
    (forall (M: Exp m), forall n (sigma : fin m -> Value n), eval_exp (M[sigma]) = (eval_exp M)[sigma >> eval_val]).
Proof.
  apply trans_subst_val'.
Qed.

Require Import CBN.CBN_CBPV.

Lemma injective_shift n: injective (@shift n).
Proof. intros x y H. unfold shift in *. congruence. Qed.

Lemma injective_renup n: injective (@var_zero (S n) .: shift >> shift).
Proof. intros [] [] H; unfold shift, funcomp in *; simpl in *; try congruence.
       inv H. inv H. Qed.

Ltac smartinv := match goal with
                 | [ H : context [($$ <- ?M; ?N)] |- _] => destruct M; inv H
                 end.

Ltac letc_step_inv := match goal with
                        [ H: context [$$ <- ?M; ?N] |- _] => ( destruct (eagerlet_inv M N) as [ [HH ?] | (? & ? & HH) ]); [rewrite HH in H; clear HH|rewrite HH in H; clear HH]
                      end.

Lemma injective_eval:
 forall n, (forall (M N: Exp n), eval_exp M = eval_exp N -> M = N) /\ (forall (U V: Value n), eval_val U = eval_val V -> U = V).
Proof with try (now repeat smartinv).
  apply ExpVal_ind; intros; try (destruct V; simpl in *; try congruence; inv H; f_equal; auto); simpl in *.
  all: try (destruct V; cbn in *; try (inv H0); try (inv H1); repeat f_equal; eauto).
  - destruct N; cbn in *...
   inv H0. f_equal. eauto.
  - destruct N; cbn in *...
    repeat letc_step_inv; try discriminate; asimpl in H1.
    all: inv H1; f_equal; eauto.
    all: try (eapply H0); try eapply H.
    all: try (now ( eapply ren_inj; eauto using injective_shift; congruence)).
    all: try now (try (destruct x0); try (destruct x); inv H4).
    + eapply ren_inj in H4; eauto using injective_shift.
      subst; congruence.
    + clear - e2 e4 H4.
      destruct e0; inv e2; asimpl in H4; try (repeat letc_step_inv; discriminate).
      destruct N2; inv e4; asimpl in H4; try (repeat letc_step_inv; discriminate).
      cbn. congruence.
  - destruct N; cbn in *...
    repeat letc_step_inv; try discriminate.
    + inv H2. f_equal; eauto using ren_inj.
      * eapply H0. eapply ren_inj; eauto using injective_renup.
      * eapply H1. eapply ren_inj; eauto using injective_renup.
    + inv H2. rewrite <- e3 in e2. asimpl in H5. asimpl in H6. f_equal; eauto.
  - destruct N; cbn in *...
    letc_step_inv; letc_step_inv; try discriminate.
    + inv H1. f_equal; eauto using ren_inj. eapply H0. eapply ren_inj; eauto.
      intros [ []|] [ [] |] ?H; now try inv H1.
    + inv H1. rewrite <- e2 in e1. asimpl in H4. f_equal; eauto.
Qed.