(** * Exercises at the end!! *)
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.

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.

(** ** 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.

(** ** 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).

Lemma step_example1 :
  tApp idB tTrue -->* tTrue.
Proof.
  constructor.
  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.

(** ** Typing *)

Definition context := list ty.

Declare Scope context_scope.
Delimit Scope context_scope with con.
Bind Scope context_scope with context.

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

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

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

Lemma in_zero Γ T : in_context 0 (Γ,,,T) T.
Proof. reflexivity. 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) (Γ in scope context_scope).

Hint Constructors has_type : core.

Example typing_example_1 :
  nil |- idB :: TArr TBool TBool.
Proof.
  unfold idB.
  eauto.
Qed.

Lemma var_empty n T : ~ in_context n nil T.
Proof.
  unfold in_context ; cbn.
  discriminate.
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 ; eauto.
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 ; 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 [] T' Hin ; cbn.
  - unfold in_context in Hin ; cbn in *.
    injection 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.
Qed.

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

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.

(** ** 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.
    destruct IHHt2 as [| [] ] ; eauto.

  - left.
    eauto.
    
  - left.
    eauto.
    
  - right.
    destruct IHHt1 as [| [] ] ; eauto.
    apply canonical_forms_bool in Ht1 as [|] ; auto.
    + subst.
      destruct IHHt2 as [| [] ] ; eauto.
    + subst.
      destruct IHHt2 as [| [] ] ; 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.





(** ** Exercise: determinism of reduction *)

(** Show that one-step reduction is deterministic: *)

Lemma one_determinism (t t' t'' : tm) :
  t --> t' ->
  t --> t'' ->
  t' = t''.
Proof.
Admitted.

(** Show that values do not reduce further *)

Lemma value_no_red (t t' : tm) :
  value t ->
  t --> t' ->
  False.
Proof.
Admitted.

(** Better induction principles, which induct on the first step,
useful to exploit the fact that this step is deterministic: *)

Lemma clos_refl_trans_ind_right A R : forall (P : A -> A -> Prop),
  (forall z, P z z) ->
  (forall x y z, R x y -> P y z -> clos_refl_trans A R y z -> P x z) ->
  forall x z, clos_refl_trans A R x z -> P x z.
Proof.
  intros P Hrefl Hstep x z H.
  pattern x.
  eapply clos_refl_trans_ind_right ; eauto.
Qed.

(** A form of case-splitting, which might also come in handy: *)
Lemma clos_refl_trans_case_right {A} (R : relation A) (x y : A) :
  clos_refl_trans _ R x y ->
  x = y \/ exists z, R x z /\ clos_refl_trans _ R z y.
Proof.
  intros H.
  pattern x, y.
  eapply clos_refl_trans_ind_right ; eauto.
Qed.

(** Show that multi-step reduction to a value must be reflexivity: *)
(** Hint: the induction principles above might be useful. *)
Lemma one_red_value (t t' : tm) :
  t -->* t' ->
  value t ->
  t = t'.
Proof.
Admitted.

(** Show the following form of "confluence": *)
Lemma red_value_red_determinism (t t' t'' : tm) :
  t -->* t' ->
  t -->* t'' ->
  value t'' ->
  t' -->* t''.
Proof.
Admitted.

(** And conclude that reduction to a value is a deterministic relation: *)
Lemma red_value_determinism (t v v' : tm) :
  t -->* v ->
  t -->* v' ->
  value v ->
  value v' ->
  v = v'.
Proof.
Admitted.

(** Harder: if we do not know that the reducts are value, what can we say?
  Try to find a statement that does not use the value predicate at all. *)
Lemma red_determinism (t t' t'' : tm) :
  t -->* t' ->
  t -->* t'' ->
  True. (** Fill me!*)
Proof.
Admitted.

(** ** Exercise: proving canonicity *)

(** We are going to prove the following theorem: *)

Definition canonicity_statement := forall t,
  (nil |- t :: TBool) ->
  t -->* tTrue \/ t -->* tFalse.

(** In words: every well-typed, closed program of type [TBool] evaluates
  to a value, either [tTrue] or [tFalse]. *)

(** The proof is by logical relation: we need to adequately extend the
  theorem to function types, and to open terms. *)

(** *** Definitions *)

(** First, a few definitions *)

Definition halts (t : tm) : Prop :=
    exists t', t -->* t' /\ value t'.

(** A term halts if it evaluates to a value. *)

(** The logical relation on closed terms *)

Fixpoint LR_closed (T : ty) (t : tm) : Prop :=
  (match T with
  | TBool => halts t
  | TArr T1 T2 =>
      forall a,
      (nil |- a :: T1) ->
      LR_closed T1 a ->
      LR_closed T2 (tApp t a)
  end).

(** A closed program is in the logical relation at type [T] if either: 
  - [T] is [TBool] and the program halts
  - [T] is an arrow type, and for any well-typed argument, applying the
    program to that argument is again in the logical relation. *)

(** This is extended pointwise to substitutions. *)

Definition LR_subst (Γ : context) (s : subst) : Prop :=
  forall i T, in_context i Γ T -> LR_closed T (s i).

(** The logical relation on open terms:
  we use parallel substitutions to close over all free variables. *)

Definition LR (Γ : context) (T : ty) (t : tm) : Prop :=
  (Γ |- t :: T) /\
  forall s,
    subst_has_type nil Γ s ->
    LR_subst Γ s -> 
    LR_closed T t[s].

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

(** *** General lemmas *)

Lemma escape Γ T t :
  (Γ ||- t :: T) ->
  Γ |- t :: T.
Proof.
Admitted.

Hint Resolve escape : core.

Lemma exp_LR_closed_one T t t' :
  LR_closed T t' ->
  t --> t' ->
  LR_closed T t.
Proof.
Admitted.

Lemma exp_LR_closed T t t' :
  LR_closed T t' ->
  t -->* t' ->
  LR_closed T t.
Proof.
Admitted.

(** *** Semantic typing *)

(** The core of an argument by logical relation: we show that the logical
  relation is a "model" of the language, by showing that all typing rules
  are valid for the relation. *)

Lemma var_LR Γ n T :
  in_context n Γ T ->
  Γ ||- tVar n :: T.
Proof.
Admitted.

Lemma abs_LR Γ T1 T2 t :
  (Γ ,,, T1 ||- t :: T2) ->
  Γ ||- tAbs T1 t :: TArr T1 T2.
Proof.
Admitted.

Lemma app_LR Γ T1 T2 t1 t2 :
  (Γ ||- t1 :: TArr T1 T2) ->
  (Γ ||- t2 :: T1) ->
  Γ ||- tApp t1 t2 :: T2.
Proof.
Admitted.

Lemma true_LR Γ :
  Γ ||- tTrue :: TBool.
Proof.
Admitted.

Lemma false_LR Γ :
  Γ ||- tFalse :: TBool.
Proof.
Admitted.

Lemma if_LR Γ T b t t' :
  (Γ ||- b :: TBool) ->
  (Γ ||- t :: T) ->
  (Γ ||- t' :: T) ->
  Γ ||- tIf b t t' :: T.
Proof.
Admitted.


Theorem fundamental Γ T t :
  (Γ |- t :: T) ->
  Γ ||- t :: T.
Proof.
  (** Putting all the lemmas above together in one induction. *)
Admitted.

Corollary canonicity t :
  (nil |- t :: TBool) ->
  t -->* tTrue \/ t -->* tFalse.
Proof.
Admitted.



(** ** Exercise: a certified type-checker *)

(** During type-checking, we need to compare types, so we need first
  an equality test between types. Define it! *)

Fixpoint eqb_ty (T T' : ty) : bool.
Admitted.

(** Show that the test is correct: it reflects propositional equality. *)

Lemma eqb_refl T : eqb_ty T T = true.
Proof.
Admitted.

Lemma eqb_sound T T' : eqb_ty T T' = true -> T = T'.
Proof.
Admitted.

Lemma eqb_ty_correct T T' : reflect (T = T') (eqb_ty T T').
Proof.
Admitted.

(** Write the following [infer] function, with the specification that
  [infer Γ t] is [Some T] if [t] has type [T] in [Γ], and [None] if
  [t] is not typable. (This is a poor man's error monad, with [None]
  representing an error; there are ways to make this nicer, but this
  is out of scope here.) *)

Fixpoint infer (Γ : context) (t : tm) : option ty.
Admitted.

(** First, we can show that [infer] indeed infers the right type
  for well-typed terms. *)

Lemma typing_infer Γ t (T : ty) :
  (Γ |- t :: T) ->
  infer Γ t = Some T.
Proof.
Admitted.

(** Interestingly, this implies uniqueness of types. Why? You should not
  need any induction here. *)

Lemma typing_unique Γ t T T' :
  (Γ |- t :: T) ->
  (Γ |- t :: T') ->
  T = T'.
Proof.
Admitted.

(** Harder: show that the function is sound, ie when it answers positively
  then it has indeed deduced that the term is well-typed. *)

Lemma infer_sound Γ t T :
  infer Γ t = Some T ->
  Γ |- t :: T.
Proof.
Admitted.

(** Conclude that you have a decision procedure on typing.
  What should be the boolean that reflects typing? *)

Lemma typing_decide Γ t T :
  reflect (Γ |- t :: T) true.
Proof.
Admitted.