From stdpp Require Import gmap base relations tactics.
From iris Require Import prelude.
From semantics.ts.stlc Require Import lang notation.
From semantics.ts.stlc Require untyped types.


(** README: Please also download the assigment sheet as a *.pdf from here:
            https://cms.sic.saarland/semantics_ws2324/materials/
            It contains additional explanation and excercises. **)

(** ** Exercise 1: Prove that the structural and contextual semantics are equivalent. *)
(** You will find it very helpful to separately derive the structural rules of the
  structural semantics for the contextual semantics. *)


Ltac ectx_step K :=
  eapply (Ectx_step _ _ K); subst; eauto.

Lemma contextual_step_beta x e e':
  is_val e' → contextual_step ((λ: x, e) e') (subst' x e' e).
Proof.
  intro H_val.
  ectx_step HoleCtx.
Qed.


Lemma contextual_step_app_r (e1 e2 e2': expr) :
  contextual_step e2 e2' →
  contextual_step (e1 e2) (e1 e2').
Proof.
  intro H_step.
  inversion H_step.
  induction K eqn:H_K.
  (* I am a smart foxxo >:3 *)
  all: ectx_step (AppRCtx e1 K).
Qed.

Ltac is_val_to_val v H :=
  rewrite (is_val_spec _) in H; destruct H as [v H]; apply of_to_val in H; symmetry in H.

Lemma contextual_step_app_l (e1 e1' e2: expr) :
  is_val e2 →
  contextual_step e1 e1' →
  contextual_step (e1 e2) (e1' e2).
Proof.
  intros H_val H_step.
  is_val_to_val v H_val.
  subst.

  inversion H_step.
  induction K eqn:H_K.
  all: ectx_step (AppLCtx K v).
Qed.

Lemma contextual_step_plus_red (n1 n2 n3: Z) :
  (n1 + n2)%Z = n3 →
  contextual_step (n1 + n2)%E n3.
Proof.
  intro H_plus.
  ectx_step HoleCtx.
Qed.


Lemma contextual_step_plus_r e1 e2 e2' :
  contextual_step e2 e2' →
  contextual_step (Plus e1 e2) (Plus e1 e2').
Proof.
  intro H_step.
  inversion H_step.
  ectx_step (PlusRCtx e1 K).
Qed.


Lemma contextual_step_plus_l e1 e1' e2 :
  is_val e2 →
  contextual_step e1 e1' →
  contextual_step (Plus e1 e2) (Plus e1' e2).
Proof.
  intro H_val.
  is_val_to_val v H_val.
  intro H_step.
  inversion H_step.
  ectx_step (PlusLCtx K v).
Qed.


(** We register these lemmas as hints for [eauto]. *)
#[global]
Hint Resolve contextual_step_beta contextual_step_app_l contextual_step_app_r contextual_step_plus_red contextual_step_plus_l contextual_step_plus_r : core.

Ltac step_ind H := induction H as [
  name e_λ e_v
  | e_fn e_fn' e_v H_val H_fn_step IH
  | e_fn e_arg e_arg' H_arg_step IH
  | n1 n2 n_sum H_plus
  | e_l e_l' e_r H_val H_l_step IH
  | e_l e_r e_r' H_r_step IH
].

Lemma step_contextual_step e1 e2: step e1 e2 → contextual_step e1 e2.
Proof.
  intro H_step.
  step_ind H_step; eauto.
Qed.


(** Now the other direction. *)
(* You may find it helpful to introduce intermediate lemmas. *)


Lemma contextual_step_step e1 e2:
  contextual_step e1 e2 → step e1 e2.
Proof.
  intro H_cstep.
  inversion H_cstep as [K e1' e2' H_eq1 H_eq2 H_bstep]; subst.
  inversion H_bstep as [
    name body arg H_val H_eq1 H_eq2 H_eq3
    | e1 e2 n1 n2 n_sum H_n1 H_n2 H_sum H_eq1 H_eq2
  ]; subst.
  (*
    Here we do an induction on K, and we let eauto solve it for us.
    In practice, each case of the induction on K can be solved quite easily,
    as the induction hypothesis has us prove a `contextual_step`, for which we have plenty of useful lemmas.
  *)
  all: induction K; unfold fill; eauto.
Qed.



(** ** Exercise 2: Scott encodings *)
Section scott.
  (* take a look at untyped.v for usefull lemmas and definitions *)
  Import semantics.ts.stlc.untyped.

  (** Scott encoding of Booleans *)
  Definition true_scott : val := (λ: "t" "f", "t").
  Definition false_scott : val := (λ: "t" "f", "f").

  (* Lemma steps_beta e_λ e_arg *)
  Ltac rtc_single step_cons := eapply rtc_l; last reflexivity; eapply step_cons; auto.

  Lemma true_red (v1 v2 : val) :
    closed [] v1 →
    closed [] v2 →
    rtc step (true_scott v1 v2) v1.
  Proof.
    intros H_cl1 H_cl2.
    unfold true_scott.
    etransitivity.
    eapply steps_app_l; auto.
    rtc_single StepBeta.
    simpl.
    etransitivity.
    rtc_single StepBeta.
    simpl.
    rewrite subst_closed_nil; auto.
    reflexivity.
  Qed.

  Lemma steps_plus_r (e1 e2 e2': expr) :
    rtc step e2 e2' → rtc step (e1 + e2)%E (e1 + e2')%E.
  Proof.
    induction 1; subst.
    reflexivity.
    etransitivity; last exact IHrtc.
    rtc_single StepPlusR.
  Qed.

  Lemma steps_plus_l (e1 e1' e2: expr) :
    is_val e2 →
    rtc step e1 e1' →
    rtc step (e1 + e2)%E (e1' + e2)%E.
  Proof.
    induction 2; subst.
    reflexivity.
    etransitivity; last exact IHrtc.
    rtc_single StepPlusL.
  Qed.

  Lemma lam_is_val name e_body :
    is_val (Lam name e_body).
  Proof.
    unfold is_val.
    intuition.
  Qed.

  Lemma int_is_val n :
    is_val (LitInt n).
  Proof.
    unfold is_val.
    intuition.
  Qed.

  Hint Resolve lam_is_val int_is_val: core.

  (* TODO: recursively traverse the goal for subst instances? *)
  Ltac auto_subst :=
    (rewrite subst_closed_nil; last assumption) ||
    (unfold subst'; unfold subst; simpl; fold subst).

  (* This is ridiculously powerful, although it only works when you know all the terms *)
  Ltac auto_step :=
    match goal with
      | [ |- rtc step (App ?e_l ?e_v) ?e_target ] =>
        etransitivity;
        first eapply steps_app_r;
        first auto_step;
        simpl;
        etransitivity;
        first eapply steps_app_l;
        first auto;
        first auto_step;
        simpl;
        repeat auto_subst;
        rtc_single StepBeta;
        simpl;
        done
      | [ |- rtc step (of_val ?v) ?e_target ] => reflexivity
      | [ |- rtc step (Lam ?name ?body) ?e_target ] => reflexivity
      | [ |- rtc step (LitInt ?n) ?e_target ] => reflexivity
      | [ |- rtc step (Plus ?e1 ?e2) ?e_target ] =>
        etransitivity;
        first eapply steps_plus_r;
        first auto_step;
        etransitivity;
        first eapply steps_plus_l;
        first auto;
        first auto_step;
        rtc_single StepPlusRed;
        done
      | [ |- rtc step (subst ?var ?thing) ?e_target ] =>
        repeat auto_subst;
        auto_step
    end
  .

  Ltac multi_step :=
    repeat (reflexivity || (
      etransitivity;
      first auto_step;
      first repeat auto_subst
    )).

  Lemma false_red (v1 v2 : val) :
    closed [] v1 →
    closed [] v2 →
    rtc step (false_scott v1 v2) v2.
  Proof.
    intros H_cl1 H_cl2.
    auto_step.
  Qed.


  (** Scott encoding of Pairs *)
  Definition pair_scott : val := (λ: "lhs" "rhs" "f", ("f" "lhs" "rhs")).

  Definition fst_scott : val := (λ: "pair", ("pair" (λ: "lhs" "rhs", "lhs"))).
  Definition snd_scott : val := (λ: "pair", ("pair" (λ: "lhs" "rhs", "rhs"))).

  Lemma fst_red (v1 v2 : val) :
    is_closed [] v1 →
    is_closed [] v2 →
    rtc step (fst_scott (pair_scott v1 v2)) v1.
  Proof.
    intros H_cl1 H_cl2.
    multi_step.
  Qed.

  Lemma snd_red (v1 v2 : val) :
    is_closed [] v1 →
    is_closed [] v2 →
    rtc step (snd_scott (pair_scott v1 v2)) v2.
  Proof.
    intros H_cl1 H_cl2.
    multi_step.
  Qed.
End scott.

Import semantics.ts.stlc.types.

(** ** Exercise 3: type erasure *)
(** Source terms *)
Inductive src_expr :=
| ELitInt (n: Z)
(* Base lambda calculus *)
| EVar (x : string)
| ELam (x : binder) (A: type) (e : src_expr)
| EApp (e1 e2 : src_expr)
(* Base types and their operations *)
| EPlus (e1 e2 : src_expr).

(** The erasure function *)
Fixpoint erase (E: src_expr) : expr :=
  match E with
  | ELitInt n => LitInt n
  | EVar x => Var x
  | ELam x A e => Lam x (erase e)
  | EApp e1 e2 => App (erase e1) (erase e2)
  | EPlus e1 e2 => Plus (erase e1) (erase e2)
  end.

Reserved Notation "Γ '⊢S' e : A" (at level 74, e, A at next level).
Inductive src_typed : typing_context → src_expr → type → Prop :=
| src_typed_var Γ x A :
    Γ !! x = Some A →
    Γ ⊢S (EVar x) : A
| src_typed_lam Γ x E A B :
    (<[ x := A]> Γ) ⊢S E : B →
    Γ ⊢S (ELam (BNamed x) A E) : (A → B)
| src_typed_int Γ z :
    Γ ⊢S (ELitInt z) : Int
| src_typed_app Γ E1 E2 A B :
    Γ ⊢S E1 : (A → B) →
    Γ ⊢S E2 : A →
    Γ ⊢S EApp E1 E2 : B
| src_typed_add Γ E1 E2 :
    Γ ⊢S E1 : Int →
    Γ ⊢S E2 : Int →
    Γ ⊢S EPlus E1 E2 : Int
where "Γ '⊢S' E : A" := (src_typed Γ E%E A%ty) : FType_scope.
#[export] Hint Constructors src_typed : core.

Lemma type_erasure_correctness Γ E A:
  (Γ ⊢S E : A)%ty → (Γ ⊢ erase E : A)%ty.
Proof.
  intro H_styped.
  induction H_styped; unfold erase; eauto.
Qed.


(** ** Exercise 4: Unique Typing *)
Lemma src_typing_unique Γ E A B:
  (Γ ⊢S E : A)%ty → (Γ ⊢S E : B)%ty → A = B.
Proof.
  intro H_typed.
  revert B.
  induction H_typed as [
    Γ x A H_x_ty
    | Γ x e_body A1 A2 H_body_ty IH
    | Γ n
    | Γ e_fn e_arg A1 A2 H_fn_ty H_arg_ty IH
    | Γ e1 e2 H_e1_ty H_e2_ty
  ]; intro B; intro H_typed'.
  all: inversion H_typed' as [
    Γ' y B' H_y_ty
    | Γ' y e_body' B1 B2 H_body_ty'
    | Γ' n'
    | Γ' e_fn' e_arg' B1 B2 H_fn_ty' H_arg_ty'
    | Γ' e3 e4 H_e3_ty H_e4_ty
  ]; subst; try auto.
  - rewrite H_y_ty in H_x_ty; injection H_x_ty.
    intuition.
  - rewrite (IH B2); eauto.
  - remember (H_arg_ty _ H_fn_ty') as H_eq.
    injection H_eq.
    intuition.
Qed.

Lemma syn_typing_not_unique:
  ∃ (Γ: typing_context) (e: expr) (A B: type),
  (Γ ⊢ e: A)%ty ∧ (Γ ⊢ e: B)%ty ∧ A ≠ B.
Proof.
  exists ∅.
  exists (λ: "x", "x")%E.
  exists (Int → Int)%ty.
  exists ((Int → Int) → (Int → Int))%ty.
  repeat split.
  3: discriminate.
  all: apply typed_lam; eauto.
Qed.

(** ** Exercise 5: Type Inference *)

Fixpoint type_eq A B :=
  match A, B with
  | Int, Int => true
  | Fun A B, Fun A' B' => type_eq A A' && type_eq B B'
  | _, _ => false
  end.

Lemma type_eq_iff A B: type_eq A B ↔ A = B.
Proof.
  induction A in B |-*; destruct B; simpl; naive_solver.
Qed.

Notation ctx := (gmap string type).
Fixpoint infer_type (Γ: ctx) E :=
  match E with
  | EVar x => Γ !! x
  | ELam (BNamed x) A E =>
    match infer_type (<[x := A]> Γ) E with
    | Some B => Some (Fun A B)
    | None => None
    end
  (* TODO: complete the definition for the remaining cases *)
  | ELitInt l => Some (Int) (* TODO *)
  | EApp E1 E2 => match infer_type Γ E1, infer_type Γ E2 with
    | Some (Fun A B), Some A' => (if type_eq A A' then Some B else None)
    | _, _ => None
    end
  | EPlus E1 E2 => match infer_type Γ E1, infer_type Γ E2 with
    | Some Int, Some Int => Some Int
    | _, _ => None
    end
  | ELam BAnon A E => None
  end.

Ltac destruct_match H H_eq :=
  repeat match goal with
  | [H: match ?matcher with _ => _ end = Some _ |- _] =>
    induction matcher eqn:H_eq; try discriminate H
  end.

(** Prove both directions of the correctness theorem. *)
Lemma infer_type_typing Γ E A:
  infer_type Γ E = Some A → (Γ ⊢S E : A)%ty.
Proof.
  revert Γ A.
  induction E; intros Γ B H_infer; inversion H_infer; subst; eauto.
  - destruct_match H0 H_x.
    destruct_match H0 H_eq.
    injection H0; intro H_eq'.
    subst.
    eapply src_typed_lam.
    exact (IHE _ _ H_eq).
  - destruct_match H0 H_E1.
    destruct_match H0 H_a.
    destruct_match H0 H_E2.
    destruct_match H0 H_eq.
    clear IHt1 IHt2.
    apply Is_true_eq_left in H_eq.
    rewrite type_eq_iff in H_eq.
    injection H0; intro H_eq'.
    subst.
    eapply src_typed_app.
    exact (IHE1 _ _ H_E1).
    exact (IHE2 _ _ H_E2).
  - destruct_match H0 H_E1.
    destruct_match H0 H_a.
    destruct_match H0 H_E2.
    rename a0 into b.
    destruct_match H0 H_b.
    injection H0; intro H_eq.
    subst.
    eapply src_typed_add.
    exact (IHE1 _ _ H_E1).
    exact (IHE2 _ _ H_E2).
Qed.


Lemma typing_infer_type Γ E A:
  (Γ ⊢S E : A)%ty → infer_type Γ E = Some A.
Proof.
  intro H_typed.
  induction H_typed; simpl; try eauto.
  - induction (infer_type (<[x := A]> Γ) E) eqn:H1; try discriminate IHH_typed.
    rewrite H1.
    injection IHH_typed; intro H_eq.
    rewrite H_eq.
    intuition.
  - induction (infer_type Γ E1) eqn:H1; try discriminate IHH_typed1.
    injection IHH_typed1; intro H_eq; subst.
    induction (infer_type Γ E2) eqn:H2; try discriminate IHH_typed2.
    injection IHH_typed2; intro H_eq; subst.
    destruct (type_eq A A) eqn:H_AA.
    + reflexivity.
    + (* idk why I struggled so much to manipulate H_AA *)
      assert (A = A) as H_AA_true by reflexivity.
      rewrite <-type_eq_iff in H_AA_true.
      apply Is_true_eq_true in H_AA_true.
      rewrite H_AA_true in H_AA.
      discriminate H_AA.
  - induction (infer_type Γ E1) eqn:H1; try discriminate IHH_typed.
    injection IHH_typed1; intro H_eq; subst.
    induction (infer_type Γ E2) eqn:H2; try discriminate IHH_typed2.
    injection IHH_typed2; intro H_eq; subst.
    + reflexivity.
    + discriminate IHH_typed1.
Qed.



(** ** Exercise 6: untypable, safe term *)

(* The exercise asks you to:
  "Give one example if there is such an expression, otherwise prove their non-existence."
  So either finish one section or the other.
*)

Section give_example.
  Definition omega : expr := (λ: "x", "x" "x").
  (* This is simply binding Ω to a variable, without using it. *)
  Definition ust : expr := ((λ: "x" "y", "y") (λ: "_", omega omega) 1)%E.

  Lemma ust_safe e':
    rtc step ust e' → is_val e' ∨ reducible e'.
  Proof.

    intro H_steps.
    assert (e' = 1 ∨ e' = ((λ: "y", "y") 1)%E ∨ e' = ust).
    {
      refine (rtc_ind_r (λ (e: expr), e = 1 ∨ e = ((λ: "y", "y") 1)%E ∨ e = ust) ust _ _ _ H_steps).
      - right; right; reflexivity.
      - intros y z H_steps' H_step_yz H_y.
        destruct H_y; subst; try val_no_step.
        destruct H; subst.
        + inversion H_step_yz; subst; try val_no_step; simpl.
          left; reflexivity.
        + inversion H_step_yz; subst; try val_no_step; simpl.
          inversion H3; subst; try val_no_step; simpl.
          right; left; reflexivity.
    }
    destruct H as [ H | [ H | H ]].
    - left.
      rewrite H.
      unfold is_val; intuition.
    - right.
      exists 1.
      subst.
      apply StepBeta.
      unfold is_val; intuition.
    - right.
      exists ((λ: "y", "y") 1)%E.
      subst.
      apply StepAppL.
      unfold is_val; intuition.
      apply StepBeta.
      unfold is_val; intuition.
  Qed.

  Lemma rec_type_contra A B:
    (A → B)%ty = A -> False.
  Proof.
    revert B.
    induction A.
    - intros B H_eq.
      discriminate H_eq.
    - intros B H_eq.
      injection H_eq.
      intros H_eqb H_eqA1.
      eapply IHA1.
      exact H_eqA1.
  Qed.

  Lemma ust_no_type Γ A:
    ¬ (Γ ⊢ ust : A)%ty.
  Proof.
    intro H_typed.
    inversion H_typed; subst; rename H2 into H_typed_let_omega.
    inversion H_typed_let_omega; subst; rename H5 into H_typed_lambda_omega.
    inversion H_typed_lambda_omega; subst; rename H5 into H_typed_omega_omega.
    inversion H_typed_omega_omega; subst; rename H6 into H_typed_omega.
    inversion H_typed_omega; subst; rename H6 into H_typed_omega_inner.
    inversion H_typed_omega_inner; subst.
    rename H5 into H_typed_x.
    rename H7 into H_typed_x'.
    inversion H_typed_x; subst; clear H_typed_x; rename H1 into H_typed_x.
    inversion H_typed_x'; subst; clear H_typed_x'; rename H1 into H_typed_x'.
    rewrite lookup_insert in H_typed_x.
    rewrite lookup_insert in H_typed_x'.
    injection H_typed_x; intro H_eq1.
    injection H_typed_x'; intro H_eq2.
    rewrite H_eq1 in H_eq2.
    exact (rec_type_contra _ _ H_eq2).
  Qed.

End give_example.

(* Section prove_non_existence.
  Lemma no_ust :
  ∀ e, (∀ e', rtc step e e' → is_val e' ∨ reducible e') → ∃ A, (∅ ⊢ e : A)%ty.
  Proof.
  Admitted.

End prove_non_existence. *)