Some basic untyped lambda calculus semantics

untyped.v

Require Import Coq.Unicode.Utf8.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.SetoidClass.
Require Import Coq.Program.Basics.
Require Import Coq.Relations.Relation_Definitions.
Require Coq.Vectors.Vector.
Require Coq.Vectors.Fin.
Require Coq.Lists.List.

Import IfNotations.
Import List.ListNotations.
Import Vector.VectorNotations.

(* Mostly taken from plfa's chapter on denotations *)

Fixpoint tip {n} (x: Fin.t n): nat :=
  match x with
  | @Fin.F1 n' => n'
  | Fin.FS x' => S (tip x')
  end.

Fixpoint eq_dec {n} (x: Fin.t n): Fin.t n → option (Fin.t (tip x)).
Proof.
  destruct x.
  all: cbn.
  - intro y.
    inversion y.
    * exact None.
    * exact (Some H0).
  - intro y.
    inversion y.
    * exact (Some Fin.F1).
    * subst.
      destruct (eq_dec _ x H0).
      2: exact None.
      exact (Some (Fin.FS t)).
Defined.

Module Term.
  Inductive t {n: nat}: Set :=
  | var: Fin.t n → t
  | Λ: @t (S n) → t
  | app: t → t → t.
  Arguments t: clear implicits.

  Fixpoint wk {n} (e: t n): t (S n) :=
    match e with
    | var x => var (Fin.FS x)
    | Λ e => Λ (wk e)
    | app e1 e2 => app (wk e1) (wk e2)
    end.

  Fixpoint subst {n} (x: Fin.t n) (s: t (tip x)) (e: t n): t (tip x) :=
    match e with
    | var y => match eq_dec x y with
               | None => s
               | Some y' => var y'
               end
    | Λ e => Λ (subst (Fin.FS x) (wk s) e)
    | app e1 e2 => app (subst x s e1) (subst x s e2)
    end.
End Term.

Inductive sort :=
| any
| meet (τ1 τ2: sort)
| fn (τ1 τ2: sort).

Notation "⊤" := any.
Infix "∩" := meet (at level 30).

Inductive le: relation sort :=
| refl: Reflexive le
| trans: Transitive le

| le_fn: Proper (Basics.flip le ==> le ==> le) fn

| le_any A: ⊤ ≤ A

| le_fanin A B C:
  A ≤ C →
  B ≤ C →
  (A ∩ B) ≤ C
| le_i1 A B: A ≤ (A ∩ B)
| le_i2 A B: B ≤ (A ∩ B)
where "A ≤ B" := (le A B).

Existing Instance refl.
Existing Instance trans.
Existing Instance le_fn.

Instance le_PreOrder: PreOrder le := {
    PreOrder_Reflexive := _ ;
}.

Instance meet_Proper: Proper (le ==> le ==> le) meet.
Proof.
  intros ? ? p ? ? q.
  apply le_fanin.
  - rewrite p.
    apply le_i1.
  - rewrite q.
    apply le_i2.
Qed.

Module Var.
  Section var.
    Context {A: sort}.

    Inductive t: list sort → Type :=
    | Z {Γ}: t (A :: Γ)
    | S {Γ B}: t Γ → t (B :: Γ).
  End var.

  Arguments t: clear implicits.

  Fixpoint rm {A} Γ (x: t A Γ) {struct x}: list _ :=
    match x with
    | @Z _ Γ' => Γ'
    | @S _ Γ' B x' => B :: rm Γ' x'
    end.

  Definition discrim {A B Γ} (x: t A (B :: Γ)): t A Γ + {B = A} :=
    match x with
    | Z => inright eq_refl
    | S x' => inleft x'
    end.

  Fixpoint wk {A B Γ} (x: t A Γ): t B (rm Γ x) → t B Γ :=
    match x with
    | Z => λ y, S y
    | S x' => λ y,
        match discrim y with
        | inleft y' => S (wk x' y')
        | inright p =>
            match p with
            | eq_refl => Z
            end
        end
    end.

  Fixpoint eq_dec {A B Γ} (x: t A Γ): t B Γ → t B (rm Γ x) + {A = B} :=
      match x with
      | Z => λ y, discrim y
      | S x' => λ y,
          match discrim y with
          | inleft y' =>
              match eq_dec x' y' with
              | inleft z => inleft (S z)
              | inright p => inright p
              end
          | inright p => inleft (match p with
                                 | eq_refl => Z
                                 end)
          end
      end.
End Var.

Infix "-" := Var.rm.

Reserved Notation "Γ ⊢ e ∈ τ" (at level 90).

Module Judge.
  Inductive t {n} {Γ: Vector.t sort n}: Term.t n → sort → Prop :=
  | var {x}:
    Γ ⊢ Term.var x ∈ Γ [@ x]
  | Λ {e: Term.t (S _)} {τ1 τ2}:
    τ1 :: Γ ⊢ e ∈ τ2 →
    Γ ⊢ Term.Λ e ∈ fn τ1 τ2
  | app {e1 e2} {τ1 τ2}:
    Γ ⊢ e1 ∈ fn τ1 τ2 →
    Γ ⊢ e2 ∈ τ1 →
    Γ ⊢ Term.app e1 e2 ∈ τ2

  | any {e}: Γ ⊢ e ∈ ⊤
  | meet {e τ1 τ2}:
    Γ ⊢ e ∈ τ1 →
    Γ ⊢ e ∈ τ2 →
    Γ ⊢ e ∈ τ1 ∩ τ2
  | sub {e τ1 τ2}:
    Γ ⊢ e ∈ τ1 →
    τ2 ≤ τ1 →
    Γ ⊢ e ∈ τ2

  where "Γ ⊢ e ∈ τ" := (@t _ Γ e τ).
  Arguments t {n}.
End Judge.

Notation "Γ ⊢ e ∈ τ" := (Judge.t Γ e τ).

Definition Forall2_hd {A P} {n} {Γ Δ: Vector.t A (S n)} (f: Vector.Forall2 P Γ Δ): P (Vector.hd Γ) (Vector.hd Δ) :=
  match f in @Vector.Forall2 _ _ _ (S n') Γ' Δ' return P (Vector.hd Γ') (Vector.hd Δ') with
  | Vector.Forall2_cons _ _ _ _ _ h _ => h
  end.

Definition Forall2_tl {A P} {n} {Γ Δ: Vector.t A (S n)} (f: Vector.Forall2 P Γ Δ): Vector.Forall2 P (Vector.tl Γ) (Vector.tl Δ) :=
  match f in @Vector.Forall2 _ _ _ (S n') Γ' Δ' return Vector.Forall2 P (Vector.tl Γ') (Vector.tl Δ') with
  | Vector.Forall2_cons _ _ _ _ _ _ t => t
  end.

Lemma Forall_app {A P} {n}: ∀ {Γ Δ: Vector.t A n} (f: Vector.Forall2 P Γ Δ), ∀ {x}, P (Γ[@x]) (Δ[@x]).
Proof.
Admitted.

Lemma weaken: ∀ {n} {Γ Δ: Vector.t _ n}, Vector.Forall2 le Γ Δ → ∀ {e τ}, Γ ⊢ e ∈ τ → Δ ⊢ e ∈ τ.
Proof.
  refine (fix loop _ Γ Δ _ _ _ P {struct P} := _).
  inversion P.
  all: subst.
  - eapply (@Judge.sub _ _ _ (Δ[@x])).
    2: {
      apply (Forall_app f).
    }
    constructor.
  - constructor.
    eapply loop.
    2: eapply H.
    constructor.
    1: reflexivity.
    eauto.
  - econstructor.
    all: eauto.
  - econstructor.
    all: eauto.
  - econstructor.
    all: eauto.
  - econstructor.
    all: eauto.
Qed.

Module Model.
  Definition t (n: nat): Type :=
    Vector.t sort n → sort → Prop.

  Definition refine {n}: relation (t n) :=
    pointwise_relation (Vector.t sort n) (pointwise_relation sort (Basics.flip impl)).

  #[global]
  Instance refine_Reflexive {n}: Reflexive (@refine n).
  Proof.
    unfold Reflexive, refine.
    reflexivity.
  Qed.

  #[global]
  Instance refine_Transitive {n}: Transitive (@refine n).
  Proof.
    unfold Transitive, refine.
    intros ? ? ? p.
    rewrite p.
    auto.
  Qed.

  #[global]
  Instance refine_PreOrder {n}: PreOrder (@refine n) := {
      PreOrder_Reflexive := _ ;
    }.

  Definition equiv {n}: relation (t n) :=
    pointwise_relation (Vector.t sort n) (pointwise_relation sort iff).

  #[global]
  Instance equiv_Reflexive {n}: Reflexive (@equiv n).
  Proof.
    unfold Reflexive, refine.
    reflexivity.
  Qed.

  #[global]
  Instance equiv_Symmetric {n}: Symmetric (@equiv n).
  Proof.
    unfold Symmetric, refine.
    symmetry.
    auto.
  Qed.

  #[global]
  Instance equiv_Transitive {n}: Transitive (@equiv n).
  Proof.
    unfold Transitive, refine.
    intros ? ? ? p.
    rewrite p.
    auto.
  Qed.

  #[global]
  Instance equiv_Equivalence {n}: Equivalence (@equiv n) := {
      Equivalence_Reflexive := _ ;
  }.

  #[global]
  Instance t_Setoid {n}: Setoid (@t n) := {
      equiv := @equiv n ;
    }.

  Definition var {n} (x: Fin.t n): Model.t n :=
    λ Γ τ,
       τ ≤ Γ [@ x].

  Inductive Λ {n} (P: Model.t (S n)): Model.t n :=
  | Λ_fn {Γ τ1 τ2}: P (τ1 :: Γ) τ2 → Λ P Γ (fn τ1 τ2)
  | Λ_any {Γ}: Λ P Γ ⊤
  | Λ_meet {Γ τ1 τ2}:
    Λ P Γ τ1 → Λ P Γ τ2 →
    Λ P Γ (τ1 ∩ τ2)
  .

  Inductive app {n} (P Q: Model.t n): Model.t n :=
  | app_any {Γ}: app P Q Γ ⊤
  | app_meet {Γ τ1 τ2}:
    app P Q Γ τ1 → app P Q Γ τ2 →
    app P Q Γ (τ1 ∩ τ2)
  | app_fn {Γ τ1 τ2}: P Γ (fn τ1 τ2) → Q Γ τ1 → app P Q Γ τ2
  .

  #[global]
  Instance equiv_refine_subrelation {n}: subrelation (@equiv n) refine.
  Proof.
    intros ? ? p ? ? ?.
    apply (p _ _).
    auto.
  Qed.

  #[global]
  Instance Λ_Proper {n}: Proper (refine ==> @refine n) Λ.
  Proof.
    unfold refine.
    intros ? ? p ? ? q.
    induction q.
    all: econstructor.
    all: eauto.
    all: apply (p _ _).
    all: auto.
  Qed.

  #[global]
    Instance app_Proper {n}: Proper (refine ==> refine ==> @refine n) app.
  Proof.
    unfold refine.
    intros ? ? p ? ? q ? ? r.
    induction r.
    all: econstructor.
    all: eauto.
    all: try apply p.
    all: try apply q.
    all: eauto.
  Qed.

  #[global]
  Instance Λ_equiv_Proper {n}: Proper (equiv ==> @equiv n) Λ.
  Proof.
    unfold equiv.
    intros ? ? p.
    split.
    all: intros q.
    all: induction q.
    all: econstructor.
    all: eauto.
    all: apply (p _ _).
    all: auto.
  Qed.

  #[global]
  Instance app_equiv_Proper {n}: Proper (equiv ==> equiv ==> @equiv n) app.
  Proof.
    unfold equiv.
    intros ? ? p ? ? q.
    split.
    all: intros r.
    all: induction r.
    all: econstructor.
    all: eauto.
    all: try apply p.
    all: try apply q.
    all: eauto.
  Qed.
End Model.

Infix "⊆" := Model.refine (at level 90).

Definition model {n} (e: Term.t n): Model.t n := λ (Γ: Vector.t _ n) τ, Γ ⊢ e ∈ τ.

Fixpoint eval {n} (e: Term.t n): Model.t n :=
  match e with
  | Term.var x => Model.var x
  | Term.app e1 e2 => Model.app (eval e1) (eval e2)
  | Term.Λ e => Model.Λ (eval e)
  end.

Definition equiv {n} (x y: Term.t n) := model x == model y.

#[global]
Instance equiv_Reflexive {n}: Reflexive (@equiv n).
Proof.
  unfold Reflexive,equiv.
  reflexivity.
Qed.

#[global]
Instance equiv_Transitive {n}: Transitive (@equiv n).
Proof.
  unfold Transitive, equiv.
  intros ? ? ? p.
  rewrite p.
  auto.
Qed.

#[global]
Instance equiv_Symmetric {n}: Symmetric (@equiv n).
Proof.
  unfold Symmetric, equiv.
  intros ? ? p.
  symmetry.
  auto.
Qed.

#[global]
Instance equiv_Equivalence {n}: Equivalence (@equiv n) := {
   Equivalence_Reflexive := _ ;
 }.

#[global]
Instance Term_Setoid {n}: Setoid (@Term.t n) := {
    equiv := @equiv n ;
}.

Lemma var_ref {n} {x: Fin.t n}: Model.var x ⊆ model (Term.var x).
Proof.
  unfold Model.var, model.
  refine (fix loop _ _ P {struct P} := _).
  inversion P.
  all: subst.
  - reflexivity.
  - apply le_any.
  - apply le_fanin.
    + eapply loop.
      eauto.
    + eapply loop.
      eauto.
  - rewrite H0.
    eapply loop.
    eauto.
Qed.

Lemma ref_var {n} {x: Fin.t n}: model (Term.var x) ⊆ Model.var x.
Proof.
  unfold Model.var, model.
  intros ? ? ?.
  eapply Judge.sub.
  2: eauto.
  constructor.
Qed.

Lemma model_var {n} {x: Fin.t n}: model (Term.var x) == Model.var x.
Proof.
  unfold model, Model.var.
  split.
  - apply var_ref.
  - apply ref_var.
Qed.

Lemma Λ_sub {n} {e: Term.t (S n)}: ∀ {τ1 τ2}, τ1 ≤ τ2 →
  ∀ {Γ}, Model.Λ (model e) Γ τ2 → Model.Λ (model e) Γ τ1.
Proof.
  refine (fix loop _ _ P {struct P} := _).
  inversion P.
  all: subst.
  - auto.
  - intros.
    apply (loop _ _ H).
    eauto.
  - unfold model.
    intros.
    inversion H1.
    subst.
    constructor.
    eapply Judge.sub.
    all: eauto.
    unfold Basics.flip in H.
    eapply weaken.
    2: eapply H4.
    constructor.
    1: auto.
    clear.
    induction Γ.
    1: constructor.
    constructor.
    1: reflexivity.
    auto.
  - intro.
    constructor.
  - intro.
    constructor.
    all: eauto.
  - intros ? q.
    inversion q.
    auto.
  - intros ? q.
    inversion q.
    auto.
Qed.

Lemma Λ_ref {n} {e: Term.t (S n)}: Model.Λ (model e) ⊆ model (Term.Λ e).
Proof.
  refine (fix loop _ _ P {struct P} := _).
  inversion P.
  all: subst.
  - constructor.
    auto.
  - constructor.
  - constructor.
    all: eauto.
  - apply (Λ_sub H0).
    eauto.
Qed.

Lemma ref_Λ {n} {e: Term.t (S n)}: model (Term.Λ e) ⊆ Model.Λ (model e).
Proof.
  refine (fix loop _ _ P {struct P} := _).
  inversion P.
  all: subst.
  - constructor.
    auto.
  - constructor.
  - constructor.
    all: apply loop.
    all: eauto.
Qed.

Lemma model_Λ {n} (e: Term.t (S n)): model (Term.Λ e) == Model.Λ (model e).
Proof.
  split.
  - apply Λ_ref.
  - apply ref_Λ.
Qed.

Lemma app_sub {n} {e1 e2: Term.t n}:
  ∀{τ1 τ2}, τ1 ≤ τ2 →
  ∀ {Γ}, Model.app (model e1) (model e2) Γ τ2 → Model.app (model e1) (model e2) Γ τ1.
Proof.
  refine (fix loop _ _ P {struct P} := _).
  inversion P.
  all: subst.
  - intros.
    auto.
  - intros.
    eapply loop.
    all: eauto.
  - intros.
    inversion H1.
    subst.
    econstructor.
    all: eauto.
    eapply Judge.sub.
    all: eauto.
    unfold Basics.flip in H.
    rewrite P.
    reflexivity.
  - intro.
    constructor.
  - intro.
    constructor.
    all: eauto.
  - intros ? q.
    inversion q.
    + subst.
      eauto.
    + subst.
      econstructor.
      all: eauto.
      eapply Judge.sub.
      eauto.
      rewrite <- P.
      reflexivity.
  - intros ? q.
    inversion q.
    + subst.
      eauto.
    + subst.
      econstructor.
      all: eauto.
      eapply Judge.sub.
      all: eauto.
      rewrite <- P.
      reflexivity.
Qed.

Lemma app_ref {n} {e1 e2: Term.t n}:
  Model.app (model e1) (model e2) ⊆ model (Term.app e1 e2).
Proof.
  refine (fix loop _ _ P {struct P} := _).
  inversion P.
  all: subst.
  - econstructor.
    all: eauto.
  - constructor.
  - constructor.
    all: eauto.
  - eapply app_sub.
    all: eauto.
Qed.

Lemma ref_app {n} {e1 e2: Term.t n}: model (Term.app e1 e2) ⊆ Model.app (model e1) (model e2).
Proof.
  refine (fix loop _ _ P {struct P} := _).
  inversion P.
  all: subst.
  - constructor.
  - constructor.
    all: apply loop.
    all: eauto.
  - econstructor.
    all: eauto.
Qed.

Lemma model_app {n} (e1 e2: Term.t n): model (Term.app e1 e2) == Model.app (model e1) (model e2).
Proof.
  split.
  - apply app_ref.
  - apply ref_app.
Qed.

Lemma eval_model {n} (e: Term.t n): model e == eval e.
Proof.
  induction e.
  all: cbn.
  - rewrite model_var.
    reflexivity.
  - rewrite model_Λ.
    rewrite IHe.
    reflexivity.
  - rewrite model_app.
    rewrite IHe1, IHe2.
    reflexivity.
Qed.