(*Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".*)
From Coq Require Import Strings.String.
(*
From PLF Require Import Maps.
From PLF Require Import Smallstep.*)
From Coq Require Import Unicode.Utf8.
From Equations Require Import Equations.
Require Import Notations.
Require Import Ltac.
Require Import Logic.
Require Import Specif.
From Coq Require Import Arith.Arith.
From Coq Require Import Bool.Bool.
Require Export Coq.Strings.String.
From Coq Require Import Logic.FunctionalExtensionality.
From Coq Require Import Lists.List.
Import ListNotations.
Require Import Coq.Logic.FunctionalExtensionality.


(* types *)
Inductive ty : Type :=
  | Ty_Base : ty
  | Ty_Arrow : ty -> ty -> ty.

(* terms *)
Inductive tm : Type :=
  | tm_var : string -> tm
  | tm_app : tm -> tm -> tm
  | tm_abs : string -> ty -> tm -> tm.

Notation "<{ e }>" := e (e at level 99).
Notation "S --> T" := (Ty_Arrow S T) (at level 60, right associativity).
Notation "x ** y" := (tm_app x y) (at level 1, left associativity).
Notation "\\ x :: t , y" :=
  (tm_abs x t y) (at level 90 , x at level 99,
                 t at level 99, y at level 99,
                     left associativity).


Definition eqb_string (x y : string) : bool :=
  if string_dec x y then true else false.

(* substitution *)
Fixpoint subst (x :string) (s :tm) (t :tm) : tm :=
  match t with
  | tm_var y =>
      if eqb_string x y then s else t
  | tm_abs y T t1 =>
      if eqb_string x y then t else (tm_abs y T (subst x s t1))
  | tm_app t1 t2 =>
      tm_app (subst x s t1) (subst x s t2)
  end.

(* beta-reduction *)
Inductive reduction : tm -> tm -> Prop :=
  | Red_AppAbs : ∀ x T2 t1 v2,
         reduction (tm_app (tm_abs x T2 t1) v2) (subst x v2 t1)
  | Red_App1 : ∀ t1 t1' t2,
         reduction t1 t1' ->
         reduction (tm_app t1 t2) (tm_app t1' t2)
  | Red_App2 : ∀ t1 t2 t2',
         reduction t2 t2' ->
         reduction (tm_app t1 t2) (tm_app t1 t2') 
  | Red_Abs :  ∀ x v1 t2 t2',
         reduction t2 t2' ->
         reduction (tm_abs x v1 t2) (tm_abs x v1 t2'). 

(*not used*)
Lemma ty_sameness1 : forall A B C: ty, Ty_Arrow A B = Ty_Arrow A C -> B=C.
Proof.
  intros.
  inversion H.
  auto.
Qed.

(*auxiliary lemma*)
Lemma ty_sameness2 : forall A B C D: ty, Ty_Arrow A B = Ty_Arrow C D -> A=C -> B=D.
Proof.
  intros.
  inversion H.
  auto.
Qed.

(*auxiliary lemma*)
Lemma ty_sameness3 : forall A B C: ty,  B=C ->  Ty_Arrow A B = Ty_Arrow A C.
Proof.
  intros.
  now rewrite H.
Qed.

(*auxiliary lemma*)
Lemma ty_sameness4 : forall A B C D: ty,  Ty_Arrow A B = Ty_Arrow C D -> A=C /\ B=D.
Proof.
  intros.
  now inversion H.
Qed.

(* We want to define parial maps first, then will define contexts *)
Definition total_map (A : Type) := string → A.
Definition t_update {A : Type} (m : total_map A)
                    (x : string) (v : A) :=
  fun x' => if eqb_string x x' then v else m x'.
Definition partial_map (A : Type) := total_map (option A).
Definition update {A : Type} (m : partial_map A)
           (x : string) (v : A) :=
  (t_update m x (Some v)).

(* context *)
Definition context := partial_map ty.

(* derivaion rules [context and judgments] *)
Inductive has_type : context → tm → ty → Prop :=
  | T_Var : ∀ Gamma x T1,
      eq (Gamma x) (Some T1) →
      has_type Gamma (tm_var x) T1
  | T_Abs : ∀ Gamma x T1 T2 t1,
      has_type (update Gamma x T2) t1 T1 →        
      has_type Gamma (tm_abs x T2 t1) (Ty_Arrow T2  T1)
  | T_App : ∀ T1 T2 Gamma t1 t2,
      has_type Gamma t1 (Ty_Arrow T2 T1) →
      has_type Gamma t2  T2 →
      has_type Gamma (tm_app t1 t2) T1
.

(* In the above system, an expression like Gamma, x:T1, x:T2 
[formally this is update ((update Gamma x T1)x T2)] is allowed.
However, many textbooks define contexts such that when we have Gamma, x:T1,
then x is assumed to be a fresh variable.
The following axiom forces this property. 
 *)

Axiom well_formedness_of_context: forall (Gamma: context) (x:string) (t:tm)(T1 T2:ty),
                has_type (update Gamma x T1) t T2 -> (Gamma x)=None.


(*auxiliary lemma*)
Lemma tru_fal: true=false -> 0<>0.
Proof.
intuition.
Qed.

(*auxiliary lemma*)
Lemma eqb_st_xx: forall x:string, (eqb_string x x) = true.
Proof.
  intros.
  unfold eqb_string.
  case_eq (string_dec x x).
    - intros;auto.
    - intros.
      intuition.
Qed.

(*auxiliary lemma*)
Lemma eqb_st_xy: forall x y:string, ~x=y -> (eqb_string x y) = false.
Proof.
  intros.
  unfold eqb_string.
  case_eq (string_dec x y).
    - intros;auto;intuition.
    - intros;auto.
Qed.

(*auxiliary lemma*)
Lemma t_update_eq : ∀ (A : Type) (m : total_map A) x v,
  (t_update m x v) x = v.
Proof.
  intros.
  unfold t_update.
  case_eq (eqb_string x x).
    -  intros;auto.
    -  rewrite eqb_st_xx.
       intro.
       apply tru_fal in H.
       intuition.
Qed.

(*auxiliary lemma*)
Lemma t_update_neq : ∀ (A : Type) (m : total_map A) (x y:string) v,
  ~x=y -> (t_update m x v) y = m y.
Proof.
  intros.
  unfold t_update.
  case_eq (eqb_string x y).
    -  intros;auto.
       rewrite eqb_st_xy in H0.
        + symmetry in H0.
          apply tru_fal in H0.
          intuition.
        + auto.
    -  rewrite eqb_st_xy.
       + intro;auto.
       + auto.
Qed.

(*auxiliary lemma*)
Lemma update_eq : ∀ (A : Type) (m : partial_map A) x v,
  (update m x v) x = Some v.
Proof.
  intros.
  unfold update.
  now rewrite t_update_eq.
Qed.

(*auxiliary lemma*)
Lemma update_neq :forall (Gamma: context) (T2:ty) (x x0:string),  
           ~x=x0 -> (update Gamma x T2 x0)=(Gamma x0).
Proof.
  intros.
  unfold update.
  now rewrite t_update_neq.
Qed.

(*auxiliary lemma*)
Lemma same_string_true_iff : forall x x0: string, 
                    eqb_string x x0 = true <-> x=x0.
Proof.
  intros.
  unfold eqb_string.
  destruct (string_dec x x0) as [Hs_eq | Hs_not_eq].
  - rewrite Hs_eq. 
    split. 
    reflexivity.
    reflexivity.
  - split.
    + intros.
      symmetry in H.
      apply tru_fal in H.
      intuition.
    + intros.
      intuition.
Qed.

(*auxiliary lemma*)
Lemma same_string_false_iff : forall x x0: string, 
                    eqb_string x x0 = false <-> ~x=x0.
Proof.
  intros.
  unfold eqb_string.
  destruct (string_dec x x0) as [Hs_eq | Hs_not_eq].
  - rewrite Hs_eq. 
    split.
    + intuition.
    + intuition.
  - split.
    + now intros.
    + now intros.
Qed.
    

(*auxiliary lemma*)
Lemma eqb_string_true_var_same: forall x x0 :string,
                   eqb_string x x0 = true -> tm_var x = tm_var x0. 
Proof.
  intros.
  f_equal.
  now apply same_string_true_iff.
Qed.

(*auxiliary lemma*)
Lemma eqb_stringP : ∀ x y : string,
  reflect (x = y) (eqb_string x y).
Proof.
  intros.
  apply iff_reflect. 
  now rewrite same_string_true_iff.
Qed.

(*auxiliary lemma*)
Lemma update_override : ∀ (A : Type) (m : partial_map A) x v1 v2,
  (update (update m x v1) x v2) = (update m x v2).
Proof.
  intros.
  unfold update.
  unfold t_update.
  extensionality x'.
  now destruct (eqb_stringP x x').
Qed.

(*auxiliary lemma*)
Lemma t_update_same : ∀ (Gamma : context) x y,
  t_update Gamma x (Gamma x) y = Gamma y.
Proof.
  intros.
  unfold t_update.
  destruct (eqb_stringP x y).
  - now f_equal.
  - auto.
Qed.

(*auxiliary lemma*)
Lemma update_same : ∀ (Gamma : context) x v y,
  Gamma x = Some v →
  (update Gamma x v) y = Gamma y.
Proof.
  intros.
  unfold update.
  rewrite <- H.
  apply t_update_same.
Qed.

(*auxiliary lemma*)
Lemma trans_eq {A:Type}: forall a b c :A, a=b -> b=c -> c=a.
Proof.
  intros.
  rewrite <- H0.
  now symmetry.
Qed.

(*In the following, we have several lemms for a context premutation,
which will be useful in main lemmas later.*)

Lemma update_permutation_has_type_aux1 (Gamma: context): 
                  forall (t:tm) (T1 T2 T3:ty) (x1 x2 x3:string)
            , has_type (update (update Gamma x1 T1) x2 T2) t T3
              -> ((update Gamma x1 T1) x2)=None. 
Proof.
  intros.
  now apply well_formedness_of_context with (Gamma:=(update Gamma x1 T1))(t:=t)(T1:=T2)(T2:=T3).
Qed.

Lemma update_permutation_has_type_aux2 (Gamma: context): 
                  forall (t:tm) (T1 T2 T3:ty) (x1 x2 x3:string)
            , ((update Gamma x1 T1) x2)=None -> ~x1=x2. 
Proof.
  intros.
  rewrite <- same_string_false_iff.
  destruct (eqb_stringP x1 x2).
  - unfold update in H.
    unfold t_update in H.
    destruct (eqb_stringP x1 x2) in H.
    + easy.
    + intuition.
  - auto.
Qed.

Lemma update_permutation_has_type_aux3 (Gamma: context): 
                  forall (t:tm) (T1 T2 T3:ty) (x1 x2 x3:string)
            , has_type (update (update Gamma x1 T1) x2 T2) t T3
              ->~x1=x2. 
Proof.
  intros.
  apply update_permutation_has_type_aux2 with (Gamma:=Gamma)(x1:=x1)(x2:=x2)(T1:=T1).
  - auto.
  - auto.
  - auto.
  - auto.
  - apply update_permutation_has_type_aux1 with (t:=t)(T1:=T1)(T2:=T2)(T3:=T3).
    + auto.
    + auto.
Qed.

Lemma update_permutation_has_type_aux4_0 (Gamma: context): 
                  forall (t:tm) (T1 T2 T3 T4:ty) (x1 x2 x3:string)
            , has_type (update (update (update Gamma x1 T1) x2 T2) x3 T3) t T4
              -> has_type (update (update Gamma x1 T1)  x2 T2) (tm_var x2) T2. 
Proof.
  intros.
  apply well_formedness_of_context in H.
  apply T_Var.
  unfold update.
  unfold t_update.
  case_eq (eqb_string x2 x2).
  - intros;auto.
  - intros.
    rewrite same_string_false_iff in H0.
    intuition.
Qed.

Lemma update_permutation_has_type_aux4_1 (Gamma: context): 
                  forall (t:tm) (T1 T2 T3 T4:ty) (x1 x2 x3:string)
            , has_type (update (update Gamma x1 T1)  x2 T2) (tm_var x2) T2
              -> ~x1=x2. 
Proof.
  intros.
  apply well_formedness_of_context in H .
  apply update_permutation_has_type_aux2 with (Gamma:=Gamma)(T1:=T1);auto.
Qed.

Lemma update_permutation_has_type_aux4_2 (Gamma: context): 
                  forall (t:tm) (T1 T2 T3 T4:ty) (x1 x2 x3:string)
            , has_type (update (update (update Gamma x1 T1) x2 T2) x3 T3) t T4
              -> ~x1=x2. 
Proof.
  intros.
  apply update_permutation_has_type_aux4_1 with (Gamma:=Gamma)(T1:=T1)(T2:=T2).
  - auto.
  - auto.
  - auto.
  - auto.
  - now apply update_permutation_has_type_aux4_0 with (t:=t)(T3:=T3)(T4:=T4)(x3:=x3).
Qed.

Lemma auxiliary_update_permutation (Gamma: context): 
                  forall (T1 T2:ty) (x1 x2 x3:string)
            , ~x1=x2 ->  (update (update Gamma x1 T1) x2 T2) x3
              = (update (update Gamma x2 T2) x1 T1) x3. 
Proof.
  intros.
  unfold update.
  unfold t_update.
  case_eq (eqb_string x2 x3).
  - case_eq (eqb_string x1 x3).
    + intros.
      apply same_string_true_iff in H0.
      apply same_string_true_iff in H1.
      symmetry in H1.
      apply trans_eq with (a:=x1) (c:=x2) in H0.
      * symmetry in H0;intuition.
      * auto.
    + now intros.
  - case_eq (eqb_string x1 x3).
    + now intros.
    + now intros.
Qed.

Lemma auxiliary_update_permutation2 (Gamma: context): 
                  forall (T1 T2:ty) (x1 x2 :string)
            , ~x1=x2 ->  (update (update Gamma x1 T1) x2 T2)
              = (update (update Gamma x2 T2) x1 T1). 
Proof.
  intros.
  extensionality x3.
  now apply auxiliary_update_permutation.
Qed.

(*Among many version of permutation lemmas, the following is the 
most important one.*)

Lemma update_permutation_has_type (Gamma: context): 
                  forall (t:tm) (T1 T2 T3:ty) (x1 x2 x3:string)
            , has_type (update (update Gamma x1 T1) x2 T2) t T3
              -> has_type (update (update Gamma x2 T2) x1 T1) t T3. 
Proof.
  intros.
  inversion_clear H.
  - apply T_Var.
    rewrite auxiliary_update_permutation.
    + auto.
    + apply T_Var in H0.
      apply update_permutation_has_type_aux3 with
      (Gamma:=Gamma)(t:=tm_var x)(T1:=T1)(T2:=T2)(T3:=T3) in H0;auto.
  - apply T_Abs.
    rewrite <- auxiliary_update_permutation2 with (x2:=x2).
    + auto.
    + now apply update_permutation_has_type_aux4_2 with
      (Gamma:=Gamma)(t:=t1)(T1:=T1)(T2:=T2)(T3:=T4)(T4:=T0)(x3:=x).
  - apply T_App with (T2:=T4).
    + rewrite <- auxiliary_update_permutation2 with (x2:=x2). 
      * auto.
      * apply update_permutation_has_type_aux3 
        with (Gamma:=Gamma)(t:=t2)(T1:=T1)(T2:=T2)(T3:=T4);auto.
    + rewrite <- auxiliary_update_permutation2 with (x2:=x2).
      * auto.
      * apply update_permutation_has_type_aux3 
        with (Gamma:=Gamma)(t:=t2)(T1:=T1)(T2:=T2)(T3:=T4);auto.
Qed.


Lemma same_string_then_same_type  : 
                  forall  (Gamma: context)(T1 T2:ty) (x1 x2:string)
            , x1=x2 -> has_type (update Gamma x1 T1) (tm_var x2) T2 ->
              T1=T2 
              . 
Proof.
  intros.
  inversion_clear H0.
  unfold update in H1.
  unfold t_update in H1.
  destruct (eqb_stringP x1 x2) in H1.
  - now inversion H1. 
  - intuition.
Qed.

(* Now we will show one of the most basic lemmas called generation lemma.
It will be shown immediately, but will be necessary in later stages.*)

Lemma Generation_lemma_var (Gamma: context): forall (T :ty) (x:string)
                , has_type Gamma (tm_var x) T -> (Gamma x) = (Some T).
Proof.
  intros.
  now inversion_clear H.
Qed.

Lemma Generation_lemma_app (Gamma: context): forall (t1 t2: tm) (T1 T2 :ty)
                , has_type Gamma (tm_app t1 t2) T1 
                  -> exists T2, has_type Gamma t1 (Ty_Arrow T2 T1) 
                  /\ has_type Gamma t2 T2.
Proof.
  intros.
  inversion_clear H.
  exists T3.
  now intros.
Qed.

Lemma Generation_lemma_abs (Gamma: context): 
                              forall (t: tm) (T1 T2 :ty) (x:string)
                , has_type Gamma (tm_abs x T1 t) T2 
                  -> exists T3, has_type (update Gamma x T1) t T3 
                  /\ T2= (Ty_Arrow T1 T3).
Proof.
  intros.
  inversion_clear H.
  exists T0.
  now intros.
Qed.

(* Our next non-trivial lemma. Uniqueness of typing. *)

Lemma unique_type (Gamma: context): forall (t:tm) (T1 T2:ty)
            ,  has_type Gamma t T1 -> has_type Gamma t T2 -> T1=T2.
Proof.
  intros.
  revert H.
  revert T1.
  revert H0.
  revert T2.
  revert Gamma.
  induction t.
  - intros.
    inversion H0.
    inversion H.
    symmetry in H7. 
    apply trans_eq with (c:= Some T2)  in H7.
    symmetry in H7.
    + now inversion H7.
    + auto.
  - intros Gamma X2 K2 X1 K1.
    inversion_clear K2.
    inversion_clear K1.
    pose proof (IHt1 Gamma) as IHt1'.
    pose proof (IHt1' (T0 --> X1)) as B1.
    pose proof (B1 H1) as C1.
    pose proof (C1 (T2 --> X2)) as C2.
    pose proof (C2 H) as D1.
    pose proof (IHt2 Gamma) as IHt2'.
    pose proof (IHt2' T0) as B2.
    pose proof (B2 H2) as C3.
    pose proof (C3 T2) as C4.
    pose proof (C4 H0) as D2.
        apply ty_sameness2 with (A:=T0) (C:=T2).
      + auto.
      + auto.
  - intros Gamma X2 K2 X1 K1.
    inversion_clear K2.
    inversion_clear K1.
    apply ty_sameness3 with (A:=t).
    apply IHt with (Gamma:= (update Gamma s t)).
    + auto.
    + auto.
Qed.  

(* The followin two lemmas are auxiliary lemmas for the weakening lemma. *)

Lemma aux_for_weak1 :forall T:ty, ~ (None = (Some T) ).
Proof.
  intros.
  intuition.
  inversion H.
Qed.


Lemma aux_for_weak2 (Gamma: context): forall (t:tm) (T1 T2 t:ty) (x s:string)
            ,
              Gamma x = None -> ~x=s ->
 update Gamma s t x = None 
             . 
Proof.
  intros.
  induction H.
  apply update_neq.
  auto.
Qed.

(*One of our main goals: weakening lemma.*)

Lemma weakening (Gamma: context): forall (t:tm) (T T2:ty) (x:string)
            , (Gamma x)=None -> has_type Gamma t T 
              -> has_type (update Gamma x T2) t T. 
Proof.
  intros.
  revert T2.
  revert H.
  revert x.
  revert H0.
  revert Gamma.
  revert T.
  induction t.
  - intros.
    apply T_Var.
    unfold update.
    unfold t_update.
    case_eq (eqb_string x s).
    + apply Generation_lemma_var in H0.
      intros.
      apply   same_string_true_iff in H1. 
      rewrite H1 in H.
      symmetry in H0.
      apply trans_eq with (a:=(Some T)) (b:= (Gamma s)) in H.
      * assert (JJJ:= aux_for_weak1).
        pose proof (JJJ T) as B1.
        intuition.
      * auto.
    + intros.
      now apply Generation_lemma_var.
  - intros.
    inversion_clear H0.
    apply T_App with (T2:=T0).
    +  apply IHt1.
      * auto.
      * auto.
    + apply IHt2.
      * auto.
      * auto.
  - intros. 
    inversion_clear H0.
    apply T_Abs.
    case_eq (eqb_string x s).
    + intros.
      rewrite same_string_true_iff in H0.
      rewrite H0.
      now rewrite update_override.
    + intros.
      rewrite auxiliary_update_permutation2.
      * apply IHt.
        -- auto.
        -- rewrite same_string_false_iff in H0.
           now apply aux_for_weak2.
      * now  rewrite same_string_false_iff in H0.
Qed.

(* The following substitution lemma is a support lemma for the subject reduction lemma.
But, this lemma is the essential part of the subject reduction lemma.*)

Lemma Substitution_lemma (Gamma: context): 
                forall (M N:tm) (sigma tau:ty) (x:string)
            ,    has_type (update Gamma x sigma) M tau 
              /\ has_type Gamma N sigma
              -> has_type Gamma (subst x N M) tau.
Proof.
  intros.
  destruct H.
  revert H0.
  revert N.
  revert H.
  revert Gamma.
  revert tau.
  revert sigma.
  induction M.
  - intros.
    simpl. 
    case_eq (eqb_string x s).
    + intros.
      apply same_string_true_iff in H1.
      rewrite H1 in H.
      inversion H.
      rewrite update_eq in H4.
      inversion H4.
      now rewrite H7 in H0.
    + intros.
      inversion H.
      rewrite update_neq in H4.
      apply T_Var in H4.
      * auto.
      * now apply same_string_false_iff in H1.
  - intros.
    simpl.
    inversion_clear H.
    apply T_App with (T2:=T2).
    + apply IHM1 with (sigma:=sigma) (tau:=T2 --> tau);auto.
    + apply IHM2 with (sigma:=sigma) (tau:=T2);auto.
  - intros. 
    simpl.
    case_eq (eqb_string x s).
    + intros.
      inversion_clear H.
      apply same_string_true_iff in H1.
      rewrite H1 in H2.
      rewrite update_override in H2.
      now apply T_Abs in H2.
    + intros.
      apply same_string_false_iff in H1. 
      inversion_clear H.
      apply update_permutation_has_type 
            with (Gamma:= Gamma) (t:=M) (T1:=sigma)(T2:=t)(T3:=T1) 
            in H2.
      pose proof (IHM sigma) as IHM'.
      pose proof (IHM' T1) as IHM1.
      pose proof (IHM1 (update Gamma s t)) as IHM2.
      pose proof (IHM2 H2) as IHM3.
      pose proof (IHM3 N) as IHM4.
      assert (JJJ:=H1).
      apply T_Abs in H2.
      apply well_formedness_of_context in H2.
      apply weakening with (x:=s) (t:=N)(T:=sigma)(T2:=t) in H0.
      apply IHM4 in H0.
      * now apply T_Abs.
      * auto.
      * auto.
Qed.

(*Our main goal: subject reduction lemma.*)

Lemma Subject_reduction (Gamma: context): forall (t t':tm) (T:ty) 
            , has_type Gamma t T -> reduction t t' -> has_type Gamma t' T.
Proof.
  intros.
  revert H.
  revert T.
  revert Gamma.
  induction H0.
  - intros.
    apply Generation_lemma_app in H.
    destruct H.
    destruct H.
    apply Generation_lemma_abs in H.
    destruct H.
    destruct H.
    apply ty_sameness4 in H1.
    destruct H1.
    + apply Substitution_lemma with (sigma:=T2).
      split.
      * now rewrite <- H2 in H.
      * now rewrite H1 in H0. 
    + auto.
  - intros.
    inversion_clear H.
    apply T_App with (T2:=T2).
    + apply IHreduction;auto.
    + auto.
  - intros.
    inversion_clear H.
    apply T_App with (T2:=T2).
    + auto.
    + apply IHreduction;auto.
  - intros.
    inversion_clear H.
    apply T_Abs.
    apply IHreduction;auto.
Qed.