Intrinsically well-scoped de Bruijn representation with fancy notation

Syntax.v

From Coq Require Import String.
From stdpp Require Import base strings.

Section AUX.

  #[global] Instance option_eq_dec_normalizable A `{dec : EqDecision A} : EqDecision (option A).
  Proof.
    intros x y. destruct x as [x|], y as [y|].
    - destruct (decide (x = y)).
      + left. congruence.
      + right. congruence.
    - right. congruence.
    - right. congruence.
    - left. congruence.
  Defined.

  Definition Decision_yes_type {P} (d : Decision P) : Prop :=
    match d with
    | left _ => P
    | right _ => True
    end.

  Definition Decision_yes {P} (d : Decision P) : Decision_yes_type d :=
    match d with
    | left H => H
    | right _ => I
    end.

End AUX.

Module Syntax.

  Inductive Ctx : Set :=
  | CNil : Ctx
  | CExt : Ctx -> option string -> Ctx
  .

  Notation "⋄" := (CNil).
  Notation "Γ , *" := (CExt Γ None) (at level 40, left associativity).
  Notation "Γ , x" := (CExt Γ (Some x)) (at level 40, left associativity).

  Inductive Idx : Ctx -> Set :=
  | IZ Γ x : Idx (CExt Γ x)
  | IS Γ x : Idx Γ -> Idx (CExt Γ x)
  .

  Arguments IZ {_ _}.
  Arguments IS {_ _}.

  Definition code (Γ : Ctx) : Set :=
    match Γ with
    | CNil => Empty_set
    | CExt Γ _ => option (Idx Γ)
    end.

  Definition encode {Γ} (i : Idx Γ) : code Γ :=
    match i with
    | IZ => None
    | IS i => Some i
    end.

  Definition decode {Γ} : code Γ -> Idx Γ :=
    match Γ with
    | CNil => fun c => match c with end
    | CExt _ _ => fun c => match c with
                       | None => IZ
                       | Some i => IS i
                       end
    end.

  Inductive Tm (Γ : Ctx) : Set :=
  | TVar : Idx Γ -> Tm Γ
  | TLam : Tm (Γ, *) -> Tm Γ
  | TApp : Tm Γ -> Tm Γ -> Tm Γ
  .

  Arguments TVar {Γ} i.
  Arguments TLam {Γ} M.
  Arguments TApp {Γ} M N.
  
  Inductive Wk : Ctx -> Ctx -> Set :=
  | wk_id    Γ         : Wk Γ Γ
  | wk_shift Γ' Γ x' x : Wk Γ' Γ -> Wk (CExt Γ' x') (CExt Γ x)
  | wk_wk    Γ' Γ x    : Wk Γ' Γ -> Wk (CExt Γ' x ) Γ
  .

  Arguments wk_id    {Γ}.
  Arguments wk_shift {Γ' Γ x' x} ρ.
  Arguments wk_wk    {Γ' Γ x} ρ.

  Inductive Subst : Ctx -> Ctx -> Set :=
  | subst_id    Γ      : Subst Γ Γ
  | subst_shift Γ' Γ x :         Subst Γ' Γ -> Subst (CExt Γ' x) (CExt Γ x)
  | subst_subst Γ' Γ x : Tm Γ' -> Subst Γ' Γ -> Subst Γ'          (CExt Γ x)
  .

  Arguments subst_id    {Γ}.
  Arguments subst_shift {Γ' Γ x} σ.
  Arguments subst_subst {Γ' Γ x} M σ.

  Fixpoint wk_idx {Γ Γ'} (ρ : Wk Γ' Γ) : Idx Γ -> Idx Γ' :=
    match ρ with
    | wk_id => fun i => i
    | wk_shift ρ => fun i => match encode i with
                         | None => IZ
                         | Some i => IS (wk_idx ρ i)
                         end
    | wk_wk ρ => fun i => IS (wk_idx ρ i)
    end.

  Fixpoint wk_tm {Γ Γ'} (ρ : Wk Γ' Γ) (M : Tm Γ) : Tm Γ' :=
    match M with
    | TVar i => TVar (wk_idx ρ i)
    | TLam M => TLam (wk_tm (wk_shift ρ) M)
    | TApp M N => TApp (wk_tm ρ M) (wk_tm ρ N)
    end.

  Fixpoint subst_idx {Γ Γ'} (σ : Subst Γ' Γ) : Idx Γ -> Tm Γ' :=
    match σ with
    | subst_id => fun i => TVar i
    | subst_shift σ => fun i => match encode i with
                            | None => TVar IZ
                            | Some i => wk_tm (wk_wk wk_id) (subst_idx σ i)
                            end
    | subst_subst M σ => fun i => match encode i with
                              | None => M
                              | Some i => subst_idx σ i
                              end
    end.

  Fixpoint subst_tm {Γ Γ'} (σ : Subst Γ' Γ) (M : Tm Γ) : Tm Γ' :=
    match M with
    | TVar i => subst_idx σ i
    | TLam M => TLam (subst_tm (subst_shift σ) M)
    | TApp M N => TApp (subst_tm σ M) (subst_tm σ N)
    end.

  Definition bind {Γ} : forall x, Tm (Γ, x) -> Tm (Γ, *) :=
    fun x M => wk_tm (wk_shift wk_id) M.

  Inductive Ctx_elem_of : ElemOf string Ctx :=
  | Ctx_elem_of_here Γ x y (H : y = x) : Ctx_elem_of x (Γ, y)
  | Ctx_elem_of_further Γ x y (H : y <> Some x) : Ctx_elem_of x Γ -> Ctx_elem_of x (CExt Γ y)
  .
  #[global] Existing Instance Ctx_elem_of.

  #[global] Instance decide_Ctx_elem_of : RelDecision Ctx_elem_of.
  Proof.
    intros x Γ.
    induction Γ.
    - right. intro F. inversion F.
    - destruct (decide (o = Some x)).
      + subst. left. eapply Ctx_elem_of_here. reflexivity.
      + destruct IHΓ.
        * left. eapply Ctx_elem_of_further; eauto.
        * right. intro F. inversion F; subst; congruence.
  Defined.

  Program Fixpoint find_idx {Γ} : forall x, Ctx_elem_of x Γ -> Idx Γ :=
    match Γ with
    | CNil => fun x H => _
    | CExt Γ y => fun x H =>
                   match decide (y = Some x) with
                   | left _ => IZ
                   | right E => IS (find_idx x _)
                   end
    end.
  Next Obligation.
    intros. exfalso. inversion H.
  Qed.
  Next Obligation.
    intros. inversion H.
    - congruence.
    - eauto.    
  Qed.

  Definition TNVar {Γ} (x : string) (H : Ctx_elem_of x Γ) : Tm Γ := TVar (find_idx x H).

  Notation "#0" := (TVar IZ).
  Notation "#1" := (TVar (IS IZ)).
  Notation "#2" := (TVar (IS (IS IZ))).
  Notation "#3" := (TVar (IS (IS (IS IZ)))).
  Notation "% x" := (TNVar x _) (at level 40).
  Notation "'lam' x => M" := (TLam (bind x M)) (at level 60, right associativity).
  Notation "'lam.' M" := (TLam M) (at level 60, right associativity).
  Notation "M ⋅ N" := (TApp M N) (at level 50, left associativity).

  Ltac solve_scope :=
    intros;
    match goal with
    | [ |- Ctx_elem_of ?x ?Γ ] => exact (Decision_yes (decide_Ctx_elem_of x Γ))
    end.

  Program Definition tm_id {Γ} : Tm Γ := lam "x" => %"x".
  Solve All Obligations with solve_scope.

  Program Definition tm_ω {Γ} : Tm Γ := lam "x" => %"x" ⋅ %"x".
  Solve All Obligations with solve_scope.

  Definition tm_Ω {Γ} : Tm Γ := tm_ω ⋅ tm_ω.

  Program Definition tm_Y {Γ} : Tm Γ := lam "f" => (lam "x" => %"f" ⋅ (%"x" ⋅ %"x")) ⋅ (lam "x" => %"f" ⋅ (%"x" ⋅ %"x")).
  Solve All Obligations with solve_scope.

End Syntax.