From Coq Require Import Relations Arith Lia Bool List.

Set Structural Injection.
Add Search Blacklist "_ind" "_sind" "_rec" "_rect".
Set Default Goal Selector "!".
Import ListNotations.

(** ** Types *)

Inductive ty : Type :=
  | TBool  : ty
  | TArr (A B : ty) : ty.

(** ** Terms *)

Inductive tm : Type :=
  | tVar (n : nat) : tm
  | tApp (t u : tm) : tm
  | tAbs (A : ty) (t : tm) : tm
  | tTrue  : tm
  | tFalse : tm
  | tIf (b t t' : tm) : tm.

(** [tVar (n : nat)]? What is this? *)


Definition idB : tm := (tAbs TBool (tVar 0)). (** λ x : 𝔹. x *)

Definition appB : tm :=
  tAbs (TArr TBool TBool)
    (tAbs TBool
      (tApp (tVar 1) (tVar 0))).
  
    (** λ x : 𝔹 → 𝔹. λ y : 𝔹. x y *)

(** *** De Bruijn calculus *)

Reserved Notation "t [ s ]" (at level 1, s constr, format "t [ s ]").


(** *** Renamings *)

Reserved Notation "t ⟨ r ⟩" (at level 1, format "t ⟨ r ⟩").

Definition ren := nat -> nat.

Declare Scope ren_scope.
Delimit Scope ren_scope with ren.
Bind Scope ren_scope with ren.

Definition cons_ren (r : ren) (n : nat) : ren :=
  fun i => match i with
  | 0 => n
  | S i' => r i'
  end.

Arguments cons_ren _ _ _ /.

Definition shift_ren : ren := S.

Arguments shift_ren _ /.

Definition ren_comp (r r' : ren) := fun i => r' (r i).

Arguments ren_comp _ _ _ /.

Notation "↑" := shift_ren : ren_scope.
Infix ",," := cons_ren (at level 50, left associativity) : ren_scope.
Infix ";" := ren_comp (at level 40) : ren_scope.

Definition up_ren (r : ren) : ren := r ; ↑ ,, 0.

Notation "⇑ r" := (up_ren r) (at level 1) : ren_scope.

Arguments up_ren _ _ /.

Fixpoint rename (r : ren) (t : tm) {struct t} : tm :=
  match t with
  | tVar y => tVar (r y)
  | tAbs T t => tAbs T t⟨⇑ r⟩
  | tApp t1 t2 => tApp t1⟨r⟩ t2⟨r⟩
  | tTrue => tTrue
  | tFalse => tFalse
  | tIf t1 t2 t3 => tIf t1⟨r⟩ t2⟨r⟩ t3⟨r⟩
  end

where "t ⟨ r ⟩" := (rename r t) (r in scope ren_scope).

Definition id_ren : ren := (fun i => i).

Arguments id_ren _ /.
Notation "⋅" := id_ren : ren_scope.

(** *** Substitution *)

Definition subst := nat -> tm.

Declare Scope subst_scope.
Delimit Scope subst_scope with sub.
Bind Scope subst_scope with subst.

Definition cons_subst (s : subst) (t : tm) : subst :=
  fun i => match i with
  | 0 => t
  | S i' => s i'
  end.

Arguments cons_subst _ _ _ /.

Definition rename_subst (r : ren) (s : subst) : subst :=
  fun i => (s i)⟨r⟩.

Arguments rename_subst _ _ _ /.

Definition id_subst : subst := tVar.

Arguments id_subst _ /.

Notation "⋅" := id_subst : subst_scope.
Infix ",," := cons_subst (at level 50, left associativity) : subst_scope.
Notation "s '⟨' r '⟩' " := (rename_subst r s) : subst_scope.

Definition up_subst (s : subst) : subst :=  s⟨↑⟩ ,, (tVar 0).

Notation "⇑ s" := (up_subst s) (at level 1) : subst_scope.

Arguments up_subst _ _ /.

Definition one_subst (t : tm) : subst := ⋅ ,, t.

Arguments one_subst _ _ /.

Coercion one_subst : tm >-> subst.

Definition ren_to_subst (r : ren) : subst := fun i => tVar (r i).

Arguments ren_to_subst _ _/.

Coercion ren_to_subst : ren >-> subst.

Fixpoint substitute (s : subst) (t : tm) : tm :=
  match t with
  | tVar y => s y
  | tAbs T t => tAbs T t[⇑ s]
  | tApp t1 t2 => tApp t1[s] t2[s]
  | tTrue => tTrue
  | tFalse => tFalse
  | tIf t1 t2 t3 => tIf t1[s] t2[s] t3[s]
  end

where "t [ s ]" := (substitute s t) (s in scope subst_scope).

Definition subst_comp (s s' : subst) : subst :=
    fun i => (s i)[s'].

Arguments subst_comp _ _ _ /.

Infix ";" := subst_comp (at level 40) : subst_scope.

(** *** Equations *)

Lemma subst_ext (s s' : subst) (t : tm) :
  (forall i, s i = s' i) ->
  t[s] = t[s'].
Proof.
  intros e.
  induction t in s, s', e |- * ; cbn ; auto.
  - erewrite IHt1, IHt2 ; eauto.
  - erewrite IHt ; eauto.
    destruct i ; cbn ; eauto.
    now rewrite e.
  - erewrite IHt1, IHt2, IHt3 ; eauto.
Qed.

(* Note: not needed with funext *)

Lemma subst_compose (s s' : subst) (t : tm) :
  t[s][s'] = t[s ; s'].
Proof.
  induction t in s, s' |- * ; cbn ; auto.
  - now rewrite IHt1, IHt2.
  - rewrite IHt.
    erewrite subst_ext.
    1: reflexivity.
    simpl.
    intros [] ; simpl.
    + reflexivity.
    + (* ?? *)
Abort.

(* Let's do some more proofs *)

Lemma ren_subst_eq (r : ren) (t : tm) :
  t[r] = t⟨r⟩.
Proof.
  induction t in r |- * ; cbn ; auto.
  - now rewrite IHt1, IHt2.
  - rewrite <- IHt.
    f_equal.
    apply subst_ext.
    now intros [].
  - now rewrite IHt1, IHt2, IHt3.
Qed.

Corollary ren_ext (r r' : ren) (t : tm) :
  (forall i, r i = r' i) ->
  t⟨r⟩ = t⟨r'⟩.
Proof.
  intros.
  rewrite <- !ren_subst_eq.
  apply subst_ext.
  intros ; cbn ; auto.
Qed.

Lemma id_ren_eq t : t⟨⋅⟩ = t.
Proof.
  induction t ; cbn ; auto.
  - now rewrite IHt1, IHt2.
  - erewrite ren_ext, IHt ; eauto.
    intros [] ; reflexivity.
  - now rewrite IHt1, IHt2, IHt3.
Qed.

Corollary id_subst_eq t : t[⋅] = t.
Proof.
  erewrite subst_ext.
  - rewrite ren_subst_eq, id_ren_eq ; reflexivity.
  - reflexivity.
Qed.

Lemma ren_compose (r r' : ren) (t : tm) :
  t⟨r⟩⟨r'⟩ = t⟨r ; r' ⟩.
Proof.
  induction t in r, r' |- * ; cbn ; auto.
  
  - now rewrite IHt1, IHt2.
  - rewrite IHt.
    f_equal.
    apply ren_ext.
    intros [] ; cbn.
    all: easy.
  - now rewrite IHt1, IHt2, IHt3.
Qed.

Lemma ren_subst_compose (r : ren) (s : subst) (t : tm) :
  t⟨r⟩[s] = t[r ; s].
Proof.
  induction t in r, s |- * ; cbn ; auto.

  - now rewrite IHt1, IHt2.
  - rewrite IHt.
    f_equal.
    apply subst_ext.
    intros [] ; cbn ; auto.
  - now rewrite IHt1, IHt2, IHt3.
Qed.

Lemma subst_ren_compose (s : subst) (r : ren) (t : tm) :
  t[s]⟨r⟩ = t[s ; r].
Proof.
  induction t in r, s |- * ; cbn ; auto.

  - now rewrite ren_subst_eq.
  - now rewrite IHt1, IHt2.
  - rewrite IHt.
    f_equal.
    apply subst_ext.
    intros [] ; cbn ; eauto.
    rewrite !ren_subst_eq, !ren_compose.
    apply ren_ext.
    intros [] ; cbn ; eauto.
  - now rewrite IHt1, IHt2, IHt3.
Qed.

Lemma subst_compose (s s' : subst) (t : tm) :
  t[s][s'] = t[s ; s'].
Proof.
  induction t in s, s' |- * ; cbn ; auto.

  - now rewrite IHt1, IHt2.
  - rewrite IHt.
    f_equal.
    apply subst_ext.
    intros [] ; cbn ; eauto.
    rewrite ren_subst_compose, subst_ren_compose ; cbn.
    eapply subst_ext.
    cbn.
    eauto using ren_subst_eq.
  - now rewrite IHt1, IHt2, IHt3.
Qed.

Corollary subst_lift_cons (s : subst) (h : tm) (t : tm) :
  t[⇑ s ; h] = t[s,,h].
Proof.
  apply subst_ext.
  intros [] ; cbn ; eauto.
  rewrite ren_subst_compose.
  erewrite subst_ext.
  - rewrite id_subst_eq ; eauto.
  - intros [] ; reflexivity.
Qed.


(** ** Typing *)

Definition context := list ty.

Definition con_cons (Γ : context) (T : ty) := cons T Γ.

Notation "Γ ,,, T" := (con_cons Γ T) (at level 50).

Fixpoint nth_error {A} (l : list A) (n : nat) : option A :=
  match l, n with
  | nil, _ => None
  | a :: _, 0 => Some a
  | _ :: l', S n' => nth_error l' n'
  end.

Definition in_context (n : nat) (Γ : context) (T : ty) : Prop :=
  nth_error Γ n = Some T.

Lemma in_zero Γ T : in_context 0 (Γ,,,T) T.
Proof. unfold in_context. simpl. reflexivity. Qed.

Lemma var_empty n T : ~ in_context n nil T.
Proof.
  unfold in_context ; cbn.
  discriminate.
Qed.

Hint Resolve in_zero : core.

Reserved Notation "Γ '|-' t '::' T"
  (at level 101, t at level 59).

Inductive has_type : context -> tm -> ty -> Prop :=
| T_Var : forall Γ n T,
  in_context n Γ T ->
  Γ |- tVar n :: T

| T_Abs : forall Γ T1 (T2 : ty) t,
  (Γ ,,, T1 |- t :: T2) ->
  Γ |- tAbs T1 t :: TArr T1 T2

| T_App : forall Γ T1 T2 t1 t2,
  (Γ |- t1 :: TArr T1 T2) ->
  (Γ |- t2 :: T1) ->
  Γ |- tApp t1 t2 :: T2

| T_True : forall Γ,
  Γ |- tTrue :: TBool

| T_False : forall Γ,
  Γ |- tFalse :: TBool

| T_If : forall Γ t1 t2 t3 T,
  (Γ |- t1 :: TBool) ->
  (Γ |- t2 :: T) ->
  (Γ |- t3 :: T) ->
  Γ |- tIf t1 t2 t3 :: T

where "Γ '|-' t '::' T" := (has_type Γ t T).

Hint Constructors has_type : core.

Example typing_example_1 :
  nil |- idB :: TArr TBool TBool.
Proof.
  unfold idB.
  (* constructor.
  constructor.
  apply in_zero. *)
  auto.
Qed.

(** ** Renamings and substitutions preserve types *)

Definition ren_has_type (Δ Γ : context) (r : ren) : Prop :=
  forall i T, in_context i Γ T -> in_context (r i) Δ T.

Lemma shift_has_type (Γ : context) (T : ty) : ren_has_type (Γ,,,T) Γ ↑.
Proof.
  intros i T' H.
  cbn.
  unfold in_context.
  cbn.
  exact H.
Qed.

Lemma ren_lift_has_type (Δ Γ : context) (T : ty) (r : ren) :
  ren_has_type Δ Γ r ->
  ren_has_type (Δ,,,T) (Γ,,,T) (⇑ r).
Proof.
  intros Hr i T' Hin.
  unfold ren_has_type, in_context in *.
  cbn.
  destruct i ; cbn ; auto.
Qed.

Lemma ren_typing Δ Γ r t T :
  ren_has_type Δ Γ r ->
  (Γ |- t :: T) ->
  Δ |- t⟨r⟩ :: T.
Proof.
  intros Hr Ht.
  induction Ht in Δ, r, Hr ; cbn.
  (* - unfold ren_has_type in Hr.
    constructor.
    auto.
  - constructor.
    apply IHHt, ren_lift_has_type.
    assumption. *)
  all: eauto using ren_lift_has_type.
Qed.

Definition subst_has_type (Δ Γ : context) (s : subst) : Prop :=
  forall i T, in_context i Γ T -> Δ |- s i :: T.

Lemma subst_cons_has_type (Δ Γ : context) (T : ty) (s : subst) (t : tm) :
  subst_has_type Δ Γ s ->
  (Δ |- t :: T) ->
  subst_has_type Δ (Γ,,,T) (s ,, t).
Proof.
  intros Hs Hty [|i'] T' Hin ; cbn.
  - unfold in_context in Hin ; cbn in *.
    inversion Hin ; subst.
    assumption.
  - apply Hs, Hin.
Qed.

Lemma id_subst_has_type (Γ : context) :
  subst_has_type Γ Γ ⋅.
Proof.
  intros i T Hin ; cbn.
  induction Γ.
  - auto using var_empty.
  - constructor.
    assumption.
Qed.

Set Printing Coercions.

Lemma subst_one_has_type (Γ : context) (T : ty) (t : tm) :
  (Γ |- t :: T) -> 
  subst_has_type Γ (Γ,,,T) t.
Proof.
  unfold one_subst.
  apply subst_cons_has_type, id_subst_has_type.
Qed.

Unset Printing Coercions.


Lemma subst_lift_has_type (Δ Γ : context) (T : ty) (s : subst) :
  subst_has_type Δ Γ s ->
  subst_has_type (Δ,,,T) (Γ,,,T) (⇑ s).
Proof.
  intros Hs.
  apply subst_cons_has_type ; eauto.
  intros i T' Hin ; cbn.
  eapply ren_typing ; eauto using shift_has_type.
Qed.

Lemma subst_typing Δ Γ s t T :
  subst_has_type Δ Γ s ->
  (Γ |- t :: T) ->
  Δ |- t[s] :: T.
Proof.
  intros Hr Ht.
  induction Ht in Δ, s, Hr ; cbn ; eauto using subst_lift_has_type.
Qed.


(** ** Evaluation *)

Reserved Notation "t '-->' t'" (at level 40).

Inductive step : tm -> tm -> Prop :=
  | ST_Beta : forall T t1 v2,
        tApp (tAbs T t1) v2 --> t1[v2]
  | ST_Fun : forall t1 t1' t2,
        t1 --> t1' ->
        tApp t1 t2 --> tApp t1' t2
  | ST_IfTrue : forall t1 t2,
      tIf tTrue t1 t2 --> t1
  | ST_IfFalse : forall t1 t2,
      tIf tFalse t1 t2 --> t2
  | ST_If : forall t1 t1' t2 t3,
      t1 --> t1' ->
      tIf t1 t2 t3 --> tIf t1' t2 t3

where "t '-->' t'" := (step t t').

Hint Constructors step : core.

Notation multistep := (clos_refl_trans tm step).
Notation "t1 '-->*' t2" := (multistep t1 t2) (at level 40).

Print clos_refl_trans.

Lemma step_example1 :
  tApp idB tTrue -->* tTrue.
Proof.
  constructor.
  unfold idB.
  constructor.
Qed.

Lemma ST_If_multi b b' t t' :
  b -->* b' ->
  tIf b t t' -->* tIf b' t t'.
Proof.
  intros Hred.
  induction Hred using clos_refl_trans_ind_left ; eauto using rt_refl, rt_step, rt_trans.
Qed.

Inductive value : tm -> Prop :=
| v_abs : forall T t,
    value (tAbs T t)
| v_true :
    value tTrue
| v_false :
    value tFalse.

Hint Constructors value : core.

(** ** Progress *)

Lemma canonical_forms_bool (v : tm) :
  (nil |- v :: TBool) ->
  value v ->
  (v = tTrue) \/ (v = tFalse).
Proof.
  intros HT HVal.
  destruct HVal; auto.
  inversion HT.
Qed.

Lemma canonical_forms_fun v T1 T2 :
  (nil |- v :: TArr T1 T2) ->
  value v ->
  exists u, v = tAbs T1 u.
Proof.
  intros HT HVal.
  destruct HVal as [? t1| |] ; inversion HT ; subst.
  exists t1. reflexivity.
Qed.

Theorem progress t T :
  (nil |- t :: T) ->
  value t \/ exists t', t --> t'.
Proof.
  intros Ht.
  remember nil as Γ eqn:eΓ.
  induction Ht in eΓ ; subst Γ.

  - unfold in_context in H ; cbn in H.
    discriminate.

  - left.
    constructor.

  - right.
    destruct IHHt1 as [ ? | [] ] ; eauto.
      
    apply canonical_forms_fun in Ht1 as [] ; auto.
    subst.
    eauto.
    
  - left.
    eauto.
    
  - left.
    eauto.
    
  - right.
    destruct IHHt1 as [| [] ] ; eauto.
    apply canonical_forms_bool in Ht1 as [|] ; auto ; subst.
    all: eauto.

Qed.

(** ** Preservation *)

Lemma preservation_one Γ T t t' :
  (Γ |- t :: T) ->
  (t --> t') ->
  (Γ |- t' :: T).
Proof.
  intros Hty Hred.
  induction Hred in Γ, T, Hty |- *.
  all: try solve [inversion Hty ; eauto].
  
  inversion Hty as [ | | ? T1 T2 ? ? Hfun Harg | | | ] ; subst ; clear Hty.
  inversion Hfun ; subst ; clear Hfun.
  eapply subst_typing ; eauto using subst_one_has_type.

Qed.

Lemma preservation Γ T t t' :
  (Γ |- t :: T) ->
  (t -->* t') ->
  Γ |- t' :: T.
Proof.
  intros Hty Hred.
  induction Hred using clos_refl_trans_ind_left ; eauto using preservation_one.
Qed.